instOrderClosedTopologyOrderDual

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#instOrderClosedTopologyOrderDual

English

The order closed topology transfers to the opposite order via a suitable dualization map.

Русский

Топология замкнута по порядку переносится на двойственный порядок через дуальное отображение.

LaTeX

$$$\text{OrderClosedTopology }\alpha^{\mathrm{op}}$$$

Lean4

instance : OrderClosedTopology αᵒᵈ :=
  ⟨(OrderClosedTopology.isClosed_le' (α := α)).preimage continuous_swap⟩

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

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

Разделы

Аффилиация

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