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' : Injective self.toFun

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

def Function.«term_↪_» : Lean.TrailingParserDescr

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

@[implicit_reducible]

instance Function.instFunLikeEmbedding {α : Sort u} {β : Sort v} : FunLike (α ↪ β) α β

instance Function.instEmbeddingLikeEmbedding {α : Sort u} {β : Sort v} : EmbeddingLike (α ↪ β) α β

instance Function.instCanLiftForallEmbeddingCoeInjective {α : Sort u_1} {β : Sort u_2} : CanLift (α → β) (α ↪ β) DFunLike.coe Injective

theorem Function.exists_surjective_iff {α : Sort u_1} {β : Sort u_2} : (∃ (f : α → β), Surjective f) ↔ Nonempty (α → β) ∧ Nonempty (β ↪ α)

@[reducible]

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

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

@[implicit_reducible]

instance Equiv.coeEmbedding {α : Sort u} {β : Sort v} : Coe (α ≃ β) (α ↪ β)

theorem Function.Embedding.coe_injective {α : Sort u_1} {β : Sort u_2} : Injective fun (f : α ↪ β) => ⇑f

theorem Function.Embedding.ext {α : Sort u_1} {β : Sort u_2} {f g : α ↪ β} (h : ∀ (x : α), f x = g x) : f = g

theorem Function.Embedding.ext_iff {α : Sort u_1} {β : Sort u_2} {f g : α ↪ β} : f = g ↔ ∀ (x : α), f x = g x

@[implicit_reducible]

instance Function.Embedding.instUniqueOfIsEmpty {α : Sort u_1} {β : Sort u_2} [IsEmpty α] : Unique (α ↪ β)

@[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 : Injective f) : ⇑{ toFun := f, inj' := i } = f

@[simp]

theorem Function.Embedding.mk_coe {α : Type u_1} {β : Type u_2} (f : α ↪ β) (inj : Injective ⇑f) : { toFun := ⇑f, inj' := inj } = f

theorem Function.Embedding.injective {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) : Injective ⇑f

theorem Function.Embedding.apply_eq_iff_eq {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) (x y : α) : f x = f y ↔ x = y

def Function.Embedding.refl (α : Sort u_1) : α ↪ α

The identity map as a Function.Embedding.

@[simp]

theorem Function.Embedding.refl_apply (α : Sort u_1) (a : α) : (Embedding.refl α) a = a

theorem Function.Embedding.coe_refl (α : Sort u_1) : ⇑(Embedding.refl α) = id

def Function.Embedding.trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α ↪ β) (g : β ↪ γ) : α ↪ γ

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

@[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✝)

theorem Function.Embedding.coe_trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α ↪ β) (g : β ↪ γ) : ⇑(f.trans g) = ⇑g ∘ ⇑f

@[implicit_reducible]

instance Function.Embedding.instTrans : Trans Embedding Embedding Embedding

@[simp]

theorem Function.Embedding.mk_id {α : Sort u_1} : { toFun := id, inj' := ⋯ } = Embedding.refl α

@[simp]

theorem Function.Embedding.mk_trans_mk {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : β → γ) (hf : Injective f) (hg : Injective g) : { toFun := f, inj' := hf }.trans { toFun := g, inj' := hg } = { toFun := g ∘ f, inj' := ⋯ }

theorem Function.Embedding.equiv_toEmbedding_trans_symm_toEmbedding {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) : e.toEmbedding.trans e.symm.toEmbedding = Embedding.refl α

theorem Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) : e.symm.toEmbedding.trans e.toEmbedding = Embedding.refl β

def Function.Embedding.congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α ≃ β) (e₂ : γ ≃ δ) (f : α ↪ γ) : β ↪ δ

Transfer an embedding along a pair of equivalences.

@[simp]

theorem Function.Embedding.congr_apply {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α ≃ β) (e₂ : γ ≃ δ) (f : α ↪ γ) : ⇑(Embedding.congr e₁ e₂ f) = ⇑(f.trans e₂.toEmbedding) ∘ ⇑e₁.symm

noncomputable def Function.Embedding.ofSurjective {α : Sort u_1} {β : Sort u_2} (f : β → α) (hf : Surjective f) : α ↪ β

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

noncomputable def Function.Embedding.equivOfSurjective {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) (hf : Surjective ⇑f) : α ≃ β

Convert a surjective Embedding to an Equiv

