toEquiv — Mathlib

English

There is a natural equivalence between a type and its specialization, given by the identity map.

Русский

Существует естественное эквивалентное отображение между типом и его специализацией, задаваемое идентичностью.

LaTeX

$$$\text{toEquiv}: \alpha \simeq \text{Specialization}(\alpha)\quad\text{is the identity equivalence.}$$$

Lean4

/-- `toEquiv` is the "identity" function to the `Specialization` of a type. -/
@[match_pattern]
def toEquiv : α ≃ Specialization α :=
  Equiv.refl _

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