mathlib documentation

logic.embedding

Injective functions

@[nolint]
structure function.embedding  :
Sort u_1Sort u_2Sort (max 1 (imax u_1 u_2))

α ↪ β is a bundled injective function.

@[instance]
def function.has_coe_to_fun {α : Sort u} {β : Sort v} :

Equations
@[simp]
theorem equiv.to_embedding_to_fun {α : Sort u} {β : Sort v} (f : α β) (a : α) :

def equiv.to_embedding {α : Sort u} {β : Sort v} :
α βα β

Convert an α ≃ β to α ↪ β.

Equations
@[ext]
theorem function.embedding.ext {α : Sort u_1} {β : Sort u_2} {f g : α β} :
(∀ (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

theorem function.embedding.injective {α : Sort u_1} {β : Sort u_2} (f : α β) :

def function.embedding.refl (α : Sort u_1) :
α α

Equations
@[simp]
theorem function.embedding.refl_to_fun (α : Sort u_1) (a : α) :

def function.embedding.trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} :
β) γ)α γ

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

def function.embedding.congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} :
α βγ δ γ)β δ

Equations
def function.embedding.of_surjective {α : Sort u_1} {β : Sort u_2} (f : β → α) :

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

Equations
def function.embedding.equiv_of_surjective {α : Sort u_1} {β : Type u_2} (f : α β) :

Convert a surjective embedding to an equiv

Equations
def function.embedding.of_not_nonempty {α : Sort u_1} {β : Sort u_2} :
¬nonempty αα β

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

def function.embedding.some {α : Type u_1} :
α option α

Embedding into option

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

def function.embedding.punit {β : Sort u_1} :
β → punit β

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

Equations
def function.embedding.sectl (α : Type u_1) {β : Type u_2} :
β → α α × β

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

Equations
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 : α β) :
(∀ (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} :
β) δ)α × γ β × δ

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.sum_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} :
β) δ)α γ β δ

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
def function.embedding.inr {α : Type u_1} {β : Type u_2} :
β α β

The embedding of β into the sum α ⊕ β.

Equations
@[simp]
theorem function.embedding.sigma_mk_to_fun {α : 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_to_fun {α : 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 : α α') :
(Π (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
def function.embedding.Pi_congr_right {α : Sort u_1} {β : α → Sort u_2} {γ : α → Sort u_3} :
(Π (a : α), β a γ a)((Π (a : α), β a) Π (a : α), γ a)

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

Equations
def function.embedding.arrow_congr_right {α : Sort u} {β : Sort v} {γ : Sort w} [inhabited γ] :
β)(α → γ) β → γ

Equations
def function.embedding.subtype_map {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α β) :
(∀ ⦃x : α⦄, p xq (f x)){x // p x} {y // q y}

Equations
@[simp]
theorem function.embedding.image_to_fun {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
(f.image) s = f '' s

def function.embedding.image {α : Type u_1} {β : Type u_2} :
β)set α set β

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

Equations
@[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 α) :
s ts t

The injection map is an embedding between subsets.

Equations
@[simp]
theorem set.embedding_of_subset_to_fun {α : Type u_1} (s t : set α) (h : s t) (x : s) :
(s.embedding_of_subset t h) x = x.val, _⟩

def add_left_embedding {G : Type u} [add_left_cancel_semigroup G] :
G → G G

The embedding of a left cancellative additive semigroup into itself by left translation by a fixed element.

def mul_left_embedding {G : Type u} [left_cancel_semigroup G] :
G → G G

The embedding of a left cancellative semigroup into itself by left multiplication by a fixed element.

Equations
def mul_right_embedding {G : Type u} [right_cancel_semigroup G] :
G → G G

The embedding of a right cancellative semigroup into itself by right multiplication by a fixed element.

Equations
def add_right_embedding {G : Type u} [add_right_cancel_semigroup G] :
G → G G

The embedding of a right cancellative additive semigroup into itself by right translation by a fixed element.