toHomeomorphClass — Mathlib

English

An isometry class with EquivLike structure yields a HomeomorphClass; forward and inverse maps are continuous, so the maps are homeomorphisms.

Русский

Класс изометрий с структурой EquivLike образует HomeomorphClass; отображения и их обратные непрерывны, следовательно, это гомеоморфизмы.

LaTeX

$$$ \forall f \in F,\; \operatorname{Continuous}(f) \wedge \operatorname{Continuous}(f^{-1}). $$$

Lean4

instance toHomeomorphClass [EquivLike F α β] [IsometryClass F α β] : HomeomorphClass F α β
    where
  map_continuous := IsometryClass.continuous
  inv_continuous f := ((IsometryClass.isometry f).right_inv (EquivLike.right_inv f)).continuous

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