instHomeomorphClass

Mathlib.Topology.Order.MonotoneContinuity

URI: https://scilib.ai/kg/mathlib#OrderIso.instHomeomorphClass

English

OrderIso induces a HomeomorphClass structure.

Русский

OrderIso задаёт структуру класса гомеоморфизмов.

LaTeX

$$$\\text{OrderIso }\\alpha\\beta \\Rightarrow \\text{HomeomorphClass}(OrderIso\\alpha\\beta).$$$

Lean4

instance : HomeomorphClass (α ≃o β) α β
    where
  map_continuous := OrderIso.continuous
  inv_continuous e := e.symm.continuous

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru