instCompletelyNormalSpaceOfIsUpperSet

English

If α is a linear order with an upper-set topology, then α carries a completely normal topology.

Русский

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

LaTeX

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

Lean4

instance (priority := low) {α : Type*} [TopologicalSpace α] [LinearOrder α] [Topology.IsUpperSet α] :
    CompletelyNormalSpace α where
  completely_normal s t hcst
    hsct := by
    obtain (rfl | ⟨a, ha⟩) := s.eq_empty_or_nonempty
    case inl => simp
    obtain (rfl | ⟨b, hb⟩) := t.eq_empty_or_nonempty
    case inl => simp
    exfalso
    grewrite [← singleton_subset_iff.mpr ha, ← singleton_subset_iff.mpr hb] at hcst hsct
    conv at hcst => equals a < b => simp
    conv at hsct => equals b < a => simp
    exact lt_asymm hcst hsct

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