Injective functions #

source

ink

structure Function.Embedding (α : Sort u_1) (β : Sort u_2) :

Sort (max(max1u_1)u_2)

An embedding as a function. Use coercion instead.
toFun : α → β
An embedding is an injective function. Use Function.Embedding.injective instead.
inj' : Function.Injective toFun

α ↪ β is a bundled injective function.

Instances For

source

ink

def Function.«term_↪_» :

Lean.TrailingParserDescr

An embedding, a.k.a. a bundled injective function.

Equations

Function.«term_↪_» = Lean.ParserDescr.trailingNode `Function.term_↪_ 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↪ ") (Lean.ParserDescr.cat `term 25))

source

ink

instance Function.instEmbeddingLikeEmbedding {α : Sort u} {β : Sort v} :

EmbeddingLike (α ↪ β) α β

Equations

Function.instEmbeddingLikeEmbedding = EmbeddingLike.mk (_ : ∀ (self : α ↪ β), Function.Injective self.toFun)

source

ink

def Equiv.toEmbedding {α : Sort u} {β : Sort v} (f : α ≃ β) :

α ↪ β

Convert an α ≃ β to α ↪ β.

This is also available as a coercion Equiv.coeEmbedding. The explicit Equiv.toEmbedding 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.toEmbedding = 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.toEmbedding := by simp

Equations

