mathlib docs: logic.embedding

source

structure function.embedding (α : Sort u_1) (β : Sort u_2) :

Sort (max 1 (imax u_1 u_2))

to_fun : α → β
inj' : function.injective c.to_fun

α ↪ β is a bundled injective function.

source

@[instance]

def function.has_coe_to_fun {α : Sort u} {β : Sort v} :

has_coe_to_fun (α ↪ β)

Equations

function.has_coe_to_fun = {F := λ (x : α ↪ β), α → β, coe := function.embedding.to_fun β}

source

@[simp]

theorem equiv.to_embedding_to_fun {α : Sort u} {β : Sort v} (f : α ≃ β) (a : α) :

⇑(f.to_embedding) a = ⇑f a

source

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

α ↪ β

Convert an α ≃ β to α ↪ β.

Equations

f.to_embedding = {to_fun := ⇑f, inj' := _}

source

@[ext]

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

f = g

source

theorem function.embedding.ext_iff {α : Sort u_1} {β : Sort u_2} {f g : α ↪ β} :

(∀ (x : α), ⇑f x = ⇑g x) ↔ f = g

source

@[simp]

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

f.to_fun = ⇑f

source

@[simp]

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

⇑{to_fun := f, inj' := i} = f

source

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

function.injective ⇑f

source

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

α ↪ α

Equations

function.embedding.refl α = {to_fun := id α, inj' := _}

source

@[simp]

theorem function.embedding.refl_to_fun (α : Sort u_1) (a : α) :

⇑(function.embedding.refl α) a = a

source

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

α ↪ γ

Equations

f.trans g = {to_fun := ⇑g ∘ ⇑f, inj' := _}

source

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

source

@[simp]

theorem function.embedding.equiv_to_embedding_trans_symm_to_embedding {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) :

e.to_embedding.trans e.symm.to_embedding = function.embedding.refl α

source

@[simp]

theorem function.embedding.equiv_symm_to_embedding_trans_to_embedding {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) :

e.symm.to_embedding.trans e.to_embedding = function.embedding.refl β

source

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

β ↪ δ

Equations

function.embedding.congr e₁ e₂ f = e₁.symm.to_embedding.trans (f.trans e₂.to_embedding)

source

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

function.embedding.of_surjective f hf = {to_fun := function.surj_inv hf, inj' := _}

source

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

f.equiv_of_surjective hf = equiv.of_bijective ⇑f _

source

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

α ↪ β

Equations

function.embedding.of_not_nonempty hα = {to_fun := λ (a : α), _.elim, inj' := _}

source

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

f.set_value a b = {to_fun := λ (a' : α), ite (a' = a) b (ite (⇑f a' = b) (⇑f a) (⇑f a')), inj' := _}

source

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

source

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

α ↪ option α

Embedding into option

Equations

function.embedding.some = {to_fun := some α, inj' := _}

source

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

subtype p ↪ α

Embedding of a subtype.

Equations

function.embedding.subtype p = {to_fun := coe coe_to_lift, inj' := _}

source

@[simp]

theorem function.embedding.coe_subtype {α : Sort u_1} (p : α → Prop) :

⇑(function.embedding.subtype p) = coe

source

def function.embedding.punit {β : Sort u_1} (b : β) :

punit ↪ β

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

Equations

function.embedding.punit b = {to_fun := λ (_x : punit), b, inj' := _}

source

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

α ↪ α × β

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

Equations

function.embedding.sectl α b = {to_fun := λ (a : α), (a, b), inj' := _}

source

def function.embedding.sectr {α : Type u_1} (a : α) (β : Type u_2) :

β ↪ α × β

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

Equations

function.embedding.sectr a β = {to_fun := λ (b : β), (a, b), inj' := _}

source

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

function.embedding.cod_restrict p f H = {to_fun := λ (a : α), ⟨⇑f a, _⟩, inj' := _}

source

@[simp]

theorem function.embedding.cod_restrict_apply {α : Sort u_1} {β : Type u_2} (p : set β) (f : α ↪ β) (H : ∀ (a : α), ⇑f a ∈ p) (a : α) :

⇑(function.embedding.cod_restrict p f H) a = ⟨⇑f a, _⟩

source

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

e₁.prod_map e₂ = {to_fun := prod.map ⇑e₁ ⇑e₂, inj' := _}

source

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

source

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

e₁.sum_map e₂ = {to_fun := sum.map ⇑e₁ ⇑e₂, inj' := _}

source

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

source

def function.embedding.inl {α : Type u_1} {β : Type u_2} :

α ↪ α ⊕ β

The embedding of α into the sum α ⊕ β.

Equations

function.embedding.inl = {to_fun := sum.inl β, inj' := _}

source

def function.embedding.inr {α : Type u_1} {β : Type u_2} :

β ↪ α ⊕ β

The embedding of β into the sum α ⊕ β.

Equations

function.embedding.inr = {to_fun := sum.inr β, inj' := _}

source

@[simp]

theorem function.embedding.sigma_mk_to_fun {α : Type u_1} {β : α → Type u_3} (a : α) (snd : β a) :

⇑(function.embedding.sigma_mk a) snd = ⟨a, snd⟩

source

def function.embedding.sigma_mk {α : Type u_1} {β : α → Type u_3} (a : α) :

β a ↪ Σ (x : α), β x

sigma.mk as an function.embedding.

Equations

function.embedding.sigma_mk a = {to_fun := sigma.mk a, inj' := _}

source

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

source

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

f.sigma_map g = {to_fun := sigma.map ⇑f (λ (a : α), ⇑(g a)), inj' := _}

source

def function.embedding.Pi_congr_right {α : Sort u_1} {β : α → Sort u_2} {γ : α → Sort u_3} (e : Π (a : α), β a ↪ γ a) :

(Π (a : α), β a) ↪ Π (a : α), γ a

Equations

function.embedding.Pi_congr_right e = {to_fun := λ (f : Π (a : α), β a) (a : α), ⇑(e a) (f a), inj' := _}

source

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

(γ → α) ↪ γ → β

Equations

e.arrow_congr_left = function.embedding.Pi_congr_right (λ (_x : γ), e)

source

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

(α → γ) ↪ β → γ

Equations

e.arrow_congr_right = let f' : (α → γ) → β → γ := λ (f : α → γ) (b : β), dite (∃ (c : α), ⇑e c = b) (λ (h : ∃ (c : α), ⇑e c = b), f (classical.some h)) (λ (h : ¬∃ (c : α), ⇑e c = b), default γ) in {to_fun := f', inj' := _}