instClosedIciTopology

Mathlib.Topology.Order.OrderClosed

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

English

There exists a ClosedIciTopology on α, i.e., the topology makes upper sets closed under the order.

Русский

Существует ClosedIciTopology на α, т.е. окрестности верхних множеств замкнуты по порядку.

LaTeX

$$$\text{ClosedIciTopology }\alpha$$$

Lean4

instance : ClosedIciTopology α where isClosed_Ici _ := isClosed_le continuous_const continuous_id

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

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

Разделы

Аффилиация

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