# mathlib3documentation

logic.embedding.basic

# Injective functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[nolint]
structure function.embedding (α : Sort u_1) (β : Sort u_2) :
Sort (max 1 (imax u_1 u_2))
• to_fun : α β
• inj' :

α ↪ β is a bundled injective function.

Instances for function.embedding
@[protected, instance]
def function.embedding.has_coe_to_fun {α : Sort u} {β : Sort v} :
has_coe_to_fun β) (λ (_x : α β), α β)
Equations
@[protected, instance]
def function.embedding_like {α : Sort u} {β : Sort v} :
embedding_like β) α β
Equations
@[protected, instance]
def function.injective.can_lift {α : Sort u_1} {β : Sort u_2} :
Equations
@[protected]
def equiv.to_embedding {α : Sort u} {β : Sort v} (f : α β) :
α β

Convert an α ≃ β to α ↪ β.

This is also available as a coercion equiv.coe_embedding. The explicit equiv.to_embedding 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.to_embedding = 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.to_embedding := by simp

Equations
@[simp]
theorem equiv.coe_to_embedding {α : Sort u} {β : Sort v} (f : α β) :
theorem equiv.to_embedding_apply {α : Sort u} {β : Sort v} (f : α β) (a : α) :
@[protected, instance]
def equiv.coe_embedding {α : Sort u} {β : Sort v} :
has_coe β) β)
Equations
@[protected, instance, reducible]
def equiv.perm.coe_embedding {α : Sort u} :
α)
Equations
@[simp]
theorem equiv.coe_eq_to_embedding {α : Sort u} {β : Sort v} (f : α β) :
@[simp]
theorem equiv.as_embedding_apply {α : Sort u} {β : Sort v} {p : β Prop} (e : α ) (ᾰ : α) :
(e.as_embedding) ᾰ = (coe e)
def equiv.as_embedding {α : Sort u} {β : Sort v} {p : β Prop} (e : α ) :
α β

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

Equations
theorem function.embedding.coe_injective {α : Sort u_1} {β : Sort u_2} :
@[ext]
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 : α β} :
( (x : α), f x = g x) f = g
@[simp]
theorem function.embedding.to_fun_eq_coe {α : Sort u_1} {β : Sort u_2} (f : α β) :
@[simp]
theorem function.embedding.coe_fn_mk {α : Sort u_1} {β : Sort u_2} (f : α β) (i : function.injective f) :
{to_fun := f, inj' := i} = f
@[simp]
theorem function.embedding.mk_coe {α : Type u_1} {β : Type u_2} (f : α β) (inj : function.injective f) :
{to_fun := f, inj' := inj} = f
@[protected]
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
@[protected, refl]
def function.embedding.refl (α : Sort u_1) :
α α

The identity map as a function.embedding.

Equations
@[simp]
theorem function.embedding.refl_apply (α : Sort u_1) (a : α) :
= a
@[protected, trans]
def function.embedding.trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α β) (g : β γ) :
α γ

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

Equations
@[simp]
theorem function.embedding.trans_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α β) (g : β γ) (ᾰ : α) :
(f.trans g) = g (f ᾰ)
@[simp]
theorem function.embedding.equiv_to_embedding_trans_symm_to_embedding {α : Sort u_1} {β : Sort u_2} (e : α β) :
@[simp]
theorem function.embedding.equiv_symm_to_embedding_trans_to_embedding {α : Sort u_1} {β : Sort u_2} (e : α β) :
@[protected]
def function.embedding.congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α β) (e₂ : γ δ) (f : α γ) :
β δ

Transfer an embedding along a pair of equivalences.

Equations
@[simp]
theorem function.embedding.congr_apply {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α β) (e₂ : γ δ) (f : α γ) :
e₂ f) = (f.trans e₂.to_embedding) (e₁.symm)
@[protected]
noncomputable def function.embedding.of_surjective {α : Sort u_1} {β : Sort u_2} (f : β α) (hf : function.surjective f) :
α β

A right inverse surj_inv of a surjective function as an embedding.

Equations
@[protected]
noncomputable def function.embedding.equiv_of_surjective {α : Sort u_1} {β : Sort u_2} (f : α β) (hf : function.surjective f) :
α β

Convert a surjective embedding to an equiv

Equations
@[protected]
def function.embedding.of_is_empty {α : Sort u_1} {β : Sort u_2} [is_empty α] :
α β

There is always an embedding from an empty type.

