uniqueEmbeddingEquivResult — Mathlib

English

Embeddings from a single-element type are in bijection with elements of the target type.

Русский

Вложения из типа с одним элементом эквивалентны элементам целевого типа.

LaTeX

$$$(\\alpha \\hookrightarrow \\beta) \\cong \\beta$ при наличии уникального элемента в α$$

Lean4

/-- Embeddings from a single-member type are equivalent to members of the target type. -/
def uniqueEmbeddingEquivResult {α β : Type*} [Unique α] : (α ↪ β) ≃ β
    where
  toFun f := f default
  invFun x := ⟨fun _ => x, fun _ _ _ => Subsingleton.elim _ _⟩
  left_inv
    _ := by
    ext x
    simp_rw [Function.Embedding.coeFn_mk]
    congr 1
    exact Subsingleton.elim _ x
  right_inv _ := by simp

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