Lemmas about inclusion, the injection of subtypes induced by ⊆

@[reducible, inline]

abbrev Set.inclusion {α : Type u_1} {s t : Set α} (h : s ⊆ t) : ↑s → ↑t

inclusion is the "identity" function between two subsets s and t, where s ⊆ t

Equations

• Set.inclusion h x = ⟨↑x, ⋯⟩

theorem Set.inclusion_self {α : Type u_1} {s : Set α} (x : ↑s) : inclusion ⋯ x = x

theorem Set.inclusion_eq_id {α : Type u_1} {s : Set α} (h : s ⊆ s) : inclusion h = id

@[simp]

theorem Set.inclusion_mk {α : Type u_1} {s t : Set α} {h : s ⊆ t} (a : α) (ha : a ∈ s) : inclusion h ⟨a, ha⟩ = ⟨a, ⋯⟩

theorem Set.inclusion_right {α : Type u_1} {s t : Set α} (h : s ⊆ t) (x : ↑t) (m : ↑x ∈ s) : inclusion h ⟨↑x, m⟩ = x

@[simp]

theorem Set.inclusion_inclusion {α : Type u_1} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) (x : ↑s) : inclusion htu (inclusion hst x) = inclusion ⋯ x

@[simp]

theorem Set.inclusion_comp_inclusion {α : Type u_2} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) : inclusion htu ∘ inclusion hst = inclusion ⋯

@[simp]

theorem Set.coe_inclusion {α : Type u_1} {s t : Set α} (h : s ⊆ t) (x : ↑s) : ↑(inclusion h x) = ↑x

theorem Set.val_comp_inclusion {α : Type u_1} {s t : Set α} (h : s ⊆ t) : Subtype.val ∘ inclusion h = Subtype.val

theorem Set.inclusion_injective {α : Type u_1} {s t : Set α} (h : s ⊆ t) : Function.Injective (inclusion h)

theorem Set.inclusion_inj {α : Type u_1} {s t : Set α} (h : s ⊆ t) {x y : ↑s} : inclusion h x = inclusion h y ↔ x = y

theorem Set.eq_of_inclusion_surjective {α : Type u_1} {s t : Set α} {h : s ⊆ t} (h_surj : Function.Surjective (inclusion h)) : s = t

theorem Set.inclusion_le_inclusion {α : Type u_1} [LE α] {s t : Set α} (h : s ⊆ t) {x y : ↑s} : inclusion h x ≤ inclusion h y ↔ x ≤ y

theorem Set.inclusion_lt_inclusion {α : Type u_1} [LT α] {s t : Set α} (h : s ⊆ t) {x y : ↑s} : inclusion h x < inclusion h y ↔ x < y