scottHausdorff_le — Mathlib

English

If IsScott α univ, then the Scott topology is contained in the ambient topology on α.

Русский

Если IsScott α univ, то скоттовская топология содержится в данной топологии на α.

LaTeX

$$$[IsScott\, α\, univ] \Rightarrow (\mathrm{scottHausdorff}(α,\mathrm{univ}) \le \tau_{α}).$$$

Lean4

theorem scottHausdorff_le [IsScott α univ] : scottHausdorff α univ ≤ ‹TopologicalSpace α› := by
  rw [IsScott.topology_eq α univ, scott]; exact le_sup_right

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