English
The Scott-Hausdorff topology on a set of subsets D of α is defined by the property that a set u is open iff whenever the lub of a directed set d lies in u, there is a tail of d contained in u.
Русский
Топология Скотта-Хаусдорфа на наборе подмножеств D \u2261 Set(α) задаётся так, чтобы множество u было открытым тогда и только тогда, когда для любого направленного множества d, чья Н.У.б. лежит в u, существует хвост d, который целиком лежит в u.
LaTeX
$$$\\text{scottHausdorff}(\\alpha,D) : \\text{TopologicalSpace } \\alpha$ with IsOpen(u)\\ is as defined in the theorem$$
Lean4
/-- The Scott-Hausdorff topology.
A set `u` is open in the Scott-Hausdorff topology iff when the least upper bound of a directed set
`d` lies in `u` then there is a tail of `d` which is a subset of `u`. -/
def scottHausdorff (α : Type*) (D : Set (Set α)) [Preorder α] : TopologicalSpace α
where
IsOpen
u :=
∀ ⦃d : Set α⦄, d ∈ D → d.Nonempty → DirectedOn (· ≤ ·) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ u → ∃ b ∈ d, Ici b ∩ d ⊆ u
isOpen_univ := fun d _ ⟨b, hb⟩ _ _ _ _ ↦ ⟨b, hb, (Ici b ∩ d).subset_univ⟩
isOpen_inter s t hs ht d hd₀ hd₁ hd₂ a hd₃
ha := by
obtain ⟨b₁, hb₁d, hb₁ds⟩ := hs hd₀ hd₁ hd₂ hd₃ ha.1
obtain ⟨b₂, hb₂d, hb₂dt⟩ := ht hd₀ hd₁ hd₂ hd₃ ha.2
obtain ⟨c, hcd, hc⟩ := hd₂ b₁ hb₁d b₂ hb₂d
exact ⟨c, hcd, fun e ⟨hce, hed⟩ ↦ ⟨hb₁ds ⟨hc.1.trans hce, hed⟩, hb₂dt ⟨hc.2.trans hce, hed⟩⟩⟩
isOpen_sUnion := fun s h d hd₀ hd₁ hd₂ a hd₃ ⟨s₀, hs₀s, has₀⟩ ↦
by
obtain ⟨b, hbd, hbds₀⟩ := h s₀ hs₀s hd₀ hd₁ hd₂ hd₃ has₀
exact ⟨b, hbd, Set.subset_sUnion_of_subset s s₀ hbds₀ hs₀s⟩
