mathlib docs: logic.embedding

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 := option.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} :

β → 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} :

β → α ↪ α × β

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 : α ↪ β) :

(∀ (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} :

(α ↪ β) → (γ ↪ δ) → α × γ ↪ β × δ

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

(α ↪ β) → (γ ↪ δ) → α ⊕ γ ↪ β ⊕ δ

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

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.coe_sigma_mk {α : Type u_1} {β : α → Type u_3} (a : α) :

⇑(function.embedding.sigma_mk a) = sigma.mk a

source

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

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

source

@[simp]

theorem function.embedding.coe_sigma_map {α : Type u_1} {α' : Type u_2} {β : α → Type u_3} {β' : α' → Type u_4} (f : α ↪ α') (g : Π (a : α), β a ↪ β' (⇑f a)) :

⇑(f.sigma_map g) = sigma.map ⇑f (λ (a : α), ⇑(g a))

source

def function.embedding.Pi_congr_right {α : Sort u_1} {β : α → Sort u_2} {γ : α → Sort u_3} :

(Π (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} :

(α ↪ β) → (γ → α) ↪ γ → β

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 γ] :

(α ↪ β) → (α → γ) ↪ β → γ

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), inhabited.default γ) in {to_fun := f', inj' := _}