instClosedIciTopologyOrderDual

Mathlib.Topology.Order.OrderClosed

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

English

If α has ClosedIicTopology, then in the order dual α^op, the interval Ici(a) = {x | a ≤ x} is closed.

Русский

Если у α есть замкнутая топология IIC, то в двойственном порядке α^op множество Ici(a) = {x | a ≤ x} замкнуто.

LaTeX

$$IsClosed_{\alpha^{op}}(Ici(a))$$

Lean4

instance : ClosedIciTopology αᵒᵈ where isClosed_Ici _ := isClosed_Iic (α := α)

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

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

Разделы

Аффилиация

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