logic.embedding - mathlib docs

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

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

source

@[protected, instance]

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

has_coe (α ≃ β) (α ↪ β)

Equations

equiv.coe_embedding = {coe := equiv.to_embedding β}

source

@[protected, instance]

def equiv.perm.coe_embedding {α : Sort u} :

has_coe (equiv.perm α) (α ↪ α)

Equations

equiv.perm.coe_embedding = equiv.coe_embedding

source

@[simp]

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

↑f = f.to_embedding

source

@[simp]

theorem equiv.as_embedding_apply {α : Sort u} {β : Sort v} {p : β → Prop} (e : α ≃ subtype p) (ᾰ : α) :

⇑(e.as_embedding) ᾰ = (coe ∘ ⇑e) ᾰ

source

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

e.as_embedding = {to_fun := coe ∘ ⇑e, inj' := _}

source

@[simp]

theorem equiv.as_embedding_range {α : Sort u_1} {β : Type u_2} {p : β → Prop} (e : α ≃ subtype p) :

set.range ⇑(e.as_embedding) = set_of p

source

theorem function.embedding.coe_injective {α : Sort u_1} {β : Sort u_2} :

function.injective coe_fn

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

@[simp]

theorem function.embedding.mk_coe {α : Type u_1} {β : Type u_2} (f : α ↪ β) (inj : function.injective ⇑f) :

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

source

@[protected]

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

function.injective ⇑f

source

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

⇑f x = ⇑f y ↔ x = y

source

@[protected]

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

α ↪ α

The identity map as a function.embedding.

Equations

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

source

@[simp]

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

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

source

@[protected]

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

α ↪ γ

Composition of f : α ↪ β and g : β ↪ γ.

Equations

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

source

@[simp]

theorem function.embedding.trans_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α ↪ β) (g : β ↪ γ) (ᾰ : α) :

⇑(f.trans g) ᾰ = ⇑g (⇑f ᾰ)

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

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

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

source

@[simp]

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

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

source

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

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

source

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

f.equiv_of_surjective hf = equiv.of_bijective ⇑f _

source

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

