doc-next-gen

Mathlib.Data.Set.Inclusion

Module docstring

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

Set.inclusion abbrev
(h : s ⊆ t) : s → t
Full source 
/-- `inclusion` is the "identity" function between two subsets `s` and `t`, where `s ⊆ t` -/
abbrev inclusion (h : s ⊆ t) : s → t := fun x : s => (⟨x, h x.2⟩ : t)
Canonical Inclusion of Subsets
Informal description
Given two subsets $s$ and $t$ of a type $\alpha$ such that $s \subseteq t$, the function $\text{inclusion}(h) : s \to t$ is the canonical injection that maps each element of $s$ to itself, viewed as an element of $t$.
Set.inclusion_self theorem
(x : s) : inclusion Subset.rfl x = x
Full source 
theorem inclusion_self (x : s) : inclusion Subset.rfl x = x := by
  cases x
  rfl
Inclusion of a Subset into Itself is the Identity
Informal description
For any element $x$ of a subset $s$ of a type $\alpha$, the canonical inclusion map $\text{inclusion}(\text{Subset.rfl})$ applied to $x$ equals $x$ itself.
Set.inclusion_eq_id theorem
(h : s ⊆ s) : inclusion h = id
Full source 
theorem inclusion_eq_id (h : s ⊆ s) : inclusion h = id :=
  funext inclusion_self
Inclusion into Self is Identity
Informal description
For any subset $s$ of a type $\alpha$, the canonical inclusion map $\text{inclusion}(h) : s \to s$ (where $h$ is the proof that $s \subseteq s$) is equal to the identity function $\text{id}$ on $s$.
Set.inclusion_mk theorem
{h : s ⊆ t} (a : α) (ha : a ∈ s) : inclusion h ⟨a, ha⟩ = ⟨a, h ha⟩
Full source 
@[simp]
theorem inclusion_mk {h : s ⊆ t} (a : α) (ha : a ∈ s) : inclusion h ⟨a, ha⟩ = ⟨a, h ha⟩ :=
  rfl
Canonical Inclusion Maps Elements to Themselves in Larger Subset
Informal description
Given subsets $s \subseteq t$ of a type $\alpha$, an element $a \in \alpha$, and a proof $ha$ that $a \in s$, the canonical inclusion map $\text{inclusion}(h)$ sends the element $\langle a, ha \rangle$ of $s$ to the element $\langle a, h ha \rangle$ of $t$.
Set.inclusion_right theorem
(h : s ⊆ t) (x : t) (m : (x : α) ∈ s) : inclusion h ⟨x, m⟩ = x
Full source 
theorem inclusion_right (h : s ⊆ t) (x : t) (m : (x : α) ∈ s) : inclusion h ⟨x, m⟩ = x := by
  cases x
  rfl
Right Inclusion Maps Elements to Themselves
Informal description
Given subsets $s$ and $t$ of a type $\alpha$ with $s \subseteq t$, for any element $x \in t$ such that $x \in s$, the canonical inclusion map $\text{inclusion}(h)$ sends the element $\langle x, m \rangle$ (where $m$ is the proof that $x \in s$) to $x$ itself.
Set.inclusion_inclusion theorem
(hst : s ⊆ t) (htu : t ⊆ u) (x : s) : inclusion htu (inclusion hst x) = inclusion (hst.trans htu) x
Full source 
@[simp]
theorem inclusion_inclusion (hst : s ⊆ t) (htu : t ⊆ u) (x : s) :
    inclusion htu (inclusion hst x) = inclusion (hst.trans htu) x := by
  cases x
  rfl
Composition of Canonical Inclusions Commutes with Transitivity of Subset Relations
Informal description
Given subsets $s \subseteq t \subseteq u$ of a type $\alpha$, for any element $x \in s$, the composition of the canonical inclusions $\text{inclusion}(h_{tu}) \circ \text{inclusion}(h_{st})$ applied to $x$ is equal to the canonical inclusion $\text{inclusion}(h_{st} \circ h_{tu})$ applied to $x$. In other words, the following diagram commutes: $$\text{inclusion}(h_{tu}) \circ \text{inclusion}(h_{st}) = \text{inclusion}(h_{st} \circ h_{tu})$$
Set.inclusion_comp_inclusion theorem
{α} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) : inclusion htu ∘ inclusion hst = inclusion (hst.trans htu)
Full source 
@[simp]
theorem inclusion_comp_inclusion {α} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u) :
    inclusioninclusion htu ∘ inclusion hst = inclusion (hst.trans htu) :=
  funext (inclusion_inclusion hst htu)
