English
The Scott topology on α is defined as the join of the upper-set topology and the Scott–Hausdorff topology: scott(α,D) = upperSet α ⊔ scottHausdorff α D.
Русский
Топология Скотта на α определена как объединение топологии верхних множеств и топологии Скотт–Хаусдорф: scott(α,D) = upperSet α ⊔ scottHausdorff α D.
LaTeX
$$$\\mathrm{scott}(\\alpha, D) = \\mathrm{upperSet}(\\alpha) \\;\\sqcup\\; \\mathrm{scottHausdorff}(\\alpha, D)$$$
Lean4
/-- The Scott topology.
It is defined as the join of the topology of upper sets and the Scott-Hausdorff topology. -/
def scott (α : Type*) (D : Set (Set α)) [Preorder α] : TopologicalSpace α :=
upperSet α ⊔ scottHausdorff α D