def Function.Embedding.ofIsEmpty {α : Sort u_1} {β : Sort u_2} [IsEmpty α] : α ↪ β

There is always an embedding from an empty type.

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.

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

theorem Function.Embedding.setValue_eq_of_ne {α : Sort u_1} {β : Sort u_2} {f : α ↪ β} {a : α} {b : β} {c : α} [(a' : α) → Decidable (a' = a)] [(a' : α) → Decidable (f a' = b)] (hc : c ≠ a) (hb : f c ≠ b) : (f.setValue a b) c = f c

@[simp]

theorem Function.Embedding.setValue_right_apply_eq {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) (a c : α) [(a' : α) → Decidable (a' = a)] [(a' : α) → Decidable (f a' = f c)] : (f.setValue a (f c)) c = f a

def Function.Embedding.some {α : Type u_1} : α ↪ Option α

Embedding into Option α using some.

@[simp]

theorem Function.Embedding.some_apply {α : Type u_1} : ⇑Embedding.some = some

def Function.Embedding.optionMap {α : Type u_1} {β : Type u_2} (f : α ↪ β) : Option α ↪ Option β

A version of Option.map for Function.Embeddings.

@[simp]

theorem Function.Embedding.optionMap_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) : ⇑f.optionMap = Option.map ⇑f

def Function.Embedding.subtype {α : Sort u_1} (p : α → Prop) : Subtype p ↪ α

Embedding of a Subtype.

@[simp]

theorem Function.Embedding.subtype_apply {α : Sort u_1} {p : α → Prop} (x : Subtype p) : (subtype p) x = ↑x

theorem Function.Embedding.subtype_injective {α : Sort u_1} (p : α → Prop) : Injective ⇑(subtype p)

@[simp]

theorem Function.Embedding.coe_subtype {α : Sort u_1} (p : α → Prop) : ⇑(subtype p) = Subtype.val

noncomputable def Function.Embedding.quotientOut (α : Sort u_1) [s : Setoid α] : Quotient s ↪ α

Quotient.out as an embedding.

@[simp]

theorem Function.Embedding.coe_quotientOut (α : Sort u_1) [Setoid α] : ⇑(quotientOut α) = Quotient.out

def Function.Embedding.punit {β : Sort u_1} (b : β) : PUnit.{u_2} ↪ β

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

def Function.Embedding.oneEmbeddingEquiv {one : Type u_1} {α : Type u_2} [Unique one] : (one ↪ α) ≃ α

The equivalence one ↪ α with α, for Unique one.

def Function.Embedding.sectL (α : Type u_1) {β : Type u_2} (b : β) : α ↪ α × β

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

@[simp]

theorem Function.Embedding.sectL_apply (α : Type u_1) {β : Type u_2} (b : β) (a : α) : (sectL α b) a = (a, b)

def Function.Embedding.sectR {α : Type u_1} (a : α) (β : Type u_2) : β ↪ α × β

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

@[simp]

theorem Function.Embedding.sectR_apply {α : Type u_1} (a : α) (β : Type u_2) (b : β) : (sectR a β) b = (a, b)

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

@[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₂ : γ ↪ δ) : α ×' γ ↪ β ×' δ

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

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

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

def Function.Embedding.inl {α : Type u_1} {β : Type u_2} : α ↪ α ⊕ β

The embedding of α into the sum α ⊕ β.

@[simp]

theorem Function.Embedding.inl_apply {α : Type u_1} {β : Type u_2} (val : α) : inl val = Sum.inl val

def Function.Embedding.inr {α : Type u_1} {β : Type u_2} : β ↪ α ⊕ β

The embedding of β into the sum α ⊕ β.

@[simp]

theorem Function.Embedding.inr_apply {α : Type u_1} {β : Type u_2} (val : β) : inr val = Sum.inr val

def Function.Embedding.sigmaMk {α : Type u_1} {β : α → Type u_3} (a : α) : β a ↪ (x : α) × β x

Sigma.mk as a Function.Embedding.

@[simp]

theorem Function.Embedding.sigmaMk_apply {α : Type u_1} {β : α → Type u_3} (a : α) (snd : β a) : (sigmaMk a) snd = ⟨a, snd⟩

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.

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

@[simp]

