instHomeomorphClass — Mathlib

English

The class of continuous multiplicative equivalences between M and N is a HomeomorphClass: maps are continuous and their inverses are continuous.

Русский

Класс непрерывных мультипликативных эквивалентов между M и N образует HomeomorphClass: отображения непрерывны, их обратные также непрерывны.

LaTeX

$$$\text{HomeomorphClass}(\mathrm{ContinuousMulEquiv}\,M\,N)\;M\;N,\quad \text{map\_continuous}(f)=f.\mathrm{continuous\_toFun},\quad \text{inv\_continuous}(f)=f.\mathrm{continuous\_invFun}.$$$

Lean4

@[to_additive]
instance : HomeomorphClass (M ≃ₜ* N) M N
    where
  map_continuous f := f.continuous_toFun
  inv_continuous f := f.continuous_invFun

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