∀ (α : Type u_3) (D : Set (Set α)) [inst : Preorder α],
  Topology.scottHausdorff α D =
    {
      IsOpen := fun u =>
        ∀ ⦃d : Set α⦄,
          d ∈ D →
            d.Nonempty →
              DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ u → ∃ b ∈ d, Set.Ici b ∩ d ⊆ u,
      isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }