isOpen_iff_isLowerSet

Mathlib.Topology.Order.UpperLowerSetTopology

URI: https://scilib.ai/kg/mathlib#Topology.IsLowerSet.isOpen_iff_isLowerSet

English

In the lower-set topology, a subset is open if and only if it is a lower set.

Русский

В топологии нижних множеств подмножество открыто тогда и только тогда, когда оно является нижним множеством.

LaTeX

$$$$ \\text{IsOpen}(s) \\iff \\text{IsLowerSet}(s). $$$$

Lean4

theorem isOpen_iff_isLowerSet : IsOpen s ↔ IsLowerSet s := by rw [topology_eq α]; rfl

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

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

Разделы

Аффилиация

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