of_isClosed_null — Mathlib

English

Let s be a subset of a topological measure space that is closed and has measure zero. Then s is nowhere dense (its closure has empty interior).

Русский

Пусть s — множество в топологическом пространстве с мерой; если s замкнуто и μ(s) = 0, то s нигде не плотное (его замыкание имеет пустое interior).

LaTeX

$$$\bigl( \text{Closed}(s) \land \mu(s) = 0 \bigr) \Rightarrow \text{IsNowhereDense}(s)$$$

Lean4

/-- A *closed* measure zero subset is nowhere dense. (Closedness is required: for instance, the
rational numbers are countable (thus have measure zero), but are dense (hence not nowhere dense). -/
theorem of_isClosed_null (h₁s : IsClosed s) (h₂s : μ s = 0) : IsNowhereDense s :=
  h₁s.isNowhereDense_iff.mpr (interior_eq_empty_of_null h₂s)

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