instCompletelyNormalSpaceOfIsLowerSet

English

If α is a linear order with a lower-set topology, then α is completely normal.

Русский

Если у линейного упорядоченного множества есть топология нижних множеств, то пространство полностью нормальное.

LaTeX

$$$\\text{If } α \\text{ is a linear order with } \\text{Topology.IsLowerSet}(α), \\text{ then } α \\text{ is a CompletelyNormalSpace}$.$$

Lean4

instance (priority := low) {α : Type*} [TopologicalSpace α] [LinearOrder α] [Topology.IsLowerSet α] :
    CompletelyNormalSpace α :=
  inferInstanceAs (CompletelyNormalSpace αᵒᵈ)

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