equiv₂ — Mathlib

English

All denumerable types are equivalent: there exists an equivalence between any two such types.

Русский

Любые две денумерируемые типы эквивалентны: существует эквиваленция между ними.

LaTeX

$$$ \text{equiv}_2(\alpha,\beta) : \alpha \simeq \beta $$$

Lean4

/-- All denumerable types are equivalent. -/
def equiv₂ (α β) [Denumerable α] [Denumerable β] : α ≃ β :=
  (eqv α).trans (eqv β).symm

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