Equations
def function.embedding.set_value {α : 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
theorem function.embedding.set_value_eq {α : Sort u_1} {β : Sort u_2} (f : α β) (a : α) (b : β) [Π (a' : α), decidable (a' = a)] [Π (a' : α), decidable (f a' = b)] :
(f.set_value a b) a = b
@[protected]
def function.embedding.some {α : Type u_1} :
α

Embedding into option α using some.

Equations
@[simp]
theorem function.embedding.some_apply {α : Type u_1} :
@[simp]
def function.embedding.coe_option {α : Type u_1} :
α

Embedding into option α using coe. Usually the correct synctatical form for simp.

Equations
@[simp]
theorem function.embedding.option_map_apply {α : Type u_1} {β : Type u_2} (f : α β) :
def function.embedding.option_map {α : Type u_1} {β : Type u_2} (f : α β) :

A version of option.map for function.embeddings.

Equations
def function.embedding.subtype {α : Sort u_1} (p : α Prop) :
α

Embedding of a subtype.

Equations
@[simp]
theorem function.embedding.coe_subtype {α : Sort u_1} (p : α Prop) :
noncomputable def function.embedding.quotient_out (α : Sort u_1) [s : setoid α] :
α

quotient.out as an embedding.

Equations
@[simp]
theorem function.embedding.coe_quotient_out (α : Sort u_1) [s : setoid α] :
def function.embedding.punit {β : Sort u_1} (b : β) :

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

Equations
@[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
@[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
def function.embedding.prod_map {α : 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
@[simp]
theorem function.embedding.coe_prod_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α β) (e₂ : γ δ) :
(e₁.prod_map e₂) = e₂
def function.embedding.pprod_map {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α β) (e₂ : γ δ) :
γ δ

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

Equations
def function.embedding.sum_map {α : 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
@[simp]
theorem function.embedding.coe_sum_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α β) (e₂ : γ δ) :
(e₁.sum_map e₂) = sum.map e₁ e₂
def function.embedding.inl {α : Type u_1} {β : Type u_2} :
α α β

The embedding of α into the sum α ⊕ β.

Equations
@[simp]
theorem function.embedding.inl_apply {α : Type u_1} {β : Type u_2} (val : α) :
= sum.inl val
@[simp]
theorem function.embedding.inr_apply {α : Type u_1} {β : Type u_2} (val : β) :
= sum.inr val
def function.embedding.inr {α : Type u_1} {β : Type u_2} :
β α β

The embedding of β into the sum α ⊕ β.

Equations
@[simp]
theorem function.embedding.sigma_mk_apply {α : Type u_1} {β : α Type u_3} (a : α) (snd : β a) :
snd = a, snd⟩
def function.embedding.sigma_mk {α : Type u_1} {β : α Type u_3} (a : α) :
β a Σ (x : α), β x

sigma.mk as an function.embedding.

Equations
@[simp]
theorem function.embedding.sigma_map_apply {α : Type u_1} {α' : Type u_2} {β : α Type u_3} {β' : α' Type u_4} (f : α α') (g : Π (a : α), β a β' (f a)) (x : Σ (a : α), β a) :
(f.sigma_map g) x = (λ (a : α), (g a)) x
def function.embedding.sigma_map {α : 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
@[simp]
theorem function.embedding.Pi_congr_right_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.Pi_congr_right {α : 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 λ a, e a (f a).

Equations
def function.embedding.arrow_congr_right {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) :
α) γ β

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

Equations
@[simp]
theorem function.embedding.arrow_congr_right_apply {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) (f : γ α) :
noncomputable def function.embedding.arrow_congr_left {α : 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.

Equations
@[protected]
def function.embedding.subtype_map {α : 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.

Equations
theorem function.embedding.swap_apply {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α β) (x y z : α) :
(equiv.swap (f x) (f y)) (f z) = f ( y) z)
theorem function.embedding.swap_comp {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α β) (x y : α) :
(equiv.swap (f x) (f y)) f = f y)
def equiv.subtype_injective_equiv_embedding (α : Sort u_1) (β : Sort u_2) :
{f // β)

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

Equations
@[simp]
theorem equiv.embedding_congr_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (h : α β) (h' : γ δ) (f : α γ) :
def equiv.embedding_congr {α : 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
@[simp]
theorem equiv.embedding_congr_refl {α : Sort u_1} {β : Sort u_2} :
(equiv.refl β) = equiv.refl β)
@[simp]
theorem equiv.embedding_congr_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₂).embedding_congr (e₁'.trans e₂') = (e₁.embedding_congr e₁').trans (e₂.embedding_congr e₂')
@[simp]
theorem equiv.embedding_congr_symm {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
theorem equiv.embedding_congr_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 : β₁ γ₁) :
@[simp]
theorem equiv.refl_to_embedding {α : Type u_1} :
@[simp]
theorem equiv.trans_to_embedding {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f : β γ) :
def subtype_or_left_embedding {α : Type u_1} (p 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
theorem subtype_or_left_embedding_apply_left {α : Type u_1} {p q : α Prop} (x : {x // p x q x}) (hx : p x) :
x = sum.inl x, hx⟩
theorem subtype_or_left_embedding_apply_right {α : Type u_1} {p q : α Prop} (x : {x // p x q x}) (hx : ¬p x) :
x = sum.inr x, _⟩
def subtype.imp_embedding {α : 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 : α.

Equations
@[simp]
theorem subtype.imp_embedding_apply_coe {α : Type u_1} (p q : α Prop) (h : (x : α), p x q x) (x : {x // p x}) :
( h) x) = x