scottHausdorff_le_scott — Mathlib

English

The Scott–Hausdorff topology on univ is contained in the Scott topology on univ: scottHausdorff α univ ≤ scott α univ.

Русский

Топология Scott–Hausdorff на множестве единиц входит в топологию Скотта на том же множестве: scottHausdorff α univ ≤ scott α univ.

LaTeX

$$$\\mathrm{scottHausdorff}(\\alpha,\\mathrm{univ}) \\le \\mathrm{scott}(\\alpha,\\mathrm{univ})$$$

Lean4

theorem scottHausdorff_le_scott [Preorder α] : scottHausdorff α univ ≤ scott α univ :=
  le_sup_right

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