logic.embedding

# Injective functions

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

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

Equations
@[simp]
theorem equiv.to_embedding_apply {α : Sort u} {β : Sort v} (f : α β) (ᾰ : α) :
(f.to_embedding) ᾰ = f ᾰ

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

Convert an α ≃ β to α ↪ β.

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

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

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

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

def function.embedding.trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α β) (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 : α β) :

def function.embedding.congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α β) (e₂ : γ δ) (f : α γ) :
β δ

Equations
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
def function.embedding.equiv_of_surjective {α : Sort u_1} {β : Type u_2} (f : α β) (hf : function.surjective f) :
α β

Convert a surjective embedding to an equiv

Equations
def function.embedding.of_not_nonempty {α : Sort u_1} {β : Sort u_2} (hα : ¬) :
α β

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} :
α

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} (b : β) :

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

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

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 : α β) (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 : α) :
a = f 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₂) = e₂

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
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
def function.embedding.Pi_congr_right {α : Sort u_1} {β : α → Sort u_2} {γ : α → Sort u_3} (e : Π (a : α), β a γ a) :
(Π (a : α), β a) Π (a : α), γ a

Equations
• = {to_fun := λ (f : Π (a : α), β a) (a : α), (e a) (f a), inj' := _}
def function.embedding.arrow_congr_left {α : Sort u} {β : Sort v} {γ : Sort w} (e : α β) :
(γ → α) γ → β

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

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

Equations
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 ( 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)

@[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 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) :
h) x = x.val, _⟩

def add_left_embedding {G : Type u} (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} (g : G) :
G G

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

Equations
@[simp]
theorem add_left_embedding_apply {G : Type u} (g h : G) :
h = g + h

@[simp]
theorem mul_left_embedding_apply {G : Type u} (g h : G) :
h = g * h

@[simp]
theorem add_right_embedding_apply {G : Type u} (g h : G) :
h = h + g

def mul_right_embedding {G : Type u} (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} (g : G) :
G G

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

@[simp]
theorem mul_right_embedding_apply {G : Type u} (g h : G) :
h = h * g