Composition of Inclusion Maps Commutes with Subset Transitivity
Informal description
Given subsets $s \subseteq t \subseteq u$ of a type $\alpha$, the composition of the canonical inclusion maps $\text{inclusion}(h_{tu}) \circ \text{inclusion}(h_{st})$ is equal to the canonical inclusion map $\text{inclusion}(h_{st} \circ h_{tu})$. In other words, the following diagram commutes: $$\text{inclusion}(h_{tu}) \circ \text{inclusion}(h_{st}) = \text{inclusion}(h_{st} \circ h_{tu})$$
Set.coe_inclusion theorem
(h : s ⊆ t) (x : s) : (inclusion h x : α) = (x : α)
Full source 
@[simp]
theorem coe_inclusion (h : s ⊆ t) (x : s) : (inclusion h x : α) = (x : α) :=
  rfl
Inclusion Preserves Underlying Element
Informal description
For any subsets $s$ and $t$ of a type $\alpha$ with $s \subseteq t$, and for any element $x \in s$, the underlying element in $\alpha$ of the inclusion map $\text{inclusion}(h)(x) \in t$ is equal to $x$ itself, i.e., $\text{inclusion}(h)(x) = x$ as elements of $\alpha$.
Set.val_comp_inclusion theorem
(h : s ⊆ t) : Subtype.val ∘ inclusion h = Subtype.val
Full source 
theorem val_comp_inclusion (h : s ⊆ t) : Subtype.valSubtype.val ∘ inclusion h = Subtype.val :=
  rfl
Composition of Inclusion with Subtype Coercion Equals Direct Coercion
Informal description
For any subsets $s$ and $t$ of a type $\alpha$ with $s \subseteq t$, the composition of the canonical inclusion map $\text{inclusion}(h) : s \to t$ with the subtype coercion $\text{Subtype.val} : t \to \alpha$ equals the direct subtype coercion $\text{Subtype.val} : s \to \alpha$. In other words, for all $x \in s$, we have $(\text{inclusion}(h)(x)) = x$ as elements of $\alpha$.
Set.inclusion_injective theorem
(h : s ⊆ t) : Injective (inclusion h)
Full source 
theorem inclusion_injective (h : s ⊆ t) : Injective (inclusion h)
  | ⟨_, _⟩, ⟨_, _⟩ => Subtype.ext_iff_val.2 ∘ Subtype.ext_iff_val.1
Injectivity of Subset Inclusion Map
Informal description
For any subsets $s$ and $t$ of a type $\alpha$ such that $s \subseteq t$, the canonical inclusion map $\text{inclusion}(h) : s \to t$ is injective. That is, for any $x, y \in s$, if $\text{inclusion}(h)(x) = \text{inclusion}(h)(y)$, then $x = y$.
Set.inclusion_inj theorem
(h : s ⊆ t) {x y : s} : inclusion h x = inclusion h y ↔ x = y
Full source 
theorem inclusion_inj (h : s ⊆ t) {x y : s} : inclusioninclusion h x = inclusion h y ↔ x = y :=
  (inclusion_injective h).eq_iff
Inclusion Map is Injective: $\text{inclusion}(h)(x) = \text{inclusion}(h)(y) \leftrightarrow x = y$
Informal description
For any subsets $s$ and $t$ of a type $\alpha$ with $s \subseteq t$, and for any elements $x, y \in s$, the canonical inclusion map $\text{inclusion}(h) : s \to t$ satisfies $\text{inclusion}(h)(x) = \text{inclusion}(h)(y)$ if and only if $x = y$.
Set.inclusion_le_inclusion theorem
[LE α] {s t : Set α} (h : s ⊆ t) {x y : s} : inclusion h x ≤ inclusion h y ↔ x ≤ y
Full source 
theorem inclusion_le_inclusion [LE α] {s t : Set α} (h : s ⊆ t) {x y : s} :
    inclusioninclusion h x ≤ inclusion h y ↔ x ≤ y := Iff.rfl
Order Preservation by Subset Inclusion
Informal description
Let $\alpha$ be a type equipped with a preorder $\leq$, and let $s$ and $t$ be subsets of $\alpha$ such that $s \subseteq t$. For any elements $x, y \in s$, the canonical inclusion map $\text{inclusion}(h) : s \to t$ preserves the order relation, i.e., $\text{inclusion}(h)(x) \leq \text{inclusion}(h)(y)$ if and only if $x \leq y$.
Set.inclusion_lt_inclusion theorem
[LT α] {s t : Set α} (h : s ⊆ t) {x y : s} : inclusion h x < inclusion h y ↔ x < y
Full source 
theorem inclusion_lt_inclusion [LT α] {s t : Set α} (h : s ⊆ t) {x y : s} :
    inclusioninclusion h x < inclusion h y ↔ x < y := Iff.rfl
Strict Order Preservation under Subset Inclusion
Informal description
Let $\alpha$ be a type with a strict order relation $<$, and let $s$ and $t$ be subsets of $\alpha$ such that $s \subseteq t$. For any elements $x, y \in s$, the canonical inclusion map $\text{inclusion}(h) : s \to t$ preserves the strict order, i.e., $\text{inclusion}(h)(x) < \text{inclusion}(h)(y)$ if and only if $x < y$.