English
In an IsScott α D space, a set s is open precisely when, for every d ∈ D that is nonempty and directed, whenever a is a lub of d and a ∈ s, there exists b ∈ d with (d ∩ [b, ∞)) ⊆ s.
Русский
В пространстве IsScott α D множество s открыто тогда и только тогда, для всякого d ∈ D, не пустого и направленного, если a является верхней границей d и a ∈ s, то существует b ∈ d такое, что d ∩ [b, ∞) ⊆ s.
LaTeX
$$$\\text{IsOpen}(s) \\iff \\forall d\\,(d \\in D \\land d\\text{Nonempty} \\land \\text{DirectedOn}(\\le) d)\\;\\forall a:\\alpha\\;\\text{IsLUB}(d,a) \\land a \\in s \\Rightarrow \\exists b\\in d,\\; (d\\cap \\{x: x \\ge b\\}) \\subseteq s$$$
Lean4
theorem isOpen_iff [IsScottHausdorff α D] :
IsOpen s ↔
∀ ⦃d : Set α⦄,
d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s :=
by simp [topology_eq_scottHausdorff (α := α) (D := D), IsOpen, scottHausdorff]
