Mathlib.Logic.Embedding.Set

Equiv.asEmbedding_range theorem

{α β : Sort _} {p : β → Prop} (e : α ≃ Subtype p) : Set.range e.asEmbedding = setOf p

Full source

@[simp]
theorem Equiv.asEmbedding_range {α β : Sort _} {p : β → Prop} (e : α ≃ Subtype p) :
    Set.range e.asEmbedding = setOf p :=
  Set.ext fun x ↦ ⟨fun ⟨y, h⟩ ↦ h ▸ Subtype.coe_prop (e y), fun hs ↦ ⟨e.symm ⟨x, hs⟩, by simp⟩⟩

Range of Equivalence-Induced Embedding Equals Predicate Set

Informal description

Let $\alpha$ and $\beta$ be types, and let $p : \beta \to \text{Prop}$ be a predicate on $\beta$. Given an equivalence $e : \alpha \simeq \{x \in \beta \mid p(x)\}$, the range of the embedding $e.\text{asEmbedding}$ is equal to the set $\{x \in \beta \mid p(x)\}$.

Function.Embedding.optionElim definition

{α β} (f : α ↪ β) (x : β) (h : x ∉ Set.range f) : Option α ↪ β

Full source

/-- Given an embedding `f : α ↪ β` and a point outside of `Set.range f`, construct an embedding
`Option α ↪ β`. -/
@[simps]
def optionElim {α β} (f : α ↪ β) (x : β) (h : x ∉ Set.range f) : OptionOption α ↪ β :=
  ⟨Option.elim' x f, Option.injective_iff.2 ⟨f.2, h⟩⟩

Embedding extension to Option type with a new point

Informal description

Given an embedding $f : \alpha \hookrightarrow \beta$ and a point $x \in \beta$ not in the range of $f$, the function constructs an embedding from $\text{Option}\ \alpha$ to $\beta$ by mapping $\text{none}$ to $x$ and $\text{some}\ a$ to $f(a)$.

Function.Embedding.optionEmbeddingEquiv definition

(α β) : (Option α ↪ β) ≃ Σ f : α ↪ β, ↥(Set.range f)ᶜ

Full source

/-- Equivalence between embeddings of `Option α` and a sigma type over the embeddings of `α`. -/
@[simps]
def optionEmbeddingEquiv (α β) : (Option α ↪ β) ≃ Σ f : α ↪ β, ↥(Set.range f)ᶜ where
  toFun f := ⟨Embedding.some.trans f, f none, fun ⟨x, hx⟩ ↦ Option.some_ne_none x <| f.injective hx⟩
  invFun f := f.1.optionElim f.2 f.2.2
  left_inv f := ext <| by rintro (_ | _) <;> simp [Option.coe_def]
  right_inv := fun ⟨f, y, hy⟩ ↦ by ext <;> simp [Option.coe_def]

Equivalence between Option embeddings and pairs of embeddings with an extra point

Informal description

The equivalence between embeddings of $\text{Option}\ \alpha$ into $\beta$ and pairs $(f, y)$, where $f$ is an embedding of $\alpha$ into $\beta$ and $y$ is an element of $\beta$ not in the range of $f$. Given an embedding $f : \text{Option}\ \alpha \hookrightarrow \beta$, the corresponding pair is obtained by restricting $f$ to $\alpha$ (via $\text{some}$) and taking $f(\text{none})$. Conversely, given an embedding $f : \alpha \hookrightarrow \beta$ and an element $y \in \beta$ not in the range of $f$, the corresponding embedding of $\text{Option}\ \alpha$ maps $\text{none}$ to $y$ and $\text{some}\ a$ to $f(a)$.

Function.Embedding.codRestrict definition

{α β} (p : Set β) (f : α ↪ β) (H : ∀ a, f a ∈ p) : α ↪ p

Full source

/-- Restrict the codomain of an embedding. -/
def codRestrict {α β} (p : Set β) (f : α ↪ β) (H : ∀ a, f a ∈ p) : α ↪ p :=
  ⟨fun a ↦ ⟨f a, H a⟩, fun _ _ h ↦ f.injective (congr_arg Subtype.val h)⟩

