equivEquivIso — Mathlib

English

Equivalences between types are in bijection with isomorphisms; this yields an equivalence equivEquivIso: X ≃ Y ≃ (X ≅ Y).

Русский

Эквиваленции между типами соответствуют изоморфизмам; образуется эквивалентность equivEquivIso: X ≃ Y ≃ (X ≅ Y).

LaTeX

$$$ X \\simeq Y \\simeq (X \\cong Y) $$$

Lean4

/-- Equivalences (between types in the same universe) are the same as (equivalent to) isomorphisms
of types. -/
def equivEquivIso {X Y : Type u} : X ≃ Y ≃ (X ≅ Y) :=
  equivIsoIso.toEquiv

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