isClosed_iff_isLowerSet_and_dirSupClosed

English

If s is closed and α is IsScott univ, then DirSupClosed s holds.

Русский

Если s замкнуто и пространство является IsScott на универсе, то DirSupClosed s выполняется.

LaTeX

$$$[\\text{IsScott }(\\alpha,\\mathrm{univ})] \\Rightarrow \\text{DirSupClosed}(s)$$$

Lean4

theorem isClosed_iff_isLowerSet_and_dirSupClosed [IsScott α univ] : IsClosed s ↔ IsLowerSet s ∧ DirSupClosed s := by
  rw [← isOpen_compl_iff, isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ), isUpperSet_compl, dirSupInaccOn_univ,
    dirSupInacc_compl]

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