lawsonOpen_iff_scottOpen_of_isUpperSet

English

An upper set is Lawson open if and only if it is Scott open.

Русский

Верхнее множество открыто в Lawson тогда и только тогда, когда оно открыто в Scott.

LaTeX

$$$\forall s:\ Set α,\ IsUpperSet s \rightarrow IsOpen(WithLawson.ofLawson^{-1}' s) \leftrightarrow IsOpen(WithScott.ofScott^{-1}' s)$$$

Lean4

/-- An upper set is Lawson open if and only if it is Scott open -/
theorem lawsonOpen_iff_scottOpen_of_isUpperSet {s : Set α} (h : IsUpperSet s) :
    IsOpen (WithLawson.ofLawson ⁻¹' s) ↔ IsOpen (WithScott.ofScott ⁻¹' s) :=
  ⟨fun hs => IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open (D := univ).mpr ⟨h, (scottHausdorff_le_lawson s) hs⟩,
    lawson_le_scott _⟩

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