isOpen_iff_isUpperSet_and_scottHausdorff_open

English

For IsScott α D, a subset s is open precisely when s is an upper set and DirSupInaccOn D s.

Русский

Для IsScott α D любая подмножество s открыто тогда и только тогда, когда оно является верхним множеством и DirSupInaccOn D s выполняется.

LaTeX

$$$\\text{IsOpen}(s) \\iff \\text{IsUpperSet}(s) \\land \\text{DirSupInaccOn}(D,s)$$$

Lean4

theorem isOpen_iff_isUpperSet_and_scottHausdorff_open [IsScott α D] :
    IsOpen s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s := by rw [topology_eq α D]; rfl

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