interior_eq_empty_iff_dense_compl

English

The interior of s is empty if and only if the complement of s is dense: interior s = ∅ ⇔ Dense sᶜ.

Русский

Внутренность s пустая тогда и только тогда, когда дополнение s плотное: int(s) = ∅ ⇔ Dense sᶜ.

LaTeX

$$$\\\\operatorname{int}(s) = \\\\emptyset \\\\iff \\\\text{Dense}(s^c)$$$

Lean4

theorem interior_eq_empty_iff_dense_compl : interior s = ∅ ↔ Dense sᶜ := by
  rw [dense_iff_closure_eq, closure_compl, compl_univ_iff]

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