Codomain restriction of an embedding

Informal description

Given an embedding $f : \alpha \hookrightarrow \beta$ and a subset $p \subseteq \beta$ such that $f(a) \in p$ for all $a \in \alpha$, the function $\alpha \hookrightarrow p$ obtained by restricting the codomain of $f$ to $p$ is also an embedding.

Function.Embedding.codRestrict_apply theorem

{α β} (p) (f : α ↪ β) (H a) : codRestrict p f H a = ⟨f a, H a⟩

Full source

@[simp]
theorem codRestrict_apply {α β} (p) (f : α ↪ β) (H a) : codRestrict p f H a = ⟨f a, H a⟩ :=
  rfl

Evaluation of Codomain-Restricted Embedding: $\text{codRestrict}\ p\ f\ H\ a = \langle f(a), H(a) \rangle$

Informal description

For any sets $\alpha$ and $\beta$, a subset $p \subseteq \beta$, an embedding $f : \alpha \hookrightarrow \beta$, and an element $a \in \alpha$ such that $f(a) \in p$, the codomain-restricted embedding $\text{codRestrict}\ p\ f\ H$ evaluated at $a$ equals the pair $\langle f(a), H(a) \rangle$, where $H(a)$ is the proof that $f(a) \in p$.

Function.Embedding.image definition

{α β} (f : α ↪ β) : Set α ↪ Set β

Full source

/-- `Set.image` as an embedding `Set α ↪ Set β`. -/
@[simps apply]
protected def image {α β} (f : α ↪ β) : SetSet α ↪ Set β :=
  ⟨image f, f.2.image_injective⟩

Embedding of set images under an embedding

Informal description

Given an embedding $f : \alpha \hookrightarrow \beta$, the function that maps a subset $S \subseteq \alpha$ to its image $f(S) \subseteq \beta$ is also an embedding. This means the image function is injective with respect to subsets.

Set.embeddingOfSubset definition

{α} (s t : Set α) (h : s ⊆ t) : s ↪ t

Full source

/-- The injection map is an embedding between subsets. -/
@[simps apply_coe]
def embeddingOfSubset {α} (s t : Set α) (h : s ⊆ t) : s ↪ t :=
  ⟨fun x ↦ ⟨x.1, h x.2⟩, fun ⟨x, hx⟩ ⟨y, hy⟩ h ↦ by
    congr
    injection h⟩

Embedding of subset inclusion

Informal description

Given a type $\alpha$ and subsets $s, t \subseteq \alpha$ such that $s \subseteq t$, the injection map from $s$ to $t$ is an embedding. Specifically, it maps each element $x \in s$ to itself (viewed as an element of $t$), and this map is injective.

subtypeOrEquiv definition

