# Injective functions #

structure Function.Embedding (α : Sort u_1) (β : Sort u_2) :
Sort (max (max 1 u_1) u_2)

α ↪ β is a bundled injective function.

• toFun : αβ

An embedding as a function. Use coercion instead.

• inj' : Function.Injective self.toFun

An embedding is an injective function. Use Function.Embedding.injective instead.

Instances For
theorem Function.Embedding.inj' {α : Sort u_1} {β : Sort u_2} (self : α β) :

An embedding is an injective function. Use Function.Embedding.injective instead.

An embedding, a.k.a. a bundled injective function.

Equations
Instances For
instance Function.instFunLikeEmbedding {α : Sort u} {β : Sort v} :
FunLike (α β) α β
Equations
• Function.instFunLikeEmbedding = { coe := Function.Embedding.toFun, coe_injective' := }
instance Function.instEmbeddingLikeEmbedding {α : Sort u} {β : Sort v} :
EmbeddingLike (α β) α β
Equations
• =
theorem Function.exists_surjective_iff {α : Sort u_1} {β : Sort u_2} :
(∃ (f : αβ), ) Nonempty (αβ) Nonempty (β α)
instance Function.instCanLiftForallEmbeddingCoeInjective {α : Sort u_1} {β : Sort u_2} :
CanLift (αβ) (α β) DFunLike.coe Function.Injective
Equations
• =
def Equiv.toEmbedding {α : Sort u} {β : Sort v} (f : α β) :
α β

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:

-- 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

Equations
• f.toEmbedding = { toFun := f, inj' := }
Instances For
@[simp]
theorem Equiv.coe_toEmbedding {α : Sort u} {β : Sort v} (f : α β) :
f.toEmbedding = f
theorem Equiv.toEmbedding_apply {α : Sort u} {β : Sort v} (f : α β) (a : α) :
f.toEmbedding a = f a
theorem Equiv.toEmbedding_injective {α : Sort u} {β : Sort v} :
Function.Injective Equiv.toEmbedding
instance Equiv.coeEmbedding {α : Sort u} {β : Sort v} :
Coe (α β) (α β)
Equations
• Equiv.coeEmbedding = { coe := Equiv.toEmbedding }
@[reducible, inline]
instance Equiv.Perm.coeEmbedding {α : Sort u} :
Coe () (α α)
Equations
• Equiv.Perm.coeEmbedding = Equiv.coeEmbedding
theorem Function.Embedding.coe_injective {α : Sort u_1} {β : Sort u_2} :
Function.Injective fun (f : α β) => f
theorem Function.Embedding.ext {α : Sort u_1} {β : Sort u_2} {f : α β} {g : α β} (h : ∀ (x : α), f x = g x) :
f = g
instance Function.Embedding.instUniqueOfIsEmpty {α : Sort u_1} {β : Sort u_2} [] :
Unique (α β)
Equations
• Function.Embedding.instUniqueOfIsEmpty = { default := { toFun := fun (a : α) => , inj' := }, uniq := }
theorem Function.Embedding.ext_iff {α : Sort u_1} {β : Sort u_2} {f : α β} {g : α β} :
(∀ (x : α), f x = g x) f = g
@[simp]
theorem Function.Embedding.toFun_eq_coe {α : Sort u_1} {β : Sort u_2} (f : α β) :
f.toFun = f
@[simp]
theorem Function.Embedding.coeFn_mk {α : Sort u_1} {β : Sort u_2} (f : αβ) (i : ) :
{ toFun := f, inj' := i } = f
@[simp]
theorem Function.Embedding.mk_coe {α : Type u_1} {β : Type u_2} (f : α β) (inj : ) :
{ toFun := f, inj' := inj } = f
theorem Function.Embedding.injective {α : Sort u_1} {β : Sort u_2} (f : α β) :
theorem Function.Embedding.apply_eq_iff_eq {α : Sort u_1} {β : Sort u_2} (f : α β) (x : α) (y : α) :
f x = f y x = y
@[simp]
theorem Function.Embedding.refl_apply (α : Sort u_1) (a : α) :
= a
def Function.Embedding.refl (α : Sort u_1) :
α α

The identity map as a Function.Embedding.

Equations
• = { toFun := id, inj' := }
Instances For
@[simp]
theorem Function.Embedding.trans_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α β) (g : β γ) :
∀ (a : α), (f.trans g) a = g (f a)
def Function.Embedding.trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α β) (g : β γ) :
α γ

Composition of f : α ↪ β and g : β ↪ γ.

Equations
• f.trans g = { toFun := g f, inj' := }
Instances For
Equations
@[simp]
theorem Function.Embedding.equiv_toEmbedding_trans_symm_toEmbedding {α : Sort u_1} {β : Sort u_2} (e : α β) :
e.toEmbedding.trans e.symm.toEmbedding =
@[simp]
theorem Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding {α : Sort u_1} {β : Sort u_2} (e : α β) :
e.symm.toEmbedding.trans e.toEmbedding =
@[simp]
theorem Function.Embedding.congr_apply {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α β) (e₂ : γ δ) (f : α γ) :
() = (f.trans e₂.toEmbedding) e₁.symm
def Function.Embedding.congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α β) (e₂ : γ δ) (f : α γ) :
β δ

Transfer an embedding along a pair of equivalences.

Equations
• = e₁.symm.toEmbedding.trans (f.trans e₂.toEmbedding)
Instances For
noncomputable def Function.Embedding.ofSurjective {α : Sort u_1} {β : Sort u_2} (f : βα) (hf : ) :
α β

A right inverse surjInv of a surjective function as an Embedding.

Equations
• = { toFun := , inj' := }
Instances For
noncomputable def Function.Embedding.equivOfSurjective {α : Sort u_1} {β : Sort u_2} (f : α β) (hf : ) :
α β

Convert a surjective Embedding to an Equiv

Equations
• f.equivOfSurjective hf =
Instances For
def Function.Embedding.ofIsEmpty {α : Sort u_1} {β : Sort u_2} [] :
α β

There is always an embedding from an empty type.

Equations
• Function.Embedding.ofIsEmpty = { toFun := fun (a : α) => , inj' := }
Instances For
def Function.Embedding.setValue {α : Sort u_1} {β : Sort u_2} (f : α β) (a : α) (b : β) [(a' : α) → Decidable (a' = a)] [(a' : α) → Decidable (f a' = b)] :
α β

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.

Equations
• f.setValue a b = { toFun := fun (a' : α) => if a' = a then b else if f a' = b then f a else f a', inj' := }
Instances For
@[simp]
theorem Function.Embedding.setValue_eq {α : Sort u_1} {β : Sort u_2} (f : α β) (a : α) (b : β) [(a' : α) → Decidable (a' = a)] [(a' : α) → Decidable (f a' = b)] :
(f.setValue a b) a = b
@[simp]
theorem Function.Embedding.setValue_eq_iff {α : Sort u_1} {β : Sort u_2} (f : α β) {a : α} {a' : α} {b : β} [(a' : α) → Decidable (a' = a)] [(a' : α) → Decidable (f a' = b)] :
(f.setValue a b) a' = b a' = a
@[simp]
theorem Function.Embedding.some_apply {α : Type u_1} :
Function.Embedding.some = some
def Function.Embedding.some {α : Type u_1} :
α

Embedding into Option α using some.

Equations
• Function.Embedding.some = { toFun := some, inj' := }
Instances For
@[simp]
theorem Function.Embedding.optionMap_apply {α : Type u_1} {β : Type u_2} (f : α β) :
f.optionMap =
def Function.Embedding.optionMap {α : Type u_1} {β : Type u_2} (f : α β) :

A version of Option.map for Function.Embeddings.

Equations
• f.optionMap = { toFun := , inj' := }
Instances For
def Function.Embedding.subtype {α : Sort u_1} (p : αProp) :
α

Embedding of a Subtype.

Equations
• = { toFun := Subtype.val, inj' := }
Instances For
@[simp]
theorem Function.Embedding.coe_subtype {α : Sort u_1} (p : αProp) :
= Subtype.val
noncomputable def Function.Embedding.quotientOut (α : Sort u_1) [s : ] :
α

Quotient.out as an embedding.

Equations
• = { toFun := Quotient.out, inj' := }
Instances For
@[simp]
theorem Function.Embedding.coe_quotientOut (α : Sort u_1) [] :
= Quotient.out
def Function.Embedding.punit {β : Sort u_1} (b : β) :

Choosing an element b : β gives an embedding of PUnit into β.

Equations
Instances For
@[simp]
theorem Function.Embedding.sectl_apply (α : Type u_1) {β : Type u_2} (b : β) (a : α) :
() a = (a, b)
def Function.Embedding.sectl (α : Type u_1) {β : Type u_2} (b : β) :
α α × β

Fixing an element b : β gives an embedding α ↪ α × β.

Equations
• = { toFun := fun (a : α) => (a, b), inj' := }
Instances For
@[simp]
theorem Function.Embedding.sectr_apply {α : Type u_1} (a : α) (β : Type u_2) (b : β) :
() b = (a, b)
def Function.Embedding.sectr {α : Type u_1} (a : α) (β : Type u_2) :
β α × β

Fixing an element a : α gives an embedding β ↪ α × β.

Equations
• = { toFun := fun (b : β) => (a, b), inj' := }
Instances For
def Function.Embedding.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α β) (e₂ : γ δ) :
α × γ β × δ

If e₁ and e₂ are embeddings, then so is Prod.map e₁ e₂ : (a, b) ↦ (e₁ a, e₂ b).

Equations
• e₁.prodMap e₂ = { toFun := Prod.map e₁ e₂, inj' := }
Instances For
@[simp]
theorem Function.Embedding.coe_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α β) (e₂ : γ δ) :
(e₁.prodMap e₂) = Prod.map e₁ e₂
def Function.Embedding.pprodMap {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α β) (e₂ : γ δ) :
PProd α γ PProd β δ

If e₁ and e₂ are embeddings, then so is fun ⟨a, b⟩ ↦ ⟨e₁ a, e₂ b⟩ : PProd α γ → PProd β δ.

Equations
• e₁.pprodMap e₂ = { toFun := fun (x : PProd α γ) => e₁ x.fst, e₂ x.snd, inj' := }
Instances For
def Function.Embedding.sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α β) (e₂ : γ δ) :
α γ β δ

If e₁ and e₂ are embeddings, then so is Sum.map e₁ e₂.

Equations
• e₁.sumMap e₂ = { toFun := Sum.map e₁ e₂, inj' := }
Instances For
@[simp]
theorem Function.Embedding.coe_sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α β) (e₂ : γ δ) :
(e₁.sumMap e₂) = Sum.map e₁ e₂
@[simp]
theorem Function.Embedding.inl_apply {α : Type u_1} {β : Type u_2} (val : α) :
Function.Embedding.inl val = Sum.inl val
def Function.Embedding.inl {α : Type u_1} {β : Type u_2} :
α α β

The embedding of α into the sum α ⊕ β.

Equations
• Function.Embedding.inl = { toFun := Sum.inl, inj' := }
Instances For
@[simp]
theorem Function.Embedding.inr_apply {α : Type u_1} {β : Type u_2} (val : β) :
Function.Embedding.inr val = Sum.inr val
def Function.Embedding.inr {α : Type u_1} {β : Type u_2} :
β α β

The embedding of β into the sum α ⊕ β.

Equations
• Function.Embedding.inr = { toFun := Sum.inr, inj' := }
Instances For
@[simp]
theorem Function.Embedding.sigmaMk_apply {α : Type u_1} {β : αType u_3} (a : α) (snd : β a) :
snd = a, snd
def Function.Embedding.sigmaMk {α : Type u_1} {β : αType u_3} (a : α) :
β a (x : α) × β x

Sigma.mk as a Function.Embedding.

Equations
• = { toFun := , inj' := }
Instances For
@[simp]
theorem Function.Embedding.sigmaMap_apply {α : Type u_1} {α' : Type u_2} {β : αType u_3} {β' : α'Type u_4} (f : α α') (g : (a : α) → β a β' (f a)) (x : (a : α) × β a) :
(f.sigmaMap g) x = Sigma.map (f) (fun (a : α) => (g a)) x
def Function.Embedding.sigmaMap {α : Type u_1} {α' : Type u_2} {β : αType u_3} {β' : α'Type u_4} (f : α α') (g : (a : α) → β a β' (f a)) :
(a : α) × β a (a' : α') × β' a'

If f : α ↪ α' is an embedding and g : Π a, β α ↪ β' (f α) is a family of embeddings, then Sigma.map f g is an embedding.

Equations
• f.sigmaMap g = { toFun := Sigma.map f fun (a : α) => (g a), inj' := }
Instances For
@[simp]
theorem Function.Embedding.piCongrRight_apply {α : Sort u_1} {β : αSort u_2} {γ : αSort u_3} (e : (a : α) → β a γ a) (f : (a : α) → β a) (a : α) :
= (e a) (f a)
def Function.Embedding.piCongrRight {α : Sort u_1} {β : αSort u_2} {γ : αSort u_3} (e : (a : α) → β a γ a) :
((a : α) → β a) (a : α) → γ a

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).

Equations
• = { toFun := fun (f : (a : α) → β a) (a : α) => (e a) (f a), inj' := }
Instances For
def Function.Embedding.arrowCongrRight {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) :
(γα) γβ

An embedding e : α ↪ β defines an embedding (γ → α) ↪ (γ → β) that sends each f to e ∘ f.

Equations
Instances For
@[simp]
theorem Function.Embedding.arrowCongrRight_apply {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : γα) :
e.arrowCongrRight f = e f
noncomputable def Function.Embedding.arrowCongrLeft {α : Sort u} {β : Sort v} {γ : Sort w} [] (e : α β) :
(αγ) βγ

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.

Equations
• e.arrowCongrLeft = { toFun := fun (f : αγ) => Function.extend (e) f default, inj' := }
Instances For
def Function.Embedding.subtypeMap {α : Sort u_1} {β : Sort u_2} {p : αProp} {q : βProp} (f : α β) (h : ∀ ⦃x : α⦄, p xq (f x)) :
{ x : α // p x } { y : β // q y }

Restrict both domain and codomain of an embedding.

Equations
• f.subtypeMap h = { toFun := Subtype.map (f) h, inj' := }
Instances For
theorem Function.Embedding.swap_apply {α : Type u_1} {β : Type u_2} [] [] (f : α β) (x : α) (y : α) (z : α) :
(Equiv.swap (f x) (f y)) (f z) = f (() z)
theorem Function.Embedding.swap_comp {α : Type u_1} {β : Type u_2} [] [] (f : α β) (x : α) (y : α) :
(Equiv.swap (f x) (f y)) f = f ()
@[simp]
theorem Equiv.asEmbedding_apply {β : Sort u_1} {α : Sort u_2} {p : βProp} (e : α ) :
∀ (a : α), e.asEmbedding a = (e a)
def Equiv.asEmbedding {β : Sort u_1} {α : Sort u_2} {p : βProp} (e : α ) :
α β

Given an equivalence to a subtype, produce an embedding to the elements of the corresponding set.

Equations
• e.asEmbedding = e.toEmbedding.trans
Instances For
def Equiv.subtypeInjectiveEquivEmbedding (α : Sort u_1) (β : Sort u_2) :
{ f : αβ // } (α β)

The type of embeddings α ↪ β is equivalent to the subtype of all injective functions α → β.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Equiv.embeddingCongr_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (h : α β) (h' : γ δ) (f : α γ) :
(h.embeddingCongr h') f =
def Equiv.embeddingCongr {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (h : α β) (h' : γ δ) :
(α γ) (β δ)

If α₁ ≃ α₂ and β₁ ≃ β₂, then the type of embeddings α₁ ↪ β₁ is equivalent to the type of embeddings α₂ ↪ β₂.

Equations
• h.embeddingCongr h' = { toFun := fun (f : α γ) => , invFun := fun (f : β δ) => Function.Embedding.congr h.symm h'.symm f, left_inv := , right_inv := }
Instances For
@[simp]
theorem Equiv.embeddingCongr_refl {α : Sort u_1} {β : Sort u_2} :
().embeddingCongr () = Equiv.refl (α β)
@[simp]
theorem Equiv.embeddingCongr_trans {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} {α₃ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
(e₁.trans e₂).embeddingCongr (e₁'.trans e₂') = (e₁.embeddingCongr e₁').trans (e₂.embeddingCongr e₂')
@[simp]
theorem Equiv.embeddingCongr_symm {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(e₁.embeddingCongr e₂).symm = e₁.symm.embeddingCongr e₂.symm
theorem Equiv.embeddingCongr_apply_trans {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} (ea : α₁ α₂) (eb : β₁ β₂) (ec : γ₁ γ₂) (f : α₁ β₁) (g : β₁ γ₁) :
(ea.embeddingCongr ec) (f.trans g) = ((ea.embeddingCongr eb) f).trans ((eb.embeddingCongr ec) g)
@[simp]
theorem Equiv.refl_toEmbedding {α : Type u_1} :
().toEmbedding =
@[simp]
theorem Equiv.trans_toEmbedding {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f : β γ) :
(e.trans f).toEmbedding = e.toEmbedding.trans f.toEmbedding
def subtypeOrLeftEmbedding {α : Type u_1} (p : αProp) (q : αProp) [] :
{ x : α // p x q x } { x : α // p x } { x : α // q x }

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.

Equations
• = { toFun := fun (x : { x : α // p x q x }) => if h : p x then Sum.inl x, h else Sum.inr x, , inj' := }
Instances For
theorem subtypeOrLeftEmbedding_apply_left {α : Type u_1} {p : αProp} {q : αProp} [] (x : { x : α // p x q x }) (hx : p x) :
() x = Sum.inl x, hx
theorem subtypeOrLeftEmbedding_apply_right {α : Type u_1} {p : αProp} {q : αProp} [] (x : { x : α // p x q x }) (hx : ¬p x) :
() x = Sum.inr x,
@[simp]
theorem Subtype.impEmbedding_apply_coe {α : Type u_1} (p : αProp) (q : αProp) (h : ∀ (x : α), p xq x) (x : { x : α // p x }) :
(() x) = x
def Subtype.impEmbedding {α : Type u_1} (p : αProp) (q : αProp) (h : ∀ (x : α), p xq x) :
{ x : α // p x } { x : α // q x }

A subtype {x // p x} can be injectively sent to into a subtype {x // q x}, if p x → q x for all x : α.

Equations
• = { toFun := fun (x : { x : α // p x }) => x, , inj' := }
Instances For