Documentation

Mathlib.Data.Set.Inclusion

Lemmas about inclusion, the injection of subtypes induced by ⊆ #

source
@[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

Instances For
    source
    theorem Set.inclusion_self {α : Type u_1} {s : Set α} (x : ↑s) :
    inclusion ⋯ x = x
    source
    theorem Set.inclusion_eq_id {α : Type u_1} {s : Set α} (h : s ⊆ s) :
    inclusion h = id
    source
    theorem Set.inclusion_eq_subtype_map {α : Type u_1} {s t : Set α} (h : s ⊆ t) :
    inclusion h = Subtype.map id h
    source
    @[simp]
    theorem Set.inclusion_mk {α : Type u_1} {s t : Set α} {h : s ⊆ t} (a : α) (ha : a ∈ s) :
    inclusion h ⟨a, ha⟩ = ⟨a, ⋯⟩
    source
    theorem Set.inclusion_right {α : Type u_1} {s t : Set α} (h : s ⊆ t) (x : ↑t) (m : ↑x ∈ s) :
    inclusion h ⟨↑x, m⟩ = x
    source
    @[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
    source
    @[simp]
    theorem Set.inclusion_comp_inclusion {α : Type u_2} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) :
    inclusion htu ∘ inclusion hst = inclusion ⋯
    source
    @[simp]
    theorem Set.coe_inclusion {α : Type u_1} {s t : Set α} (h : s ⊆ t) (x : ↑s) :
    ↑(inclusion h x) = ↑x
    source
    theorem Set.val_comp_inclusion {α : Type u_1} {s t : Set α} (h : s ⊆ t) :
    Subtype.val ∘ inclusion h = Subtype.val
    source
    theorem Set.inclusion_injective {α : Type u_1} {s t : Set α} (h : s ⊆ t) :
    Function.Injective (inclusion h)
    source
    theorem Set.inclusion_inj {α : Type u_1} {s t : Set α} (h : s ⊆ t) {x y : ↑s} :
    inclusion h x = inclusion h y ↔ x = y
    source
    theorem Set.eq_of_inclusion_surjective {α : Type u_1} {s t : Set α} {h : s ⊆ t} (h_surj : Function.Surjective (inclusion h)) :
    s = t
    source
    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
    source
    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