mathlib documentation

logic.embedding

Injective functions #

@[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.embedding.can_lift {α : Sort u_1} {β : Sort u_2} :
can_lift (α → β) β)
Equations
@[simp]
theorem equiv.to_embedding_apply {α : Sort u} {β : Sort v} (f : α β) (ᾰ : α) :
(f.to_embedding) ᾰ = f ᾰ
@[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
@[protected, instance]
def equiv.coe_embedding {α : Sort u} {β : Sort v} :
has_coe β) β)
Equations
@[protected, instance, reducible]
def equiv.perm.coe_embedding {α : Sort u} :
has_coe (equiv.perm α) α)
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 : α subtype p) (ᾰ : α) :
(e.as_embedding) ᾰ = (coe e)
def equiv.as_embedding {α : Sort u} {β : Sort v} {p : β → Prop} (e : α subtype p) :
α β

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

Equations
@[simp]
theorem equiv.as_embedding_range {α : Sort u_1} {β : Type u_2} {p : β → Prop} (e : α subtype p) :
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 : α) :
@[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 ᾰ)
@[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 : α γ) :
@[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} :
α option α

Embedding into option α using some.

Equations
def function.embedding.coe_option {α : Type u_1} :
α option α

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

Equations
def function.embedding.coe_with_top {α : Type u_1} :

Embedding into with_top α.

Equations
@[simp]
theorem function.embedding.coe_with_top_apply {α : Type u_1} (ᾰ : α) :
def function.embedding.option_elim {α : Type u_1} {β : Type u_2} (f : α β) (x : β) (h : x set.range f) :
option α β

Given an embedding f : α ↪ β and a point outside of set.range f, construct an embedding option α ↪ β.

Equations
@[simp]
theorem function.embedding.option_elim_apply {α : Type u_1} {β : Type u_2} (f : α β) (x : β) (h : x set.range f) (ᾰ : option α) :
(f.option_elim x h) = option.elim x f
@[simp]
theorem function.embedding.option_embedding_equiv_symm_apply (α : Type u_1) (β : Type u_2) (f : Σ (f : α β), (set.range f)) :
def function.embedding.option_embedding_equiv (α : Type u_1) (β : Type u_2) :
(option α β) Σ (f : α β), (set.range f)

Equivalence between embeddings of option α and a sigma type over the embeddings of α.

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
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 : α) :
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 : β) :
def function.embedding.sectr {α : Type u_1} (a : α) (β : Type u_2) :
β α × β

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

Equations
def function.embedding.cod_restrict {α : Sort u_1} {β : Type u_2} (p : set β) (f : α β) (H : ∀ (a : α), f a p) :
α p

Restrict the codomain of an embedding.

Equations
@[simp]
theorem function.embedding.cod_restrict_apply {α : Sort u_1} {β : Type u_2} (p : set β) (f : α β) (H : ∀ (a : α), f a p) (a : α) :
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₂) = prod.map e₁ e₂
def function.embedding.pprod_map {α : 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 λ ⟨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 : α) :
@[simp]
theorem function.embedding.inr_apply {α : Type u_1} {β : Type u_2} (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) :
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 = sigma.map f (λ (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 : α) :
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 xq (f x)) :
{x // p x} {y // q y}

Restrict both domain and codomain of an embedding.

Equations
@[protected]
def function.embedding.image {α : Type u_1} {β : Type u_2} (f : α β) :
set α set β

set.image as an embedding set α ↪ set β.

Equations
@[simp]
theorem function.embedding.image_apply {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
(f.image) s = f '' s
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 ((equiv.swap x y) z)
theorem function.embedding.swap_comp {α : Type u_1} {β : Type u_2} [decidable_eq α] [decidable_eq β] (f : α β) (x y : α) :
def equiv.subtype_injective_equiv_embedding (α : Sort u_1) (β : Sort u_2) :
{f // function.injective 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} :
@[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]
@[simp]
theorem equiv.trans_to_embedding {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α β) (f : β γ) :
def set.embedding_of_subset {α : Type u_1} (s t : set α) (h : s t) :

The injection map is an embedding between subsets.

Equations
@[simp]
theorem set.embedding_of_subset_apply {α : Type u_1} (s t : set α) (h : s t) (x : s) :
(s.embedding_of_subset t h) x = x.val, _⟩
def subtype_or_left_embedding {α : Type u_1} (p q : α → Prop) [decidable_pred 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.

Equations
theorem subtype_or_left_embedding_apply_left {α : Type u_1} {p q : α → Prop} [decidable_pred p] (x : {x // p x q x}) (hx : p x) :
theorem subtype_or_left_embedding_apply_right {α : Type u_1} {p q : α → Prop} [decidable_pred p] (x : {x // p x q x}) (hx : ¬p x) :
def subtype.imp_embedding {α : Type u_1} (p q : α → Prop) (h : p q) :
{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 : p q) (x : {x // p x}) :
def subtype_or_equiv {α : Type u_1} (p q : α → Prop) [decidable_pred p] (h : disjoint p q) :
{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 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.sum_compl, for when is_compl p q.

Equations
@[simp]
theorem subtype_or_equiv_apply {α : Type u_1} (p q : α → Prop) [decidable_pred p] (h : disjoint p q) (ᾰ : {x // p x q x}) :
@[simp]
theorem subtype_or_equiv_symm_inl {α : Type u_1} (p q : α → Prop) [decidable_pred p] (h : disjoint p q) (x : {x // p x}) :
((subtype_or_equiv p q h).symm) (sum.inl x) = x, _⟩
@[simp]
theorem subtype_or_equiv_symm_inr {α : Type u_1} (p q : α → Prop) [decidable_pred p] (h : disjoint p q) (x : {x // q x}) :
((subtype_or_equiv p q h).symm) (sum.inr x) = x, _⟩