interior_eq_empty_of_null — Mathlib

English

A null set has empty interior: if μ(s) = 0, then the interior of s is empty.

Русский

Нулевая мера не содержит внутренности: если μ(s) = 0, то interior(s) = ∅.

LaTeX

$$$\\forall s,\\; μ(s) = 0 \\Rightarrow \\mathrm{int}(s) = \\emptyset.$$$

Lean4

/-- A null set has empty interior. -/
theorem interior_eq_empty_of_null (hs : μ s = 0) : interior s = ∅ :=
  isOpen_interior.eq_empty_of_measure_zero <| measure_mono_null interior_subset hs

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