scottHausdorff_le_lower — Mathlib

English

For a preorder α, the Scott topology on univ is contained in the given topology (lower).

Русский

Для предупорядочения α скоттовая топология на univ содержится в данной топологии (нижняя).

LaTeX

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

Lean4

theorem scottHausdorff_le_lower : scottHausdorff α univ ≤ lower α := fun s h =>
  IsScottHausdorff.isOpen_of_isLowerSet (t := scottHausdorff α univ) <|
    (@IsLower.isLowerSet_of_isOpen (Topology.WithLower α) _ _ _ s h)

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