instHomeomorphClass — Mathlib

English

The type of continuous affine equivalences is a HomeomorphClass: maps are continuous with respect to the forward and inverse components.

Русский

Тип непрерывных аффинных эквивалентов образует класс гомоморфизмов-гомеоморфизмов: отображения непрерывны и их обратные отображения непрерывны.

LaTeX

$$$\\text{HomeomorphClass}((P_1 \\simeq_A^k P_2), P_1, P_2)$$$

Lean4

instance : HomeomorphClass (P₁ ≃ᴬ[k] P₂) P₁ P₂
    where
  map_continuous f := f.continuous_toFun
  inv_continuous f := f.continuous_invFun

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