Module docstring
{"# Injective functions "}
Function.Embedding
structure
(α : Sort*) (β : Sort*)
Informal description
The structure `α ↪ β` represents a bundled injective function from type `α` to type `β`.
Function.term_↪_
definition
: Lean.TrailingParserDescr✝
Informal description
The notation `↪` represents an embedding, which is a bundled injective function between two types. For types $\alpha$ and $\beta$, the notation $\alpha \hookrightarrow \beta$ denotes an injective function from $\alpha$ to $\beta$.
Function.instFunLikeEmbedding
instance
{α : Sort u} {β : Sort v} : FunLike (α ↪ β) α β
Full source
instance {α : Sort u} {β : Sort v} : FunLike (α ↪ β) α β where
coe := Embedding.toFun
coe_injective' f g h := by { cases f; cases g; congr }Informal description
For any types $\alpha$ and $\beta$, the type $\alpha \hookrightarrow \beta$ of injective function embeddings from $\alpha$ to $\beta$ has a function-like structure, where each embedding can be treated as a function from $\alpha$ to $\beta$.
Function.instEmbeddingLikeEmbedding
instance
{α : Sort u} {β : Sort v} : EmbeddingLike (α ↪ β) α β
Full source
instance {α : Sort u} {β : Sort v} : EmbeddingLike (α ↪ β) α β where
injective' := Embedding.inj'Informal description
For any types $\alpha$ and $\beta$, the type $\alpha \hookrightarrow \beta$ of injective function embeddings from $\alpha$ to $\beta$ satisfies the properties of an `EmbeddingLike` structure. This means that every embedding $f : \alpha \hookrightarrow \beta$ is an injective function, and for any $x, y \in \alpha$, we have $f(x) = f(y)$ if and only if $x = y$.
Function.instCanLiftForallEmbeddingCoeInjective
instance
{α β : Sort*} : CanLift (α → β) (α ↪ β) (↑) Injective
Full source
instance {α β : Sort*} : CanLift (α → β) (α ↪ β) (↑) Injective where prf f hf := ⟨⟨f, hf⟩, rfl⟩Informal description
For any types $\alpha$ and $\beta$, the type of functions $\alpha \to \beta$ can be lifted to the type of injective embeddings $\alpha \hookrightarrow \beta$ under the condition that the function is injective. Here, the lifting function is the canonical inclusion of embeddings into functions.
Function.exists_surjective_iff
theorem
{α β : Sort*} : (∃ f : α → β, Surjective f) ↔ Nonempty (α → β) ∧ Nonempty (β ↪ α)
Full source
theorem exists_surjective_iff {α β : Sort*} :
(∃ f : α → β, Surjective f) ↔ Nonempty (α → β) ∧ Nonempty (β ↪ α) :=
⟨fun ⟨f, h⟩ ↦ ⟨⟨f⟩, ⟨⟨_, injective_surjInv h⟩⟩⟩, fun ⟨h, ⟨e⟩⟩ ↦ (nonempty_fun.mp h).elim
(fun _ ↦ ⟨isEmptyElim, (isEmptyElim <| e ·)⟩) fun _ ↦ ⟨_, invFun_surjective e.inj'⟩⟩Informal description
For any types $\alpha$ and $\beta$, there exists a surjective function from $\alpha$ to $\beta$ if and only if there exists at least one function from $\alpha$ to $\beta$ and there exists at least one injective function from $\beta$ to $\alpha$.
Function.instCanLiftForallEmbeddingCoeInjective_1
instance
{α β : Sort*} : CanLift (α → β) (α ↪ β) (↑) Injective
Full source
instance {α β : Sort*} : CanLift (α → β) (α ↪ β) (↑) Injective where
prf _ h := ⟨⟨_, h⟩, rfl⟩Informal description
For any types $\alpha$ and $\beta$, the type of functions $\alpha \to \beta$ can be lifted to the type of injective embeddings $\alpha \hookrightarrow \beta$ under the condition that the function is injective. Here, the lifting function is the canonical inclusion of embeddings into functions.
Equiv.toEmbedding
definition
: α ↪ β
Full source
/-- Convert an `α ≃ β` to `α ↪ β`.
This is also available as a coercion `Equiv.coeEmbedding`.
The explicit `Equiv.toEmbedding` version is preferred though, since the coercion can have issues
inferring the type of the resulting embedding. For example:
```lean
-- Works:
example (s : Finset (Fin 3)) (f : Equiv.Perm (Fin 3)) : s.map f.toEmbedding = s.map f := by simp
-- Error, `f` has type `Fin 3 ≃ Fin 3` but is expected to have type `Fin 3 ↪ ?m_1 : Type ?`
example (s : Finset (Fin 3)) (f : Equiv.Perm (Fin 3)) : s.map f = s.map f.toEmbedding := by simp
```
-/
protected def Equiv.toEmbedding : α ↪ β :=
⟨f, f.injective⟩Informal description
Given an equivalence (bijection) $f$ between types $\alpha$ and $\beta$, this function converts it into an injective function embedding from $\alpha$ to $\beta$. The resulting embedding has the same underlying function as $f$ and inherits its injectivity property.
Equiv.coe_toEmbedding
theorem
: (f.toEmbedding : α → β) = f
Full source
@[simp]
theorem Equiv.coe_toEmbedding : (f.toEmbedding : α → β) = f :=
rflInformal description
For any equivalence (bijection) $f$ between types $\alpha$ and $\beta$, the underlying function of the injective embedding $f.\text{toEmbedding}$ is equal to $f$ itself, i.e., $(f.\text{toEmbedding} : \alpha \to \beta) = f$.
Equiv.toEmbedding_apply
theorem
(a : α) : f.toEmbedding a = f a
Full source
theorem Equiv.toEmbedding_apply (a : α) : f.toEmbedding a = f a :=
rflInformal description
For any element $a$ of type $\alpha$, the application of the injective embedding derived from an equivalence $f$ to $a$ is equal to the application of $f$ to $a$, i.e., $f.\text{toEmbedding}(a) = f(a)$.
Equiv.toEmbedding_injective
theorem
: Function.Injective (Equiv.toEmbedding : (α ≃ β) → (α ↪ β))
Full source
theorem Equiv.toEmbedding_injective : Function.Injective (Equiv.toEmbedding : (α ≃ β) → (α ↪ β)) :=
fun _ _ h ↦ by rwa [DFunLike.ext'_iff] at h ⊢Informal description
The function `Equiv.toEmbedding`, which maps an equivalence (bijection) between types $\alpha$ and $\beta$ to its corresponding injective embedding, is itself injective. That is, if two equivalences $f$ and $g$ from $\alpha$ to $\beta$ satisfy $f.\text{toEmbedding} = g.\text{toEmbedding}$, then $f = g$.
Equiv.coeEmbedding
instance
: Coe (α ≃ β) (α ↪ β)
Full source
instance Equiv.coeEmbedding : Coe (α ≃ β) (α ↪ β) :=
⟨Equiv.toEmbedding⟩Informal description
Every equivalence (bijection) between types $\alpha$ and $\beta$ can be viewed as an injective function embedding from $\alpha$ to $\beta$.
Equiv.Perm.coeEmbedding
abbrev
: Coe (Equiv.Perm α) (α ↪ α)
Full source
@[instance] abbrev Equiv.Perm.coeEmbedding : Coe (Equiv.Perm α) (α ↪ α) :=
Equiv.coeEmbeddingInformal description
Every permutation (bijective self-map) of a type $\alpha$ can be viewed as an injective function embedding from $\alpha$ to itself.
Function.Embedding.coe_injective
theorem
{α β} : @Injective (α ↪ β) (α → β) (fun f ↦ ↑f)
Full source
theorem coe_injective {α β} : @Injective (α ↪ β) (α → β) (fun f ↦ ↑f) :=
DFunLike.coe_injectiveInformal description
For any types $\alpha$ and $\beta$, the canonical coercion map from the type of injective function embeddings $\alpha \hookrightarrow \beta$ to the type of functions $\alpha \to \beta$ is injective. That is, if two embeddings $f, g : \alpha \hookrightarrow \beta$ satisfy $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.
Function.Embedding.ext
theorem
{α β} {f g : Embedding α β} (h : ∀ x, f x = g x) : f = g
Full source
@[ext]
theorem ext {α β} {f g : Embedding α β} (h : ∀ x, f x = g x) : f = g :=
DFunLike.ext f g hInformal description
For any two injective function embeddings $f, g : \alpha \hookrightarrow \beta$, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.
Function.Embedding.instUniqueOfIsEmpty
instance
{α β : Sort*} [IsEmpty α] : Unique (α ↪ β)
Full source
instance {α β : Sort*} [IsEmpty α] : Unique (α ↪ β) where
default := ⟨isEmptyElim, Function.injective_of_subsingleton _⟩
uniq := by intro; ext v; exact isEmptyElim vInformal description
For any types $\alpha$ and $\beta$, if $\alpha$ is empty, then there exists a unique injective function embedding from $\alpha$ to $\beta$.
Function.Embedding.toFun_eq_coe
theorem
{α β} (f : α ↪ β) : toFun f = f
Full source
@[simp]
theorem toFun_eq_coe {α β} (f : α ↪ β) : toFun f = f :=
rflInformal description
For any injective function embedding $f : \alpha \hookrightarrow \beta$, the underlying function `toFun f` is equal to $f$ itself.
Function.Embedding.coeFn_mk
theorem
{α β} (f : α → β) (i) : (@mk _ _ f i : α → β) = f
Informal description
For any function $f : \alpha \to \beta$ and proof $i$ that $f$ is injective, the underlying function of the embedding $\langle f, i \rangle : \alpha \hookrightarrow \beta$ is equal to $f$.
Function.Embedding.mk_coe
theorem
{α β : Type*} (f : α ↪ β) (inj) : (⟨f, inj⟩ : α ↪ β) = f
Informal description
For any injective function embedding $f : \alpha \hookrightarrow \beta$ and proof `inj` that $f$ is injective, the constructed embedding $\langle f, \text{inj} \rangle$ is equal to $f$.
Function.Embedding.injective
theorem
{α β} (f : α ↪ β) : Injective f
Full source
protected theorem injective {α β} (f : α ↪ β) : Injective f :=
EmbeddingLike.injective fInformal description
For any injective function embedding $f \colon \alpha \hookrightarrow \beta$, the function $f$ is injective. That is, for any $x, y \in \alpha$, if $f(x) = f(y)$, then $x = y$.
Function.Embedding.apply_eq_iff_eq
theorem
{α β} (f : α ↪ β) (x y : α) : f x = f y ↔ x = y
Full source
theorem apply_eq_iff_eq {α β} (f : α ↪ β) (x y : α) : f x = f y ↔ x = y :=
EmbeddingLike.apply_eq_iff_eq fInformal description
For any injective function embedding $f \colon \alpha \hookrightarrow \beta$ and any elements $x, y \in \alpha$, we have $f(x) = f(y)$ if and only if $x = y$.
Function.Embedding.refl
definition
(α : Sort*) : α ↪ α
Full source
/-- The identity map as a `Function.Embedding`. -/
@[refl, simps +simpRhs]
protected def refl (α : Sort*) : α ↪ α :=
⟨id, injective_id⟩Informal description
The identity function $\mathrm{id} : \alpha \to \alpha$ is an injective function embedding from $\alpha$ to itself.
Function.Embedding.trans
definition
{α β γ} (f : α ↪ β) (g : β ↪ γ) : α ↪ γ
Informal description
The composition of two injective function embeddings \( f : \alpha \hookrightarrow \beta \) and \( g : \beta \hookrightarrow \gamma \) is the injective function embedding \( g \circ f : \alpha \hookrightarrow \gamma \).
Function.Embedding.instTrans
instance
: Trans Embedding Embedding Embedding
Informal description
The composition of injective function embeddings is transitive. That is, given injective embeddings $f \colon \alpha \hookrightarrow \beta$ and $g \colon \beta \hookrightarrow \gamma$, the composition $g \circ f \colon \alpha \hookrightarrow \gamma$ is also an injective embedding.
Function.Embedding.mk_id
theorem
{α} : mk id injective_id = .refl α
Informal description
For any type $\alpha$, the injective function embedding constructed from the identity function $\mathrm{id} : \alpha \to \alpha$ and its injectivity proof is equal to the identity embedding $\mathrm{refl} : \alpha \hookrightarrow \alpha$.
Function.Embedding.mk_trans_mk
theorem
{α β γ} (f : α → β) (g : β → γ) (hf hg) : (mk f hf).trans (mk g hg) = mk (g ∘ f) (hg.comp hf)
Informal description
For any types $\alpha$, $\beta$, $\gamma$ and functions $f \colon \alpha \to \beta$, $g \colon \beta \to \gamma$, if $f$ is injective (with proof $hf$) and $g$ is injective (with proof $hg$), then the composition of the embeddings $\mathrm{mk}(f, hf)$ and $\mathrm{mk}(g, hg)$ equals the embedding of the composition $g \circ f$ with its injectivity proof $hg \circ hf$. That is, $\mathrm{mk}(f, hf) \circ \mathrm{mk}(g, hg) = \mathrm{mk}(g \circ f, hg \circ hf)$.
Function.Embedding.equiv_toEmbedding_trans_symm_toEmbedding
theorem
{α β : Sort*} (e : α ≃ β) : e.toEmbedding.trans e.symm.toEmbedding = Embedding.refl _
Full source
@[simp]
theorem equiv_toEmbedding_trans_symm_toEmbedding {α β : Sort*} (e : α ≃ β) :
e.toEmbedding.trans e.symm.toEmbedding = Embedding.refl _ := by
ext
simpInformal description
For any types $\alpha$ and $\beta$ and any equivalence (bijection) $e : \alpha \simeq \beta$, the composition of the embedding $e \colon \alpha \hookrightarrow \beta$ with its symmetric embedding $e^{-1} \colon \beta \hookrightarrow \alpha$ is equal to the identity embedding on $\alpha$.
Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding
theorem
{α β : Sort*} (e : α ≃ β) : e.symm.toEmbedding.trans e.toEmbedding = Embedding.refl _
Full source
@[simp]
theorem equiv_symm_toEmbedding_trans_toEmbedding {α β : Sort*} (e : α ≃ β) :
e.symm.toEmbedding.trans e.toEmbedding = Embedding.refl _ := by
ext
simpInformal description
For any equivalence (bijection) $e$ between types $\alpha$ and $\beta$, the composition of the embedding induced by the inverse equivalence $e^{-1}$ with the embedding induced by $e$ is equal to the identity embedding on $\beta$.
Function.Embedding.congr
definition
{α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α ≃ β) (e₂ : γ ≃ δ) (f : α ↪ γ) : β ↪ δ
Full source
/-- Transfer an embedding along a pair of equivalences. -/
@[simps! -fullyApplied +simpRhs]
protected def congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α ≃ β) (e₂ : γ ≃ δ)
(f : α ↪ γ) : β ↪ δ :=
(Equiv.toEmbedding e₁.symm).trans (f.trans e₂.toEmbedding)Informal description
Given equivalences (bijections) $e₁ : α ≃ β$ and $e₂ : γ ≃ δ$, and an injective function embedding $f : α ↪ γ$, this constructs an injective function embedding from $β$ to $δ$ by composing the inverse of $e₁$, $f$, and $e₂$.
Function.Embedding.ofSurjective
definition
{α β} (f : β → α) (hf : Surjective f) : α ↪ β
Full source
/-- A right inverse `surjInv` of a surjective function as an `Embedding`. -/
protected noncomputable def ofSurjective {α β} (f : β → α) (hf : Surjective f) : α ↪ β :=
⟨surjInv hf, injective_surjInv _⟩Informal description
Given a surjective function \( f : \beta \to \alpha \), the function `Function.Embedding.ofSurjective` constructs an injective function embedding \( \alpha \hookrightarrow \beta \) using the right inverse of \( f \).
Function.Embedding.equivOfSurjective
definition
{α β} (f : α ↪ β) (hf : Surjective f) : α ≃ β
Full source
/-- Convert a surjective `Embedding` to an `Equiv` -/
protected noncomputable def equivOfSurjective {α β} (f : α ↪ β) (hf : Surjective f) : α ≃ β :=
Equiv.ofBijective f ⟨f.injective, hf⟩Informal description
Given an injective function embedding \( f : \alpha \hookrightarrow \beta \) that is also surjective, construct an equivalence (bijection) between \( \alpha \) and \( \beta \).
Function.Embedding.ofIsEmpty
definition
{α β} [IsEmpty α] : α ↪ β
Full source
/-- There is always an embedding from an empty type. -/
protected def ofIsEmpty {α β} [IsEmpty α] : α ↪ β :=
⟨isEmptyElim, isEmptyElim⟩Informal description
For any empty type $\alpha$ and any type $\beta$, there exists an injective function (embedding) from $\alpha$ to $\beta$. This is constructed using the elimination principle for empty types.
Function.Embedding.setValue
definition
{α β : Sort*} (f : α ↪ β) (a : α) (b : β) [∀ a', Decidable (a' = a)] [∀ a', Decidable (f a' = b)] : α ↪ β
Full source
/-- Change the value of an embedding `f` at one point. If the prescribed image
is already occupied by some `f a'`, then swap the values at these two points. -/
def setValue {α β : Sort*} (f : α ↪ β) (a : α) (b : β) [∀ a', Decidable (a' = a)]
[∀ a', Decidable (f a' = b)] : α ↪ β :=
⟨fun a' => if a' = a then b else if f a' = b then f a else f a', by
intro x y (h : ite _ _ _ = ite _ _ _)
split_ifs at h <;> (try subst b) <;> (try simp only [f.injective.eq_iff] at *) <;> cc⟩Informal description
Given an injective function embedding \( f : \alpha \hookrightarrow \beta \), a point \( a \in \alpha \), and a value \( b \in \beta \), this constructs a new embedding that maps \( a \) to \( b \). If \( b \) is already in the image of \( f \) at some point \( a' \), then the values at \( a \) and \( a' \) are swapped. The resulting function remains injective.
Function.Embedding.setValue_eq
theorem
{α β} (f : α ↪ β) (a : α) (b : β) [∀ a', Decidable (a' = a)] [∀ a', Decidable (f a' = b)] : setValue f a b a = b
Informal description
Given an injective function $f \colon \alpha \hookrightarrow \beta$, a point $a \in \alpha$, and a value $b \in \beta$, the modified function $\text{setValue}(f, a, b)$ satisfies $\text{setValue}(f, a, b)(a) = b$.
Function.Embedding.setValue_eq_iff
theorem
{α β} (f : α ↪ β) {a a' : α} {b : β} [∀ a', Decidable (a' = a)] [∀ a', Decidable (f a' = b)] :
setValue f a b a' = b ↔ a' = a
Full source
@[simp]
theorem setValue_eq_iff {α β} (f : α ↪ β) {a a' : α} {b : β} [∀ a', Decidable (a' = a)]
[∀ a', Decidable (f a' = b)] : setValuesetValue f a b a' = b ↔ a' = a :=
(setValue f a b).injective.eq_iff' <| setValue_eq ..Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an injective function, and let $a, a' \in \alpha$ and $b \in \beta$. Then the modified function $\text{setValue}(f, a, b)$ satisfies $\text{setValue}(f, a, b)(a') = b$ if and only if $a' = a$.
Function.Embedding.setValue_eq_of_ne
theorem
{α β} {f : α ↪ β} {a : α} {b : β} {c : α} [∀ a', Decidable (a' = a)] [∀ a', Decidable (f a' = b)] (hc : c ≠ a)
(hb : f c ≠ b) : setValue f a b c = f c
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an injective function, $a, c \in \alpha$ with $c \neq a$, and $b \in \beta$ with $f(c) \neq b$. Then the modified function $\text{setValue}(f, a, b)$ satisfies $\text{setValue}(f, a, b)(c) = f(c)$.
Function.Embedding.setValue_right_apply_eq
theorem
{α β} (f : α ↪ β) (a c : α) [∀ a', Decidable (a' = a)] [∀ a', Decidable (f a' = f c)] : setValue f a (f c) c = f a
Informal description
Let $f \colon \alpha \hookrightarrow \beta$ be an injective function, and let $a, c \in \alpha$. Then the modified function $\text{setValue}(f, a, f(c))$ satisfies $\text{setValue}(f, a, f(c))(c) = f(a)$.
Function.Embedding.some
definition
{α} : α ↪ Option α
Full source
/-- Embedding into `Option α` using `some`. -/
@[simps -fullyApplied]
protected def some {α} : α ↪ Option α :=
⟨some, Option.some_injective α⟩Informal description
The embedding of a type $\alpha$ into $\operatorname{Option} \alpha$ via the $\operatorname{some}$ constructor. This is an injective function that maps each element $x \in \alpha$ to $\operatorname{some}(x) \in \operatorname{Option} \alpha$.
Function.Embedding.optionMap
definition
{α β} (f : α ↪ β) : Option α ↪ Option β
Full source
/-- A version of `Option.map` for `Function.Embedding`s. -/
@[simps -fullyApplied]
def optionMap {α β} (f : α ↪ β) : OptionOption α ↪ Option β :=
⟨Option.map f, Option.map_injective f.injective⟩Informal description
Given an injective function embedding $f \colon \alpha \hookrightarrow \beta$, the function $\operatorname{optionMap} f$ maps an element of $\operatorname{Option} \alpha$ to $\operatorname{Option} \beta$ by applying $f$ to the underlying value when it exists (i.e., $\operatorname{some} x \mapsto \operatorname{some} (f x)$) and preserving $\operatorname{none}$. This operation preserves injectivity.
Function.Embedding.subtype
definition
{α} (p : α → Prop) : Subtype p ↪ α
Full source
/-- Embedding of a `Subtype`. -/
def subtype {α} (p : α → Prop) : SubtypeSubtype p ↪ α :=
⟨Subtype.val, fun _ _ => Subtype.ext⟩Informal description
The embedding of a subtype $\{x \in \alpha \mid p(x)\}$ into the original type $\alpha$ via the inclusion map, which is injective. Specifically, it maps each element $x$ of the subtype to its underlying value in $\alpha$.
Function.Embedding.subtype_apply
theorem
{α} {p : α → Prop} (x : Subtype p) : subtype p x = x
Full source
@[simp]
theorem subtype_apply {α} {p : α → Prop} (x : Subtype p) : subtype p x = x :=
rflInformal description
For any type $\alpha$ and predicate $p : \alpha \to \mathrm{Prop}$, if $x$ is an element of the subtype $\{x \in \alpha \mid p(x)\}$, then the application of the subtype inclusion embedding to $x$ equals $x$ itself.
Function.Embedding.subtype_injective
theorem
{α} (p : α → Prop) : Function.Injective (subtype p)
Full source
theorem subtype_injective {α} (p : α → Prop) : Function.Injective (subtype p) :=
Subtype.coe_injectiveInformal description
For any type $\alpha$ and predicate $p : \alpha \to \mathrm{Prop}$, the inclusion map from the subtype $\{x \in \alpha \mid p(x)\}$ to $\alpha$ is injective. That is, if $x, y$ are elements of the subtype and $x = y$ as elements of $\alpha$, then $x = y$ in the subtype.
Function.Embedding.coe_subtype
theorem
{α} (p : α → Prop) : ↑(subtype p) = Subtype.val
Full source
@[simp]
theorem coe_subtype {α} (p : α → Prop) : ↑(subtype p) = Subtype.val :=
rflInformal description
For any type $\alpha$ and predicate $p : \alpha \to \mathrm{Prop}$, the underlying function of the subtype inclusion embedding $\{x \in \alpha \mid p(x)\} \hookrightarrow \alpha$ is equal to the canonical projection $\mathrm{Subtype.val}$ from the subtype to $\alpha$.
Function.Embedding.quotientOut
definition
(α) [s : Setoid α] : Quotient s ↪ α
Full source
/-- `Quotient.out` as an embedding. -/
noncomputable def quotientOut (α) [s : Setoid α] : QuotientQuotient s ↪ α :=
⟨_, Quotient.out_injective⟩Informal description
The function `Quotient.out` viewed as an injective embedding from the quotient type `Quotient s` back to the original type `α`, where `s` is a setoid (an equivalence relation) on `α`.
Function.Embedding.coe_quotientOut
theorem
(α) [Setoid α] : ↑(quotientOut α) = Quotient.out
Full source
@[simp]
theorem coe_quotientOut (α) [Setoid α] : ↑(quotientOut α) = Quotient.out :=
rflInformal description
For any type $\alpha$ with a setoid (equivalence relation) $s$, the underlying function of the injective embedding `quotientOut` from the quotient type $\alpha/s$ to $\alpha$ is equal to the quotient out function $\operatorname{Quotient.out}$.
Function.Embedding.punit
definition
{β : Sort*} (b : β) : PUnit ↪ β
Full source
/-- Choosing an element `b : β` gives an embedding of `PUnit` into `β`. -/
def punit {β : Sort*} (b : β) : PUnitPUnit ↪ β :=
⟨fun _ => b, by
rintro ⟨⟩ ⟨⟩ _
rfl⟩Informal description
Given an element $b$ of type $\beta$, the function maps the unique element of the unit type $\text{PUnit}$ to $b$, forming an injective embedding from $\text{PUnit}$ into $\beta$.
Function.Embedding.sectL
definition
(α : Sort _) {β : Sort _} (b : β) : α ↪ α × β
Full source
/-- Fixing an element `b : β` gives an embedding `α ↪ α × β`. -/
@[simps]
def sectL (α : Sort _) {β : Sort _} (b : β) : α ↪ α × β :=
⟨fun a => (a, b), fun _ _ h => congr_arg Prod.fst h⟩Informal description
Given an element $b$ of type $\beta$, the function maps an element $a$ of type $\alpha$ to the pair $(a, b)$, forming an injective embedding from $\alpha$ into the product type $\alpha \times \beta$.
Function.Embedding.sectR
definition
{α : Sort _} (a : α) (β : Sort _) : β ↪ α × β
Full source
/-- Fixing an element `a : α` gives an embedding `β ↪ α × β`. -/
@[simps]
def sectR {α : Sort _} (a : α) (β : Sort _) : β ↪ α × β :=
⟨fun b => (a, b), fun _ _ h => congr_arg Prod.snd h⟩Informal description
Given an element $a$ of type $\alpha$, the function maps an element $b$ of type $\beta$ to the pair $(a, b)$, forming an injective embedding from $\beta$ into the product type $\alpha \times \beta$.
Function.Embedding.prodMap
definition
{α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α × γ ↪ β × δ
Full source
/-- If `e₁` and `e₂` are embeddings, then so is `Prod.map e₁ e₂ : (a, b) ↦ (e₁ a, e₂ b)`. -/
def prodMap {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α × γα × γ ↪ β × δ :=
⟨Prod.map e₁ e₂, e₁.injective.prodMap e₂.injective⟩Informal description
Given injective functions \( e_1: \alpha \hookrightarrow \beta \) and \( e_2: \gamma \hookrightarrow \delta \), the function \( \text{prodMap}\ e_1\ e_2 \) maps pairs \((a, c)\) in \(\alpha \times \gamma\) to pairs \((e_1(a), e_2(c))\) in \(\beta \times \delta\), and is itself injective.
Function.Embedding.coe_prodMap
theorem
{α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : e₁.prodMap e₂ = Prod.map e₁ e₂
Informal description
For any types $\alpha, \beta, \gamma, \delta$ and injective functions $e_1: \alpha \hookrightarrow \beta$, $e_2: \gamma \hookrightarrow \delta$, the embedding $e_1.\text{prodMap}\ e_2$ is equal to the product map $\text{Prod.map}\ e_1\ e_2$ that applies $e_1$ to the first component and $e_2$ to the second component of pairs in $\alpha \times \gamma$.
Function.Embedding.pprodMap
definition
{α β γ δ : Sort*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : PProd α γ ↪ PProd β δ
Full source
/-- If `e₁` and `e₂` are embeddings,
then so is `fun ⟨a, b⟩ ↦ ⟨e₁ a, e₂ b⟩ : PProd α γ → PProd β δ`. -/
def pprodMap {α β γ δ : Sort*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : PProdPProd α γ ↪ PProd β δ :=
⟨fun x => ⟨e₁ x.1, e₂ x.2⟩, e₁.injective.pprod_map e₂.injective⟩Informal description
Given injective functions $e_1: \alpha \hookrightarrow \beta$ and $e_2: \gamma \hookrightarrow \delta$, the function $\text{pprodMap}\ e_1\ e_2$ maps elements of the product type $\alpha \times \gamma$ to the product type $\beta \times \delta$ by applying $e_1$ to the first component and $e_2$ to the second component, and is itself injective.
Function.Embedding.sumMap
definition
{α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α ⊕ γ ↪ β ⊕ δ
Full source
/-- If `e₁` and `e₂` are embeddings, then so is `Sum.map e₁ e₂`. -/
def sumMap {α β γ δ : Type*} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : α ⊕ γα ⊕ γ ↪ β ⊕ δ :=
⟨Sum.map e₁ e₂, e₁.injective.sumMap e₂.injective⟩Informal description
Given injective functions $e_1: \alpha \hookrightarrow \beta$ and $e_2: \gamma \hookrightarrow \delta$, the function $\text{sumMap}\ e_1\ e_2$ maps elements of the sum type $\alpha \oplus \gamma$ to the sum type $\beta \oplus \delta$ by applying $e_1$ to left components and $e_2$ to right components, and is itself injective.
Function.Embedding.coe_sumMap
theorem
{α β γ δ} (e₁ : α ↪ β) (e₂ : γ ↪ δ) : sumMap e₁ e₂ = Sum.map e₁ e₂
Informal description
For any types $\alpha, \beta, \gamma, \delta$ and injective embeddings $e_1: \alpha \hookrightarrow \beta$ and $e_2: \gamma \hookrightarrow \delta$, the injective embedding $\text{sumMap}\ e_1\ e_2$ is equal to the sum map $\text{Sum.map}\ e_1\ e_2$ of the underlying functions.
Function.Embedding.inl
definition
{α β : Type*} : α ↪ α ⊕ β
Full source
/-- The embedding of `α` into the sum `α ⊕ β`. -/
@[simps]
def inl {α β : Type*} : α ↪ α ⊕ β :=
⟨Sum.inl, fun _ _ => Sum.inl.inj⟩Informal description
The function embeds an element of type $\alpha$ into the left component of the sum type $\alpha \oplus \beta$. It is injective, meaning that if two elements of $\alpha$ are mapped to the same element in $\alpha \oplus \beta$, then they must be equal.
Function.Embedding.inr
definition
{α β : Type*} : β ↪ α ⊕ β
Full source
/-- The embedding of `β` into the sum `α ⊕ β`. -/
@[simps]
def inr {α β : Type*} : β ↪ α ⊕ β :=
⟨Sum.inr, fun _ _ => Sum.inr.inj⟩Informal description
The function embeds an element of type $\beta$ into the right component of the sum type $\alpha \oplus \beta$. It is injective, meaning that if two elements of $\beta$ are mapped to the same element in $\alpha \oplus \beta$, then they must be equal.
Function.Embedding.sigmaMk
definition
(a : α) : β a ↪ Σ x, β x
Full source
/-- `Sigma.mk` as a `Function.Embedding`. -/
@[simps apply]
def sigmaMk (a : α) : β a ↪ Σx, β x :=
⟨Sigma.mk a, sigma_mk_injective⟩Informal description
For a fixed element $a$ of type $\alpha$, the function embeds an element of type $\beta a$ into the dependent pair type $\Sigma x, \beta x$ by constructing the pair $(a, b)$ for any $b \in \beta a$. This embedding is injective, meaning that if $(a, b_1) = (a, b_2)$ as elements of $\Sigma x, \beta x$, then $b_1 = b_2$.
Function.Embedding.sigmaMap
definition
(f : α ↪ α') (g : ∀ a, β a ↪ β' (f a)) : (Σ a, β a) ↪ Σ a', β' a'
Full source
/-- If `f : α ↪ α'` is an embedding and `g : Π a, β α ↪ β' (f α)` is a family
of embeddings, then `Sigma.map f g` is an embedding. -/
@[simps apply]
def sigmaMap (f : α ↪ α') (g : ∀ a, β a ↪ β' (f a)) : (Σa, β a) ↪ Σa', β' a' :=
⟨Sigma.map f fun a => g a, f.injective.sigma_map fun a => (g a).injective⟩Informal description
Given an injective function $f: \alpha \hookrightarrow \alpha'$ and a family of injective functions $g_a: \beta(a) \hookrightarrow \beta'(f(a))$ for each $a \in \alpha$, the function $\Sigma.\text{map}\, f\, g$ is an injective function from the dependent pair type $\Sigma a, \beta(a)$ to $\Sigma a', \beta'(a')$.
Function.Embedding.piCongrRight
definition
{α : Sort*} {β γ : α → Sort*} (e : ∀ a, β a ↪ γ a) : (∀ a, β a) ↪ ∀ a, γ a
Full source
/-- Define an embedding `(Π a : α, β a) ↪ (Π a : α, γ a)` from a family of embeddings
`e : Π a, (β a ↪ γ a)`. This embedding sends `f` to `fun a ↦ e a (f a)`. -/
@[simps]
def piCongrRight {α : Sort*} {β γ : α → Sort*} (e : ∀ a, β a ↪ γ a) : (∀ a, β a) ↪ ∀ a, γ a :=
⟨fun f a => e a (f a), fun _ _ h => funext fun a => (e a).injective (congr_fun h a)⟩Informal description
Given a family of injective embeddings $e_a : \beta(a) \hookrightarrow \gamma(a)$ for each $a \in \alpha$, the function $\text{piCongrRight}\, e$ is an injective embedding from the dependent function type $\Pi a, \beta(a)$ to $\Pi a, \gamma(a)$. It maps a function $f$ to the function $\lambda a, e_a (f(a))$.
Function.Embedding.arrowCongrRight
definition
{α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) : (γ → α) ↪ γ → β
Full source
/-- An embedding `e : α ↪ β` defines an embedding `(γ → α) ↪ (γ → β)` that sends each `f`
to `e ∘ f`. -/
def arrowCongrRight {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) : (γ → α) ↪ γ → β :=
piCongrRight fun _ => eInformal description
Given an injective function embedding $e : \alpha \hookrightarrow \beta$, the function $\text{arrowCongrRight}\, e$ is an injective embedding from the function space $\gamma \to \alpha$ to $\gamma \to \beta$. It maps a function $f : \gamma \to \alpha$ to the composition $e \circ f : \gamma \to \beta$.
Function.Embedding.arrowCongrRight_apply
theorem
{α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) (f : γ → α) : arrowCongrRight e f = e ∘ f
Full source
@[simp]
theorem arrowCongrRight_apply {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) (f : γ → α) :
arrowCongrRight e f = e ∘ f :=
rflInformal description
Given an injective function embedding $e : \alpha \hookrightarrow \beta$ and a function $f : \gamma \to \alpha$, the application of the embedding $\text{arrowCongrRight}\, e$ to $f$ is equal to the composition $e \circ f$.
Function.Embedding.arrowCongrLeft
definition
{α : Sort u} {β : Sort v} {γ : Sort w} [Inhabited γ] (e : α ↪ β) : (α → γ) ↪ β → γ
Full source
/-- An embedding `e : α ↪ β` defines an embedding `(α → γ) ↪ (β → γ)` for any inhabited type `γ`.
This embedding sends each `f : α → γ` to a function `g : β → γ` such that `g ∘ e = f` and
`g y = default` whenever `y ∉ range e`. -/
noncomputable def arrowCongrLeft {α : Sort u} {β : Sort v} {γ : Sort w} [Inhabited γ] (e : α ↪ β) :
(α → γ) ↪ β → γ :=
⟨fun f => extend e f default, fun f₁ f₂ h =>
funext fun x => by simpa only [e.injective.extend_apply] using congr_fun h (e x)⟩Informal description
Given an injective function embedding $e : \alpha \hookrightarrow \beta$ and an inhabited type $\gamma$, the function `arrowCongrLeft` constructs an embedding $(α → γ) \hookrightarrow (β → γ)$. For any $f : \alpha \to \gamma$, the resulting function $g : \beta \to \gamma$ satisfies $g \circ e = f$ and maps elements outside the range of $e$ to a default value in $\gamma$.
Function.Embedding.subtypeMap
definition
{α β} {p : α → Prop} {q : β → Prop} (f : α ↪ β) (h : ∀ ⦃x⦄, p x → q (f x)) : { x : α // p x } ↪ { y : β // q y }
Full source
/-- Restrict both domain and codomain of an embedding. -/
protected def subtypeMap {α β} {p : α → Prop} {q : β → Prop} (f : α ↪ β)
(h : ∀ ⦃x⦄, p x → q (f x)) :
{ x : α // p x }{ x : α // p x } ↪ { y : β // q y } :=
⟨Subtype.map f h, Subtype.map_injective h f.2⟩Informal description
Given an injective function embedding $f : \alpha \hookrightarrow \beta$ and predicates $p$ on $\alpha$ and $q$ on $\beta$ such that for any $x \in \alpha$, $p(x)$ implies $q(f(x))$, the function `subtypeMap` constructs an embedding from the subtype $\{x \in \alpha \mid p(x)\}$ to the subtype $\{y \in \beta \mid q(y)\}$ by restricting both the domain and codomain of $f$.
Function.Embedding.swap_apply
theorem
{α β : Type*} [DecidableEq α] [DecidableEq β] (f : α ↪ β) (x y z : α) :
Equiv.swap (f x) (f y) (f z) = f (Equiv.swap x y z)
Full source
theorem swap_apply {α β : Type*} [DecidableEq α] [DecidableEq β] (f : α ↪ β) (x y z : α) :
Equiv.swap (f x) (f y) (f z) = f (Equiv.swap x y z) :=
f.injective.swap_apply x y zInformal description
Let $\alpha$ and $\beta$ be types with decidable equality, and let $f \colon \alpha \hookrightarrow \beta$ be an injective function embedding. For any $x, y, z \in \alpha$, the swap of $f(x)$ and $f(y)$ applied to $f(z)$ equals $f$ applied to the swap of $x$ and $y$ applied to $z$. That is,
\[ \text{swap}(f(x), f(y))(f(z)) = f(\text{swap}(x, y)(z)). \]
Function.Embedding.swap_comp
theorem
{α β : Type*} [DecidableEq α] [DecidableEq β] (f : α ↪ β) (x y : α) : Equiv.swap (f x) (f y) ∘ f = f ∘ Equiv.swap x y
Full source
theorem swap_comp {α β : Type*} [DecidableEq α] [DecidableEq β] (f : α ↪ β) (x y : α) :
Equiv.swapEquiv.swap (f x) (f y) ∘ f = f ∘ Equiv.swap x y :=
f.injective.swap_comp x yInformal description
Let $\alpha$ and $\beta$ be types with decidable equality, and let $f \colon \alpha \hookrightarrow \beta$ be an injective function embedding. For any $x, y \in \alpha$, the composition of the swap permutation $\text{swap}(f(x), f(y))$ with $f$ is equal to the composition of $f$ with the swap permutation $\text{swap}(x, y)$. That is,
\[
\text{swap}(f(x), f(y)) \circ f = f \circ \text{swap}(x, y).
\]
Equiv.asEmbedding
definition
{β α : Sort*} {p : β → Prop} (e : α ≃ Subtype p) : α ↪ β
Full source
/-- Given an equivalence to a subtype, produce an embedding to the elements of the corresponding
set. -/
@[simps!]
def asEmbedding {β α : Sort*} {p : β → Prop} (e : α ≃ Subtype p) : α ↪ β :=
e.toEmbedding.trans (subtype p)Informal description
Given an equivalence (bijection) $e$ between a type $\alpha$ and a subtype $\{x \in \beta \mid p(x)\}$, this constructs an injective function embedding from $\alpha$ to $\beta$ by composing $e$ with the natural inclusion of the subtype into $\beta$.
Equiv.subtypeInjectiveEquivEmbedding
definition
(α β : Sort*) : { f : α → β // Injective f } ≃ (α ↪ β)
Full source
/-- The type of embeddings `α ↪ β` is equivalent to
the subtype of all injective functions `α → β`. -/
def subtypeInjectiveEquivEmbedding (α β : Sort*) :
{ f : α → β // Injective f }{ f : α → β // Injective f } ≃ (α ↪ β) where
toFun f := ⟨f.val, f.property⟩
invFun f := ⟨f, f.injective⟩
left_inv _ := rfl
right_inv _ := rflInformal description
The equivalence between the subtype of injective functions $\{ f : \alpha \to \beta \mid \text{Injective } f \}$ and the type of embeddings $\alpha \hookrightarrow \beta$.
Specifically:
- The forward direction maps an injective function $f$ to its bundled embedding form.
- The backward direction extracts the underlying injective function from an embedding.
- The equivalence is bijective, with both compositions yielding identity maps.
Equiv.embeddingCongr
definition
{α β γ δ : Sort*} (h : α ≃ β) (h' : γ ≃ δ) : (α ↪ γ) ≃ (β ↪ δ)
Full source
/-- If `α₁ ≃ α₂` and `β₁ ≃ β₂`, then the type of embeddings `α₁ ↪ β₁`
is equivalent to the type of embeddings `α₂ ↪ β₂`. -/
@[simps apply]
def embeddingCongr {α β γ δ : Sort*} (h : α ≃ β) (h' : γ ≃ δ) : (α ↪ γ) ≃ (β ↪ δ) where
toFun f := f.congr h h'
invFun f := f.congr h.symm h'.symm
left_inv x := by
ext
simp
right_inv x := by
ext
simpInformal description
Given equivalences (bijections) $h : \alpha \simeq \beta$ and $h' : \gamma \simeq \delta$, the type of embeddings $\alpha \hookrightarrow \gamma$ is equivalent to the type of embeddings $\beta \hookrightarrow \delta$. The equivalence is constructed by composing embeddings with the given equivalences and their inverses.
Equiv.embeddingCongr_refl
theorem
{α β : Sort*} : embeddingCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ↪ β)
Full source
@[simp]
theorem embeddingCongr_refl {α β : Sort*} :
embeddingCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ↪ β) :=
rflInformal description
For any types $\alpha$ and $\beta$, the equivalence `embeddingCongr` applied to the identity equivalences $\text{refl}_\alpha$ and $\text{refl}_\beta$ yields the identity equivalence on the type of embeddings $\alpha \hookrightarrow \beta$.
Equiv.embeddingCongr_trans
theorem
{α₁ β₁ α₂ β₂ α₃ β₃ : Sort*} (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :
embeddingCongr (e₁.trans e₂) (e₁'.trans e₂') = (embeddingCongr e₁ e₁').trans (embeddingCongr e₂ e₂')
Full source
@[simp]
theorem embeddingCongr_trans {α₁ β₁ α₂ β₂ α₃ β₃ : Sort*} (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂)
(e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :
embeddingCongr (e₁.trans e₂) (e₁'.trans e₂') =
(embeddingCongr e₁ e₁').trans (embeddingCongr e₂ e₂') :=
rflInformal description
For any types $\alpha_1, \alpha_2, \alpha_3$ and $\beta_1, \beta_2, \beta_3$, given equivalences $e_1 : \alpha_1 \simeq \alpha_2$, $e_1' : \beta_1 \simeq \beta_2$, $e_2 : \alpha_2 \simeq \alpha_3$, and $e_2' : \beta_2 \simeq \beta_3$, the equivalence of embedding types obtained by composing $e_1$ and $e_2$ for the domain and $e_1'$ and $e_2'$ for the codomain is equal to the composition of the individual embedding equivalences constructed from $e_1, e_1'$ and $e_2, e_2'$.
Equiv.embeddingCongr_symm
theorem
{α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) : (embeddingCongr e₁ e₂).symm = embeddingCongr e₁.symm e₂.symm
Full source
@[simp]
theorem embeddingCongr_symm {α₁ β₁ α₂ β₂ : Sort*} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :
(embeddingCongr e₁ e₂).symm = embeddingCongr e₁.symm e₂.symm :=
rflInformal description
For any types $\alpha_1, \alpha_2, \beta_1, \beta_2$, given equivalences $e_1 : \alpha_1 \simeq \alpha_2$ and $e_2 : \beta_1 \simeq \beta_2$, the inverse of the equivalence between embedding types $\alpha_1 \hookrightarrow \beta_1$ and $\alpha_2 \hookrightarrow \beta_2$ (induced by $e_1$ and $e_2$) is equal to the equivalence between $\alpha_2 \hookrightarrow \beta_2$ and $\alpha_1 \hookrightarrow \beta_1$ induced by the inverses of $e_1$ and $e_2$.
Equiv.embeddingCongr_apply_trans
theorem
{α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (ec : γ₁ ≃ γ₂) (f : α₁ ↪ β₁) (g : β₁ ↪ γ₁) :
Equiv.embeddingCongr ea ec (f.trans g) = (Equiv.embeddingCongr ea eb f).trans (Equiv.embeddingCongr eb ec g)
Full source
theorem embeddingCongr_apply_trans {α₁ β₁ γ₁ α₂ β₂ γ₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂)
(ec : γ₁ ≃ γ₂) (f : α₁ ↪ β₁) (g : β₁ ↪ γ₁) :
Equiv.embeddingCongr ea ec (f.trans g) =
(Equiv.embeddingCongr ea eb f).trans (Equiv.embeddingCongr eb ec g) := by
ext
simpInformal description
Given equivalences (bijections) $e_a : \alpha_1 \simeq \alpha_2$, $e_b : \beta_1 \simeq \beta_2$, and $e_c : \gamma_1 \simeq \gamma_2$, and injective embeddings $f : \alpha_1 \hookrightarrow \beta_1$ and $g : \beta_1 \hookrightarrow \gamma_1$, the equivalence of embeddings satisfies:
\[ \text{embeddingCongr}(e_a, e_c)(f \circ g) = \text{embeddingCongr}(e_a, e_b)(f) \circ \text{embeddingCongr}(e_b, e_c)(g) \]
Equiv.refl_toEmbedding
theorem
{α : Type*} : (Equiv.refl α).toEmbedding = Embedding.refl α
Full source
@[simp]
theorem refl_toEmbedding {α : Type*} : (Equiv.refl α).toEmbedding = Embedding.refl α :=
rflInformal description
For any type $\alpha$, the embedding obtained from the identity equivalence on $\alpha$ is equal to the identity embedding on $\alpha$.
Equiv.trans_toEmbedding
theorem
{α β γ : Type*} (e : α ≃ β) (f : β ≃ γ) : (e.trans f).toEmbedding = e.toEmbedding.trans f.toEmbedding
Full source
@[simp]
theorem trans_toEmbedding {α β γ : Type*} (e : α ≃ β) (f : β ≃ γ) :
(e.trans f).toEmbedding = e.toEmbedding.trans f.toEmbedding :=
rflInformal description
For any types $\alpha$, $\beta$, and $\gamma$, and any equivalences $e : \alpha \simeq \beta$ and $f : \beta \simeq \gamma$, the injective embedding obtained from the composition $e \circ f$ is equal to the composition of the injective embeddings obtained from $e$ and $f$ individually. That is, $(e \circ f).toEmbedding = e.toEmbedding \circ f.toEmbedding$.
subtypeOrLeftEmbedding
definition
(p q : α → Prop) [DecidablePred p] : { 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` can be injectively split
into a sum of subtypes `{x // p x} ⊕ {x // q x}` such that `¬ p x` is sent to the right. -/
def subtypeOrLeftEmbedding (p q : α → Prop) [DecidablePred p] :
{ x // p x ∨ q x }{ x // p x ∨ q x } ↪ { x // p x } ⊕ { x // q x } :=
⟨fun x => if h : p x then Sum.inl ⟨x, h⟩ else Sum.inr ⟨x, x.prop.resolve_left h⟩, by
intro x y
dsimp only
split_ifs <;> simp [Subtype.ext_iff]⟩Informal description
Given predicates \( p, q : \alpha \to \text{Prop} \) with \( p \) decidable, the function `subtypeOrLeftEmbedding` injectively maps the subtype \( \{x \mid p x \lor q x\} \) to the sum type \( \{x \mid p x\} \oplus \{x \mid q x\} \). Specifically, it sends \( x \) to the left summand \( \langle x, h \rangle \) if \( p x \) holds (with witness \( h \)), and to the right summand \( \langle x, h' \rangle \) otherwise (where \( h' \) is a witness derived from \( q x \) and \( \neg p x \)).
subtypeOrLeftEmbedding_apply_left
theorem
{p q : α → Prop} [DecidablePred p] (x : { x // p x ∨ q x }) (hx : p x) : subtypeOrLeftEmbedding p q x = Sum.inl ⟨x, hx⟩
Full source
theorem subtypeOrLeftEmbedding_apply_left {p q : α → Prop} [DecidablePred p]
(x : { x // p x ∨ q x }) (hx : p x) :
subtypeOrLeftEmbedding p q x = Sum.inl ⟨x, hx⟩ :=
dif_pos hxInformal description
For any predicates \( p, q : \alpha \to \text{Prop} \) with \( p \) decidable, and for any element \( x \) in the subtype \( \{x \mid p x \lor q x\} \) such that \( p x \) holds, the embedding `subtypeOrLeftEmbedding` maps \( x \) to the left summand \( \langle x, hx \rangle \) in the sum type \( \{x \mid p x\} \oplus \{x \mid q x\} \), where \( hx \) is the proof that \( p x \) holds.
subtypeOrLeftEmbedding_apply_right
theorem
{p q : α → Prop} [DecidablePred p] (x : { x // p x ∨ q x }) (hx : ¬p x) :
subtypeOrLeftEmbedding p q x = Sum.inr ⟨x, x.prop.resolve_left hx⟩
Full source
theorem subtypeOrLeftEmbedding_apply_right {p q : α → Prop} [DecidablePred p]
(x : { x // p x ∨ q x }) (hx : ¬p x) :
subtypeOrLeftEmbedding p q x = Sum.inr ⟨x, x.prop.resolve_left hx⟩ :=
dif_neg hxInformal description
For any predicates \( p, q : \alpha \to \text{Prop} \) with \( p \) decidable, and for any element \( x \) in the subtype \( \{x \mid p x \lor q x\} \) such that \( p x \) does not hold, the embedding `subtypeOrLeftEmbedding` maps \( x \) to the right summand \( \langle x, h \rangle \) in the sum type \( \{x \mid p x\} \oplus \{x \mid q x\} \), where \( h \) is a proof derived from \( q x \) and \( \neg p x \).
Subtype.impEmbedding
definition
(p q : α → Prop) (h : ∀ x, p x → q x) : { x // p x } ↪ { x // q x }
Full source
/-- A subtype `{x // p x}` can be injectively sent to into a subtype `{x // q x}`,
if `p x → q x` for all `x : α`. -/
@[simps]
def Subtype.impEmbedding (p q : α → Prop) (h : ∀ x, p x → q x) : { x // p x }{ x // p x } ↪ { x // q x } :=
⟨fun x => ⟨x, h x x.prop⟩, fun x y => by simp [Subtype.ext_iff]⟩Informal description
Given two predicates \( p \) and \( q \) on a type \( \alpha \) such that \( p(x) \) implies \( q(x) \) for all \( x \in \alpha \), there exists an injective function from the subtype \( \{x \mid p(x)\} \) to the subtype \( \{x \mid q(x)\} \), defined by mapping each \( x \) to itself.