instClosedIicTopology

Mathlib.Topology.Order.OrderClosed

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

English

There exists a ClosedIicTopology on α, i.e., the topology is such that all sets of the form {x ≤ y} are closed under the order.

Русский

Существуют замкнутые снизу интервалы в α, задающие ClosedIicTopology.

LaTeX

$$$\text{ClosedIicTopology }\alpha$$$

Lean4

instance : ClosedIicTopology α where isClosed_Iic _ := isClosed_le continuous_id continuous_const

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

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

Разделы

Аффилиация

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