function.embedding.of_is_empty = {to_fun := is_empty_elim (λ (a : α), β), 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

@[protected]

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

α ↪ option α

Embedding into option α using some.

Equations

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

source

@[simp]

theorem function.embedding.some_apply {α : Type u_1} :

⇑function.embedding.some = some

source

@[simp]

theorem function.embedding.coe_option_apply {α : Type u_1} :

⇑function.embedding.coe_option = coe

source

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

α ↪ option α

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

Equations

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

source

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

α ↪ with_top α

Embedding into with_top α.

Equations

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

source

@[simp]

theorem function.embedding.coe_with_top_apply {α : Type u_1} (ᾰ : α) :

⇑function.embedding.coe_with_top ᾰ = ↑ᾰ

source

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

f.option_elim x h = {to_fun := λ (o : option α), o.elim x ⇑f, inj' := _}

source

@[simp]

theorem function.embedding.option_elim_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (x : β) (h : x ∉ set.range ⇑f) (o : option α) :

⇑(f.option_elim x h) o = o.elim x ⇑f

source

@[simp]

theorem function.embedding.option_embedding_equiv_apply_fst (α : Type u_1) (β : Type u_2) (f : option α ↪ β) :

(⇑(function.embedding.option_embedding_equiv α β) f).fst = function.embedding.coe_option.trans f

source

@[simp]

theorem function.embedding.option_embedding_equiv_symm_apply (α : Type u_1) (β : Type u_2) (f : Σ (f : α ↪ β), ↥(set.range ⇑f)ᶜ) :

⇑((function.embedding.option_embedding_equiv α β).symm) f = f.fst.option_elim ↑(f.snd) _

source

@[simp]

theorem function.embedding.option_embedding_equiv_apply_snd_coe (α : Type u_1) (β : Type u_2) (f : option α ↪ β) :

↑((⇑(function.embedding.option_embedding_equiv α β) f).snd) = ⇑f none

source

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

function.embedding.option_embedding_equiv α β = {to_fun := λ (f : option α ↪ β), ⟨function.embedding.coe_option.trans f, ⟨⇑f none, _⟩⟩, inv_fun := λ (f : Σ (f : α ↪ β), ↥(set.range ⇑f)ᶜ), f.fst.option_elim ↑(f.snd) _, left_inv := _, right_inv := _}

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

e₁.pprod_map e₂ = {to_fun := λ (x : pprod α γ), ⟨⇑e₁ x.fst, ⇑e₂ x.snd⟩, inj' := _}

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

@[simp]

theorem function.embedding.inl_apply {α : Type u_1} {β : Type u_2} (val : α) :

⇑function.embedding.inl val = sum.inl val

source

@[simp]

theorem function.embedding.inr_apply {α : Type u_1} {β : Type u_2} (val : β) :

⇑function.embedding.inr val = sum.inr val

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_apply {α : 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_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

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

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

⇑(function.embedding.Pi_congr_right e) f a = ⇑(e a) (f a)

source

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

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

source

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

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

source

@[simp]

theorem function.embedding.arrow_congr_right_apply {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) (f : γ ↪ α) :

⇑(e.arrow_congr_right) ⇑f = ⇑e ∘ ⇑f

source

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

e.arrow_congr_left = {to_fun := λ (f : α → γ), function.extend ⇑e f (λ (_x : β), default), inj' := _}

source

@[protected]

def function.embedding.subtype_map {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α ↪ β) (h : ∀ ⦃x : α⦄, p x → q (⇑f x)) :

{x // p x} ↪ {y // q y}

Restrict both domain and codomain of an embedding.

Equations

f.subtype_map h = {to_fun := subtype.map ⇑f h, inj' := _}

source

@[protected]

def function.embedding.image {α : Type u_1} {β : Type u_2} (f : α ↪ β) :

set α ↪ set β

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

Equations

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

source

@[simp]

theorem function.embedding.image_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : set α) :

⇑(f.image) s = ⇑f '' s

source

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)

source

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 ∘ ⇑(equiv.swap x y)

source

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

equiv.subtype_injective_equiv_embedding α β = {to_fun := λ (f : {f // function.injective f}), {to_fun := f.val, inj' := _}, inv_fun := λ (f : α ↪ β), ⟨⇑f, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.embedding_congr_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (h : α ≃ β) (h' : γ ≃ δ) (f : α ↪ γ) :

⇑(h.embedding_congr h') f = function.embedding.congr h h' f

source

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

h.embedding_congr h' = {to_fun := λ (f : α ↪ γ), function.embedding.congr h h' f, inv_fun := λ (f : β ↪ δ), function.embedding.congr h.symm h'.symm f, left_inv := _, right_inv := _}

source

@[simp]

theorem equiv.embedding_congr_refl {α : Sort u_1} {β : Sort u_2} :

(equiv.refl α).embedding_congr (equiv.refl β) = equiv.refl (α ↪ β)

source

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

source

@[simp]

theorem equiv.embedding_congr_symm {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂) :

(e₁.embedding_congr e₂).symm = e₁.symm.embedding_congr e₂.symm

source

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

⇑(ea.embedding_congr ec) (f.trans g) = (⇑(ea.embedding_congr eb) f).trans (⇑(eb.embedding_congr ec) g)

source

@[simp]

theorem equiv.refl_to_embedding {α : Type u_1} :

(equiv.refl α).to_embedding = function.embedding.refl α

source

@[simp]

theorem equiv.trans_to_embedding {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ) :

(e.trans f).to_embedding = e.to_embedding.trans f.to_embedding

source

def set.embedding_of_subset {α : Type u_1} (s t : set α) (h : s ⊆ t) :

↥s ↪ ↥t

The injection map is an embedding between subsets.

Equations

s.embedding_of_subset t h = {to_fun := λ (x : ↥s), ⟨x.val, _⟩, inj' := _}

source

@[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, _⟩

source

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

subtype_or_left_embedding p q = {to_fun := λ (x : {x // p x ∨ q x}), dite (p ↑x) (λ (h : p ↑x), sum.inl ⟨↑x, h⟩) (λ (h : ¬p ↑x), sum.inr ⟨↑x, _⟩), inj' := _}

source

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

⇑(subtype_or_left_embedding p q) x = sum.inl ⟨↑x, hx⟩

source

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

⇑(subtype_or_left_embedding p q) x = sum.inr ⟨↑x, _⟩

source

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

subtype.imp_embedding p q h = {to_fun := λ (x : {x // p x}), ⟨↑x, _⟩, inj' := _}

source

@[simp]

theorem subtype.imp_embedding_apply_coe {α : Type u_1} (p q : α → Prop) (h : p ≤ q) (x : {x // p x}) :

↑(⇑(subtype.imp_embedding p q h) x) = ↑x

source

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

subtype_or_equiv p q h = {to_fun := ⇑(subtype_or_left_embedding p q), inv_fun := sum.elim ⇑(subtype.imp_embedding (λ (x : α), p x) (λ (x : α), p x ∨ q x) _) ⇑(subtype.imp_embedding (λ (x : α), q x) (λ (x : α), p x ∨ q x) _), left_inv := _, right_inv := _}

source

@[simp]

theorem subtype_or_equiv_apply {α : Type u_1} (p q : α → Prop) [decidable_pred p] (h : disjoint p q) (ᾰ : {x // p x ∨ q x}) :

⇑(subtype_or_equiv p q h) ᾰ = ⇑(subtype_or_left_embedding p q) ᾰ

source

@[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, _⟩

source

@[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, _⟩

mathlib documentation

Injective functions #