isNowhereDense_empty — Mathlib

English

A set s is nowhere dense iff its interior is empty, provided s is closed.

Русский

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

LaTeX

$$$\text{IsClosed } s \implies (\mathrm{IsNowhereDense}(s) \iff \operatorname{int}(s) = \emptyset)$$$

Lean4

/-- The empty set is nowhere dense. -/
@[simp]
theorem isNowhereDense_empty : IsNowhereDense (∅ : Set X) := by rw [IsNowhereDense, closure_empty, interior_empty]

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