equivIsoIso — Mathlib

English

Equivalences between types are in a natural sense the same as isomorphisms of types.

Русский

Эквиваленции между типами естественным образом совпадают с изоморфизмами типов.

LaTeX

$$$ \\mathrm{Equiv}(X,Y) \\;\\cong\\; X \\cong Y $$$

Lean4

/-- Equivalences (between types in the same universe) are the same as (isomorphic to) isomorphisms
of types. -/
@[simps]
def equivIsoIso {X Y : Type u} : X ≃ Y ≅ X ≅ Y where
  hom e := e.toIso
  inv i := i.toEquiv

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