Equiv.toEmbedding f = { toFun := ↑f, inj' := (_ : Function.Injective ↑f) }

source

ink

@[simp]

theorem Equiv.coe_toEmbedding {α : Sort u} {β : Sort v} (f : α ≃ β) :

↑(Equiv.toEmbedding f) = ↑f

source

ink

theorem Equiv.toEmbedding_apply {α : Sort u} {β : Sort v} (f : α ≃ β) (a : α) :

↑(Equiv.toEmbedding f) a = ↑f a

source

ink

instance Equiv.coeEmbedding {α : Sort u} {β : Sort v} :

Coe (α ≃ β) (α ↪ β)

Equations

Equiv.coeEmbedding = { coe := Equiv.toEmbedding }

source

ink

instance Equiv.Perm.coeEmbedding {α : Sort u} :

Coe (Equiv.Perm α) (α ↪ α)

Equations

Equiv.Perm.coeEmbedding = Equiv.coeEmbedding

source

ink

theorem Function.Embedding.coe_injective {α : Sort u_1} {β : Sort u_2} :

Function.Injective fun f => ↑f

source

ink

theorem Function.Embedding.ext {α : Sort u_1} {β : Sort u_2} {f : α ↪ β} {g : α ↪ β} (h : ∀ (x : α), ↑f x = ↑g x) :

f = g

source

ink

theorem Function.Embedding.ext_iff {α : Sort u_1} {β : Sort u_2} {f : α ↪ β} {g : α ↪ β} :

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

source

ink

@[simp]

theorem Function.Embedding.toFun_eq_coe {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) :

f.toFun = ↑f

source

ink

@[simp]

theorem Function.Embedding.coeFn_mk {α : Sort u_1} {β : Sort u_2} (f : α → β) (i : Function.Injective f) :

↑{ toFun := f, inj' := i } = f

source

ink

@[simp]

theorem Function.Embedding.mk_coe {α : Type u_1} {β : Type u_2} (f : α ↪ β) (inj : Function.Injective ↑f) :

{ toFun := ↑f, inj' := inj } = f

source

ink

theorem Function.Embedding.injective {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) :

Function.Injective ↑f

source

ink

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

↑f x = ↑f y ↔ x = y

source

ink

@[simp]

theorem Function.Embedding.refl_apply (α : Sort u_1) (a : α) :

↑(Function.Embedding.refl α) a = a

source

ink

def Function.Embedding.refl (α : Sort u_1) :

α ↪ α

The identity map as a Function.Embedding.

Equations

Function.Embedding.refl α = { toFun := id, inj' := (_ : Function.Injective id) }

source

ink

@[simp]

theorem Function.Embedding.trans_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α ↪ β) (g : β ↪ γ) :

∀ (a : α), ↑(Function.Embedding.trans f g) a = ↑g (↑f a)

source

ink

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

α ↪ γ

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

Equations

Function.Embedding.trans f g = { toFun := ↑g ∘ ↑f, inj' := (_ : Function.Injective (↑g ∘ ↑f)) }

source

ink

instance Function.Embedding.instTransSortSortSortEmbeddingEmbeddingEmbedding :

Trans Function.Embedding Function.Embedding Function.Embedding

Equations

Function.Embedding.instTransSortSortSortEmbeddingEmbeddingEmbedding = { trans := fun {a} {b} {c} => Function.Embedding.trans }

source

ink

@[simp]

theorem Function.Embedding.equiv_toEmbedding_trans_symm_toEmbedding {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) :

Function.Embedding.trans (Equiv.toEmbedding e) (Equiv.toEmbedding (Equiv.symm e)) = Function.Embedding.refl α

source

ink

@[simp]

theorem Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) :

Function.Embedding.trans (Equiv.toEmbedding (Equiv.symm e)) (Equiv.toEmbedding e) = Function.Embedding.refl β

source

ink

@[simp]

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

↑(Function.Embedding.congr e₁ e₂ f) = ↑(Function.Embedding.trans f (Equiv.toEmbedding e₂)) ∘ ↑(Equiv.symm e₁)

source

ink

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 = Function.Embedding.trans (Equiv.toEmbedding (Equiv.symm e₁)) (Function.Embedding.trans f (Equiv.toEmbedding e₂))

source

ink

noncomputable def Function.Embedding.ofSurjective {α : Sort u_1} {β : Sort u_2} (f : β → α) (hf : Function.Surjective f) :

α ↪ β

A right inverse surjInv of a surjective function as an Embedding.

Equations

Function.Embedding.ofSurjective f hf = { toFun := Function.surjInv hf, inj' := (_ : Function.Injective (Function.surjInv hf)) }

source

ink

noncomputable def Function.Embedding.equivOfSurjective {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) (hf : Function.Surjective ↑f) :

α ≃ β

Convert a surjective Embedding to an Equiv

Equations

Function.Embedding.equivOfSurjective f hf = Equiv.ofBijective ↑f (_ : Function.Injective ↑f ∧ Function.Surjective ↑f)

source

ink

def Function.Embedding.ofIsEmpty {α : Sort u_1} {β : Sort u_2} [inst : IsEmpty α] :

α ↪ β

There is always an embedding from an empty type.

Equations

Function.Embedding.ofIsEmpty = { toFun := fun a => isEmptyElim a, inj' := (_ : ∀ (a : α) ⦃a₂ : α⦄, (fun a => isEmptyElim a) a = (fun a => isEmptyElim a) a₂ → a = a₂) }

source

ink

def Function.Embedding.setValue {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) (a : α) (b : β) [inst : (a' : α) → Decidable (a' = a)] [inst : (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

One or more equations did not get rendered due to their size.

source

ink

theorem Function.Embedding.setValue_eq {α : Sort u_1} {β : Sort u_2} (f : α ↪ β) (a : α) (b : β) [inst : (a' : α) → Decidable (a' = a)] [inst : (a' : α) → Decidable (↑f a' = b)] :

↑(Function.Embedding.setValue f a b) a = b

source

ink

@[simp]

theorem Function.Embedding.some_apply {α : Type u_1} :

↑Function.Embedding.some = some

source

ink

def Function.Embedding.some {α : Type u_1} :

α ↪ Option α

Embedding into Option α using some.

Equations

Function.Embedding.some = { toFun := some, inj' := (_ : Function.Injective some) }

source

ink

@[simp]

theorem Function.Embedding.optionMap_apply {α : Type u_1} {β : Type u_2} (f : α ↪ β) :

↑(Function.Embedding.optionMap f) = Option.map ↑f

source

ink

def Function.Embedding.optionMap {α : Type u_1} {β : Type u_2} (f : α ↪ β) :

Option α ↪ Option β

A version of Option.map for Function.Embeddings.

Equations

Function.Embedding.optionMap f = { toFun := Option.map ↑f, inj' := (_ : Function.Injective (Option.map ↑f)) }

source

ink

def Function.Embedding.subtype {α : Sort u_1} (p : α → Prop) :

Subtype p ↪ α

Embedding of a Subtype.

Equations

Function.Embedding.subtype p = { toFun := Subtype.val, inj' := (_ : ∀ (x x_1 : Subtype p), ↑x = ↑x_1 → x = x_1) }

source

ink

@[simp]

theorem Function.Embedding.coe_subtype {α : Sort u_1} (p : α → Prop) :

↑(Function.Embedding.subtype p) = Subtype.val

source

ink

noncomputable def Function.Embedding.quotientOut (α : Sort u_1) [s : Setoid α] :

Quotient s ↪ α

Quotient.out as an embedding.

Equations

Function.Embedding.quotientOut α = { toFun := Quotient.out, inj' := (_ : Function.Injective Quotient.out) }

source

ink

@[simp]

theorem Function.Embedding.coe_quotientOut (α : Sort u_1) [inst : Setoid α] :

↑(Function.Embedding.quotientOut α) = Quotient.out

source

ink

def Function.Embedding.punit {β : Sort u_1} (b : β) :

PUnit ↪ β

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

Equations

Function.Embedding.punit b = { toFun := fun x => b, inj' := (_ : ∀ ⦃a₁ a₂ : PUnit⦄, (fun x => b) a₁ = (fun x => b) a₂ → a₁ = a₂) }

source

ink

@[simp]

theorem Function.Embedding.sectl_apply (α : Type u_1) {β : Type u_2} (b : β) (a : α) :

↑(Function.Embedding.sectl α b) a = (a, b)

source

ink

def Function.Embedding.sectl (α : Type u_1) {β : Type u_2} (b : β) :

α ↪ α × β

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

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Function.Embedding.sectr_apply {α : Type u_1} (a : α) (β : Type u_2) (b : β) :

↑(Function.Embedding.sectr a β) b = (a, b)

source

ink

def Function.Embedding.sectr {α : Type u_1} (a : α) (β : Type u_2) :

β ↪ α × β

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

Equations

One or more equations did not get rendered due to their size.

source

ink

def Function.Embedding.prodMap {α : 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

Function.Embedding.prodMap e₁ e₂ = { toFun := Prod.map ↑e₁ ↑e₂, inj' := (_ : Function.Injective (Prod.map ↑e₁ ↑e₂)) }

source

ink

@[simp]

theorem Function.Embedding.coe_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α ↪ β) (e₂ : γ ↪ δ) :

↑(Function.Embedding.prodMap e₁ e₂) = Prod.map ↑e₁ ↑e₂

source

ink

def Function.Embedding.pprodMap {α : 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

Function.Embedding.pprodMap e₁ e₂ = { toFun := fun x => { fst := ↑e₁ x.fst, snd := ↑e₂ x.snd }, inj' := (_ : Function.Injective fun x => { fst := ↑e₁ x.fst, snd := ↑e₂ x.snd }) }

source

ink

def Function.Embedding.sumMap {α : 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

Function.Embedding.sumMap e₁ e₂ = { toFun := Sum.map ↑e₁ ↑e₂, inj' := (_ : Function.Injective (Sum.map ↑e₁ ↑e₂)) }

source

ink

@[simp]

theorem Function.Embedding.coe_sumMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α ↪ β) (e₂ : γ ↪ δ) :

↑(Function.Embedding.sumMap e₁ e₂) = Sum.map ↑e₁ ↑e₂

source

ink

@[simp]

theorem Function.Embedding.inl_apply {α : Type u_1} {β : Type u_2} (val : α) :

↑Function.Embedding.inl val = Sum.inl val

source

ink

def Function.Embedding.inl {α : Type u_1} {β : Type u_2} :

α ↪ α ⊕ β

The embedding of α into the sum α ⊕ β.

Equations

Function.Embedding.inl = { toFun := Sum.inl, inj' := (_ : ∀ (x x_1 : α), Sum.inl x = Sum.inl x_1 → x = x_1) }

source

ink

@[simp]

theorem Function.Embedding.inr_apply {α : Type u_1} {β : Type u_2} (val : β) :

↑Function.Embedding.inr val = Sum.inr val

source

ink

def Function.Embedding.inr {α : Type u_1} {β : Type u_2} :

β ↪ α ⊕ β

The embedding of β into the sum α ⊕ β.

Equations

Function.Embedding.inr = { toFun := Sum.inr, inj' := (_ : ∀ (x x_1 : β), Sum.inr x = Sum.inr x_1 → x = x_1) }

source

ink

@[simp]

theorem Function.Embedding.sigmaMk_apply {α : Type u_1} {β : α → Type u_2} (a : α) (snd : β a) :

↑(Function.Embedding.sigmaMk a) snd = { fst := a, snd := snd }

source

ink

def Function.Embedding.sigmaMk {α : Type u_1} {β : α → Type u_2} (a : α) :

β a ↪ (x : α) × β x

Sigma.mk as an Function.Embedding.

Equations

Function.Embedding.sigmaMk a = { toFun := Sigma.mk a, inj' := (_ : Function.Injective (Sigma.mk a)) }

source

ink

@[simp]

theorem Function.Embedding.sigmaMap_apply {α : Type u_1} {α' : Type u_2} {β : α → Type u_3} {β' : α' → Type u_4} (f : α ↪ α') (g : (a : α) → β a ↪ β' (↑f a)) (x : (a : α) × β a) :

↑(Function.Embedding.sigmaMap f g) x = Sigma.map (↑f) (fun a => ↑(g a)) x

source

ink

def Function.Embedding.sigmaMap {α : 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

Function.Embedding.sigmaMap f g = { toFun := Sigma.map ↑f fun a => ↑(g a), inj' := (_ : Function.Injective (Sigma.map ↑f fun a => ↑(g a))) }

source

ink

@[simp]

theorem Function.Embedding.piCongrRight_apply {α : Sort u_1} {β : α → Sort u_2} {γ : α → Sort u_3} (e : (a : α) → β a ↪ γ a) (f : (a : α) → β a) (a : α) :

↑(Function.Embedding.piCongrRight e) f a = ↑(e a) (f a)

source

ink

def Function.Embedding.piCongrRight {α : 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.piCongrRight e = { toFun := fun f a => ↑(e a) (f a), inj' := (_ : ∀ (x x_1 : (a : α) → β a), (fun f a => ↑(e a) (f a)) x = (fun f a => ↑(e a) (f a)) x_1 → x = x_1) }

source

ink

def Function.Embedding.arrowCongrRight {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) :

(γ → α) ↪ γ → β

An embedding e : α ↪ β defines an embedding (γ → α) ↪ (γ → β) that sends each f to e ∘ f.

Equations

Function.Embedding.arrowCongrRight e = Function.Embedding.piCongrRight fun x => e

source

ink

@[simp]

theorem Function.Embedding.arrowCongrRight_apply {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ↪ β) (f : γ ↪ α) :

↑(Function.Embedding.arrowCongrRight e) ↑f = ↑e ∘ ↑f

source

ink

noncomputable def Function.Embedding.arrowCongrLeft {α : Sort u} {β : Sort v} {γ : Sort w} [inst : 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

One or more equations did not get rendered due to their size.

source

ink

def Function.Embedding.subtypeMap {α : 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

Function.Embedding.subtypeMap f h = { toFun := Subtype.map (↑f) h, inj' := (_ : Function.Injective (Subtype.map (fun a => ↑f a) h)) }

source

ink

theorem Function.Embedding.swap_apply {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] (f : α ↪ β) (x : α) (y : α) (z : α) :

↑(Equiv.swap (↑f x) (↑f y)) (↑f z) = ↑f (↑(Equiv.swap x y) z)

source

ink

theorem Function.Embedding.swap_comp {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst : DecidableEq β] (f : α ↪ β) (x : α) (y : α) :

↑(Equiv.swap (↑f x) (↑f y)) ∘ ↑f = ↑f ∘ ↑(Equiv.swap x y)

source

ink

@[simp]

theorem Equiv.asEmbedding_apply {β : Sort u_1} {α : Sort u_2} {p : β → Prop} (e : α ≃ Subtype p) :

∀ (a : α), ↑(Equiv.asEmbedding e) a = ↑(↑e a)

source

ink

def Equiv.asEmbedding {β : Sort u_1} {α : Sort u_2} {p : β → Prop} (e : α ≃ Subtype p) :

α ↪ β

Given an equivalence to a subtype, produce an embedding to the elements of the corresponding set.

Equations

Equiv.asEmbedding e = Function.Embedding.trans (Equiv.toEmbedding e) (Function.Embedding.subtype p)

source

ink

def Equiv.subtypeInjectiveEquivEmbedding (α : Sort u_1) (β : Sort u_2) :

{ f // Function.Injective f } ≃ (α ↪ β)

The type of embeddings α ↪ β is equivalent to the subtype of all injective functions α → β.

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

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

↑(Equiv.embeddingCongr h h') f = Function.Embedding.congr h h' f

source

ink

def Equiv.embeddingCongr {α : 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

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem Equiv.embeddingCongr_refl {α : Sort u_1} {β : Sort u_2} :

Equiv.embeddingCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ↪ β)

source

ink

@[simp]

theorem Equiv.embeddingCongr_trans {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} {α₃ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ ≃ α₂) (e₁' : β₁ ≃ β₂) (e₂ : α₂ ≃ α₃) (e₂' : β₂ ≃ β₃) :

Equiv.embeddingCongr (Equiv.trans e₁ e₂) (Equiv.trans e₁' e₂') = Equiv.trans (Equiv.embeddingCongr e₁ e₁') (Equiv.embeddingCongr e₂ e₂')

source

ink

@[simp]

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

Equiv.symm (Equiv.embeddingCongr e₁ e₂) = Equiv.embeddingCongr (Equiv.symm e₁) (Equiv.symm e₂)

source

ink

theorem Equiv.embeddingCongr_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 : β₁ ↪ γ₁) :

↑(Equiv.embeddingCongr ea ec) (Function.Embedding.trans f g) = Function.Embedding.trans (↑(Equiv.embeddingCongr ea eb) f) (↑(Equiv.embeddingCongr eb ec) g)

source

ink

@[simp]

theorem Equiv.refl_toEmbedding {α : Type u_1} :

Equiv.toEmbedding (Equiv.refl α) = Function.Embedding.refl α

source

ink

@[simp]

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

Equiv.toEmbedding (Equiv.trans e f) = Function.Embedding.trans (Equiv.toEmbedding e) (Equiv.toEmbedding f)

source

ink

def subtypeOrLeftEmbedding {α : Type u_1} (p : α → Prop) (q : α → Prop) [inst : DecidablePred 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

One or more equations did not get rendered due to their size.

source

ink

theorem subtypeOrLeftEmbedding_apply_left {α : Type u_1} {p : α → Prop} {q : α → Prop} [inst : DecidablePred p] (x : { x // p x ∨ q x }) (hx : p ↑x) :

↑(subtypeOrLeftEmbedding p q) x = Sum.inl { val := ↑x, property := hx }

source

ink

theorem subtypeOrLeftEmbedding_apply_right {α : Type u_1} {p : α → Prop} {q : α → Prop} [inst : DecidablePred p] (x : { x // p x ∨ q x }) (hx : ¬p ↑x) :

↑(subtypeOrLeftEmbedding p q) x = Sum.inr { val := ↑x, property := Or.resolve_left (_ : p ↑x ∨ q ↑x) hx }

source

ink

@[simp]

theorem Subtype.impEmbedding_apply_coe {α : Type u_1} (p : α → Prop) (q : α → Prop) (h : (x : α) → p x → q x) (x : { x // p x }) :

↑(↑(Subtype.impEmbedding p q h) x) = ↑x

source

ink

def Subtype.impEmbedding {α : Type u_1} (p : α → Prop) (q : α → Prop) (h : (x : α) → p x → q x) :

{ 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

One or more equations did not get rendered due to their size.