isOpen_iff_isUpperSet_and_dirSupInaccOn

English

In IsScott α univ, IsOpen s iff IsUpperSet s and DirSupInaccOn univ s.

Русский

В IsScott α univ IsOpen s эквивалентно IsUpperSet s и DirSupInaccOn univ s.

LaTeX

$$$[IsScott\\; \\alpha\\; univ] \\Rightarrow IsOpen(s) \\iff IsUpperSet(s) \\land DirSupInaccOn(\\mathrm{univ},s)$$$

Lean4

theorem isOpen_iff_isUpperSet_and_dirSupInaccOn [IsScott α D] : IsOpen s ↔ IsUpperSet s ∧ DirSupInaccOn D s :=
  by
  rw [isOpen_iff_isUpperSet_and_scottHausdorff_open (D := D)]
  refine
    and_congr_right fun h ↦
      ⟨@IsScottHausdorff.dirSupInaccOn_of_isOpen _ _ _ (scottHausdorff α D) _ _, fun h' d d₀ d₁ d₂ _ d₃ ha ↦ ?_⟩
  obtain ⟨b, hbd, hbu⟩ := h' d₀ d₁ d₂ d₃ ha
  exact ⟨b, hbd, Subset.trans inter_subset_left (h.Ici_subset hbu)⟩

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