oneEmbeddingEquiv — Mathlib

English

There is an equivalence between the unit type embeddings into α and α itself, given a Unique one.

Русский

Существует эквиваленция между вложением единицы в α и самим α, если единица уникальна.

LaTeX

$$$\\mathrm{oneEmbeddingEquiv} : (1 \\hookrightarrow \\alpha) \\simeq \\alpha$$$

Lean4

/-- The equivalence `one ↪ α` with `α`, for `Unique one`. -/
def oneEmbeddingEquiv {one α : Type*} [Unique one] : (one ↪ α) ≃ α
    where
  toFun f := f default
  invFun
    a :=
    { toFun := fun _ ↦ a
      inj' x y h := by simp [Unique.uniq inferInstance] }
  left_inv f := by ext; simp [Unique.uniq]

Похожие утверждения