isOpen_iff_isUpperSet_and_scottHausdorff_open'

English

For any α with preorder, any u ⊆ α satisfies IsOpen((ofScott)^{-1}(u)) iff IsUpperSet(u) and IsOpen in scottHausdorff.

Русский

Для любого α с предупорядочением для множества u ⊆ α верно: IsOpen(ofScott^{-1}(u)) тогда и только тогда, когда u — верхнее множество и оно открыто в скоттовой гом topology.

LaTeX

$$$ IsOpen(\mathrm{ofScott}^{-1}(u)) \iff IsUpperSet(u) \land (\mathrm{scottHausdorff}(\alpha,\mathrm{univ})).IsOpen(u).$$$

Lean4

theorem isOpen_iff_isUpperSet_and_scottHausdorff_open' {u : Set α} :
    IsOpen (WithScott.ofScott ⁻¹' u) ↔ IsUpperSet u ∧ (scottHausdorff α univ).IsOpen u :=
  Iff.rfl

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