(p q : α → Prop) [DecidablePred p] (h : Disjoint p q) : { x // p x ∨ q x } ≃ { x // p x } ⊕ { x // q x }

Full source

/-- A subtype `{x // p x ∨ q x}` over a disjunction of `p q : α → Prop` is equivalent to a sum of
subtypes `{x // p x} ⊕ {x // q x}` such that `¬ p x` is sent to the right, when
`Disjoint p q`.

See also `Equiv.sumCompl`, for when `IsCompl p q`. -/
@[simps apply]
def subtypeOrEquiv (p q : α → Prop) [DecidablePred p] (h : Disjoint p q) :
    { x // p x ∨ q x }{ x // p x ∨ q x } ≃ { x // p x } ⊕ { x // q x } where
  toFun := subtypeOrLeftEmbedding p q
  invFun :=
    Sum.elim (Subtype.impEmbedding _ _ fun x hx ↦ (Or.inl hx : p x ∨ q x))
      (Subtype.impEmbedding _ _ fun x hx ↦ (Or.inr hx : p x ∨ q x))
  left_inv x := by
    by_cases hx : p x
    · rw [subtypeOrLeftEmbedding_apply_left _ hx]
      simp [Subtype.ext_iff]
    · rw [subtypeOrLeftEmbedding_apply_right _ hx]
      simp [Subtype.ext_iff]
  right_inv x := by
    cases x with
    | inl x =>
      simp only [Sum.elim_inl]
      rw [subtypeOrLeftEmbedding_apply_left]
      · simp
      · simpa using x.prop
    | inr x =>
      simp only [Sum.elim_inr]
      rw [subtypeOrLeftEmbedding_apply_right]
      · simp
      · suffices ¬p x by simpa
        intro hp
        simpa using h.le_bot x ⟨hp, x.prop⟩

Equivalence between disjunctive subtype and sum of subtypes

Informal description

Given two predicates $p, q : \alpha \to \text{Prop}$ on a type $\alpha$ with a decidable predicate $p$, and assuming that $p$ and $q$ are disjoint (i.e., no element satisfies both $p$ and $q$), the subtype $\{x \mid p x \lor q x\}$ is equivalent to the sum of the subtypes $\{x \mid p x\} \oplus \{x \mid q x\}$. The equivalence maps elements satisfying $p$ to the left summand and elements satisfying $q$ to the right summand.

subtypeOrEquiv_symm_inl theorem

 (p q : α → Prop) [DecidablePred p] (h : Disjoint p q) (x : { x // p x }) :
  (subtypeOrEquiv p q h).symm (Sum.inl x) = ⟨x, Or.inl x.prop⟩

Full source

@[simp]
theorem subtypeOrEquiv_symm_inl (p q : α → Prop) [DecidablePred p] (h : Disjoint p q)
    (x : { x // p x }) : (subtypeOrEquiv p q h).symm (Sum.inl x) = ⟨x, Or.inl x.prop⟩ :=
  rfl

Inverse of Subtype Equivalence Maps Left Inclusion to Original Element

Informal description

Given two predicates $p, q : \alpha \to \text{Prop}$ on a type $\alpha$ with a decidable predicate $p$, and assuming that $p$ and $q$ are disjoint, for any element $x$ in the subtype $\{x \mid p x\}$, the inverse of the equivalence `subtypeOrEquiv` applied to the left inclusion of $x$ yields the element $\langle x, \text{Or.inl } x.\text{prop} \rangle$ in the subtype $\{x \mid p x \lor q x\}$.

subtypeOrEquiv_symm_inr theorem

 (p q : α → Prop) [DecidablePred p] (h : Disjoint p q) (x : { x // q x }) :
  (subtypeOrEquiv p q h).symm (Sum.inr x) = ⟨x, Or.inr x.prop⟩

Full source

@[simp]
theorem subtypeOrEquiv_symm_inr (p q : α → Prop) [DecidablePred p] (h : Disjoint p q)
    (x : { x // q x }) : (subtypeOrEquiv p q h).symm (Sum.inr x) = ⟨x, Or.inr x.prop⟩ :=
  rfl

Inverse of Subtype Equivalence Maps Right Inclusion to Original Element

Informal description

Given two predicates $p, q : \alpha \to \text{Prop}$ on a type $\alpha$ with a decidable predicate $p$, and assuming that $p$ and $q$ are disjoint, for any element $x$ in the subtype $\{x \mid q x\}$, the inverse of the equivalence `subtypeOrEquiv` applied to the right inclusion of $x$ yields the element $\langle x, \text{Or.inr } x.\text{prop} \rangle$ in the subtype $\{x \mid p x \lor q x\}$.

Function.Embedding.sumSet definition

(h : Disjoint s t) : s ⊕ t ↪ α

Full source

/-- For disjoint `s t : Set α`, the natural injection from `↑s ⊕ ↑t` to `α`. -/
@[simps] def Function.Embedding.sumSet (h : Disjoint s t) : s ⊕ ts ⊕ t ↪ α where
  toFun := Sum.elim (↑) (↑)
  inj' := by
    rintro (⟨a, ha⟩ | ⟨a, ha⟩) (⟨b, hb⟩ | ⟨b, hb⟩)
    · simp [Subtype.val_inj]
    · simpa using h.ne_of_mem ha hb
    · simpa using h.symm.ne_of_mem ha hb
    simp [Subtype.val_inj]

Embedding from disjoint union of subsets into $\alpha$

Informal description

For any two disjoint subsets $s$ and $t$ of a type $\alpha$, the natural embedding from the disjoint union $s \sqcup t$ to $\alpha$ is defined by mapping each element of $s$ and $t$ via their respective inclusion maps. This embedding is injective since $s$ and $t$ are disjoint.

Function.Embedding.coe_sumSet theorem

(h : Disjoint s t) : (Function.Embedding.sumSet h : s ⊕ t → α) = Sum.elim (↑) (↑)

Full source

@[norm_cast] lemma Function.Embedding.coe_sumSet (h : Disjoint s t) :
    (Function.Embedding.sumSet h : s ⊕ t → α) = Sum.elim (↑) (↑) := rfl

Embedding from Disjoint Union as Sum Elimination of Inclusions

Informal description

For any two disjoint subsets $s$ and $t$ of a type $\alpha$, the embedding function from the disjoint union $s \sqcup t$ to $\alpha$ is equal to the elimination of the inclusion maps from $s$ and $t$ into $\alpha$. That is, the embedding is given by mapping elements of $s$ and $t$ via their respective natural inclusions.

Function.Embedding.sumSet_preimage_inl theorem

(h : Disjoint s t) : .inl ⁻¹' (Function.Embedding.sumSet h ⁻¹' r) = r ∩ s

Full source

@[simp] theorem Function.Embedding.sumSet_preimage_inl (h : Disjoint s t) :
    .inl.inl ⁻¹' (Function.Embedding.sumSet h ⁻¹' r) = r ∩ s := by
  simp [Set.ext_iff]

Preimage of Subset under Left Inclusion in Disjoint Union Embedding

Informal description

For any two disjoint subsets $s$ and $t$ of a type $\alpha$, and any subset $r$ of $\alpha$, the preimage of $r$ under the embedding from the disjoint union $s \sqcup t$ to $\alpha$, restricted to the left summand $s$, is equal to the intersection $r \cap s$.

Function.Embedding.sumSet_preimage_inr theorem

(h : Disjoint s t) : .inr ⁻¹' (Function.Embedding.sumSet h ⁻¹' r) = r ∩ t

Full source

@[simp] theorem Function.Embedding.sumSet_preimage_inr (h : Disjoint s t) :
    .inr.inr ⁻¹' (Function.Embedding.sumSet h ⁻¹' r) = r ∩ t := by
  simp [Set.ext_iff]

Preimage of Subset under Right Inclusion in Disjoint Union Embedding

Informal description

For any two disjoint subsets $s$ and $t$ of a type $\alpha$, and any subset $r$ of $\alpha$, the preimage of $r$ under the embedding from the disjoint union $s \sqcup t$ to $\alpha$, restricted to the right summand $t$, is equal to the intersection $r \cap t$. In other words, the preimage of $r$ via the right inclusion map is exactly the elements of $r$ that lie in $t$.

Function.Embedding.sumSet_range theorem

{s t : Set α} (h : Disjoint s t) : range (Function.Embedding.sumSet h) = s ∪ t

Full source

@[simp] theorem Function.Embedding.sumSet_range {s t : Set α} (h : Disjoint s t) :
    range (Function.Embedding.sumSet h) = s ∪ t := by
  simp [Set.ext_iff]

Range of Disjoint Union Embedding Equals Union of Subsets

Informal description

For any two disjoint subsets $s$ and $t$ of a type $\alpha$, the range of the embedding from the disjoint union $s \sqcup t$ to $\alpha$ is equal to the union $s \cup t$.

Function.Embedding.sigmaSet definition

{s : ι → Set α} (h : Pairwise (Disjoint on s)) : (i : ι) × s i ↪ α

Full source

/-- For an indexed family `s : ι → Set α` of disjoint sets,
the natural injection from the sigma-type `(i : ι) × ↑(s i)` to `α`. -/
@[simps] def Function.Embedding.sigmaSet {s : ι → Set α} (h : Pairwise (DisjointDisjoint on s)) :
    (i : ι) × s i(i : ι) × s i ↪ α where
  toFun x := x.2.1
  inj' := by
    rintro ⟨i, x, hx⟩ ⟨j, -, hx'⟩ rfl
    obtain rfl : i = j := h.eq (not_disjoint_iff.2 ⟨_, hx, hx'⟩)
    rfl

Embedding of a disjoint indexed family of sets into the base type

Informal description

Given an indexed family of sets $ s : \iota \to \mathcal{P}(\alpha) $ that are pairwise disjoint, the embedding $ \Sigma (i : \iota), s(i) \hookrightarrow \alpha $ maps each pair $(i, x)$ where $x \in s(i)$ to the element $x$ in $\alpha$. This is well-defined because the disjointness condition ensures that each element $x$ in $\alpha$ belongs to at most one set $s(i)$, making the embedding injective.

Function.Embedding.coe_sigmaSet theorem

{s : ι → Set α} (h) : (Function.Embedding.sigmaSet h : ((i : ι) × s i) → α) = fun x ↦ x.2.1

Full source

@[norm_cast] lemma Function.Embedding.coe_sigmaSet {s : ι → Set α} (h) :
    (Function.Embedding.sigmaSet h : ((i : ι) × s i) → α) = fun x ↦ x.2.1 := rfl

Embedding of Disjoint Union via Projection

Informal description

For any indexed family of sets $ s : \iota \to \mathcal{P}(\alpha) $ with pairwise disjoint sets, the embedding $\text{sigmaSet}\, h$ from the dependent sum type $\Sigma (i : \iota), s(i)$ to $\alpha$ is given by the projection $(i, x) \mapsto x$.

Function.Embedding.sigmaSet_preimage theorem

 {s : ι → Set α} (h : Pairwise (Disjoint on s)) (i : ι) (r : Set α) :
  Sigma.mk i ⁻¹' (Function.Embedding.sigmaSet h ⁻¹' r) = r ∩ s i

Full source

@[simp] theorem Function.Embedding.sigmaSet_preimage {s : ι → Set α}
    (h : Pairwise (DisjointDisjoint on s)) (i : ι) (r : Set α) :
    Sigma.mkSigma.mk i ⁻¹' (Function.Embedding.sigmaSet h ⁻¹' r) = r ∩ s i := by
  simp [Set.ext_iff]

Preimage of Set under Sigma Embedding Equals Intersection with Component Set

Informal description

Let $\{s_i\}_{i \in \iota}$ be a family of pairwise disjoint subsets of $\alpha$, and let $h$ be the proof of their pairwise disjointness. For any index $i \in \iota$ and any subset $r \subseteq \alpha$, the preimage of $r$ under the embedding $\text{sigmaSet}\, h$ composed with the injection $\Sigma.mk\, i$ equals the intersection $r \cap s_i$. In other words: \[ (\Sigma.mk\, i)^{-1} \circ (\text{sigmaSet}\, h)^{-1}(r) = r \cap s_i. \]

Function.Embedding.sigmaSet_range theorem

{s : ι → Set α} (h : Pairwise (Disjoint on s)) : Set.range (Function.Embedding.sigmaSet h) = ⋃ i, s i

Full source

@[simp] theorem Function.Embedding.sigmaSet_range {s : ι → Set α}
    (h : Pairwise (DisjointDisjoint on s)) : Set.range (Function.Embedding.sigmaSet h) = ⋃ i, s i := by
  simp [Set.ext_iff]

Range of Sigma Embedding Equals Union of Disjoint Sets

Informal description

Given an indexed family of sets $\{s_i\}_{i \in \iota}$ in $\alpha$ that are pairwise disjoint, the range of the embedding $\text{sigmaSet}\, h$ is equal to the union $\bigcup_{i \in \iota} s_i$.