theorem Function.Embedding.piCongrRight_apply {α : Sort u_1} {β : α → Sort u_2} {γ : α → Sort u_3} (e : (a : α) → β a ↪ γ a) (f : (a : α) → β a) (a : α) : (piCongrRight e) f a = (e a) (f a)

def Function.Embedding.arrowCongrRight {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) : (γ → α) ↪ γ → β

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

@[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} [Inhabited γ] (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.

@[simp]

theorem Function.Embedding.arrowCongrLeft_apply {α : Sort u} {β : Sort v} {γ : Sort w} [Inhabited γ] (e : α ↪ β) (f : α → γ) : e.arrowCongrLeft f = extend (⇑e) f default

@[simp]

theorem Function.Embedding.arrowCongrLeft_refl {α : Sort u} {γ : Sort w} [Inhabited γ] : (Embedding.refl α).arrowCongrLeft = Embedding.refl (α → γ)

@[simp]

theorem Function.Embedding.trans_arrowCongrLeft {α₁ : Sort u} {α₂ : Sort v} {α₃ : Sort x} {γ : Sort w} [Inhabited γ] (e₁₂ : α₁ ↪ α₂) (e₂₃ : α₂ ↪ α₃) : e₁₂.arrowCongrLeft.trans e₂₃.arrowCongrLeft = (e₁₂.trans e₂₃).arrowCongrLeft

def Function.Embedding.subtypeMap {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α ↪ β) (h : ∀ ⦃x : α⦄, p x → q (f x)) : { x : α // p x } ↪ { y : β // q y }

Restrict both domain and codomain of an embedding.

theorem Function.Embedding.swap_apply {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α ↪ β) (x y z : α) : (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)

theorem Function.Embedding.swap_comp {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (f : α ↪ β) (x y : α) : ⇑(Equiv.swap (f x) (f y)) ∘ ⇑f = ⇑f ∘ ⇑(Equiv.swap x y)

def Equiv.asEmbedding {β : Sort u_1} {α : Sort u_2} {p : β → Prop} (e : α ≃ Subtype p) : α ↪ β

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

@[simp]

theorem Equiv.asEmbedding_apply {β : Sort u_1} {α : Sort u_2} {p : β → Prop} (e : α ≃ Subtype p) (a✝ : α) : e.asEmbedding a✝ = ↑(e a✝)

def Equiv.subtypeInjectiveEquivEmbedding (α : Sort u_1) (β : Sort u_2) : { f : α → β // Function.Injective f } ≃ (α ↪ β)

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

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 α₂ ↪ β₂.

@[simp]

theorem Equiv.embeddingCongr_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (h : α ≃ β) (h' : γ ≃ δ) (f : α ↪ γ) : (h.embeddingCongr h') f = Function.Embedding.congr h h' f

@[simp]

theorem Equiv.embeddingCongr_refl {α : Sort u_1} {β : Sort u_2} : (Equiv.refl α).embeddingCongr (Equiv.refl β) = 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} : (Equiv.refl α).toEmbedding = Function.Embedding.refl α

@[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 q : α → Prop) [DecidablePred p] : { 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.

@[simp]

theorem subtypeOrLeftEmbedding_apply_left {α : Type u_1} {p q : α → Prop} [DecidablePred p] (x : { x : α // p x ∨ q x }) (hx : p ↑x) : (subtypeOrLeftEmbedding p q) x = Sum.inl ⟨↑x, hx⟩

@[simp]

theorem subtypeOrLeftEmbedding_apply_right {α : Type u_1} {p q : α → Prop} [DecidablePred p] (x : { x : α // p x ∨ q x }) (hx : ¬p ↑x) : (subtypeOrLeftEmbedding p q) x = Sum.inr ⟨↑x, ⋯⟩

theorem subtypeOrLeftEmbedding_apply {α : Type u_1} {p q : α → Prop} [DecidablePred p] (x : { x : α // p x ∨ q x }) : (subtypeOrLeftEmbedding p q) x = if h : p ↑x then Sum.inl ⟨↑x, h⟩ else Sum.inr ⟨↑x, ⋯⟩

def Subtype.impEmbedding {α : Type u_1} (p q : α → Prop) (h : ∀ (x : α), p x → q 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 : α.

@[simp]

theorem Subtype.impEmbedding_apply_coe {α : Type u_1} (p q : α → Prop) (h : ∀ (x : α), p x → q x) (x : { x : α // p x }) : ↑((impEmbedding p q h) x) = ↑x