isLocallyClosed_iff_isOpen_coborder

English

For a subset s of a topological space X, s is locally closed if and only if the coborder of s is open.

Русский

Для множества s в топологическом пространстве X: s локально замкнуто тогда и только тогда coborder(s) открыто.

LaTeX

$$$ \mathrm{IsLocallyClosed}(s) \iff \mathrm{IsOpen}(\mathrm{coborder}(s))$$$

Lean4

theorem isLocallyClosed_iff_isOpen_coborder : IsLocallyClosed s ↔ IsOpen (coborder s) :=
  (isLocallyClosed_tfae s).out 0 1

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