isOpen_iff_Iic_compl_or_univ — Mathlib

English

In a complete linear order with the Scott topology, an open set is either the whole space or the complement of an initial segment Iic a.

Русский

В полном линейном порядке с топологией Скотта открыто либо всё пространство, либо комплемент начального отрезка Iic a.

LaTeX

$$$\\text{IsOpen}(U) \\iff U = \\mathrm{univ} \\lor \\exists a, (Iic(a))^{c} = U$$$

Lean4

theorem isOpen_iff_Iic_compl_or_univ [TopologicalSpace α] [Topology.IsScott α univ] (U : Set α) :
    IsOpen U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U := by
  constructor
  · intro hU
    rcases eq_empty_or_nonempty Uᶜ with eUc | neUc
    · exact Or.inl (compl_empty_iff.mp eUc)
    · apply Or.inr
      use sSup Uᶜ
      rw [compl_eq_comm, le_antisymm_iff]
      exact
        ⟨fun _ ha ↦ le_sSup ha,
          (isLowerSet_of_isClosed hU.isClosed_compl).Iic_subset
            (dirSupClosed_iff_forall_sSup.mp (dirSupClosed_of_isClosed hU.isClosed_compl) neUc
              (isChain_of_trichotomous Uᶜ).directedOn le_rfl)⟩
  · rintro (rfl | ⟨a, rfl⟩)
    · exact isOpen_univ
    · exact isClosed_Iic.isOpen_compl

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