isClosed_iff_isUpper — Mathlib

English

For a set s in the lower-set topology, s is closed if and only if s is an upper set.

Русский

Для множества s в топологии нижних множеств s замкнуто тогда и только тогда, когда является верхним множеством.

LaTeX

$$$$ \\text{IsClosed}(s) \\iff \\text{IsUpperSet}(s). $$$$

Lean4

theorem isClosed_iff_isUpper : IsClosed s ↔ IsUpperSet s := by
  rw [← isOpen_compl_iff, isOpen_iff_isLowerSet, isUpperSet_compl.symm, compl_compl]

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