instHomeomorphClass — Mathlib

English

The instance that equips a class of continuous semilinear equivalences with a homeomorph structure asserts each member is a homeomorphism.

Русский

Инстанс, дающий класс непрерывных полускалярных эквивалентностей как структуру гомеоморфизмов, утверждает, что каждый элемент является гомеоморфизмом.

LaTeX

$$$\text{IsOpenMap } e$ for each $e$ in the class; equivalently, $e$ is a homeomorphism.$$

Lean4

instance (priority := 100) [EquivLike F M M₂] [s : ContinuousSemilinearEquivClass F σ M M₂] : HomeomorphClass F M M₂ :=
  { s with }

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