coborder_eq_univ_iff — Mathlib

English

The coborder of a set s equals the whole space if and only if s is closed.

Русский

Граница coborder множества s равна всему пространству тогда и только тогда, когда s замкнуто.

LaTeX

$$$\operatorname{coborder}(s) = \operatorname{univ} \iff \text{IsClosed}(s)$$

Lean4

theorem coborder_eq_univ_iff : coborder s = univ ↔ IsClosed s := by
  simp [coborder, diff_eq_empty, closure_subset_iff_isClosed]

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