eq_empty_of_measure_zero — Mathlib

English

Let μ be an open-positive measure on a topological space X. If U is open and μ(U) = 0, then U = ∅.

Русский

Пусть μ — открыто-положительная мера на топологическом пространстве X. Если U открыто и μ(U) = 0, то U пусто.

LaTeX

$$$\\forall X\\ [TopologicalSpace X],\\forall \\mu:\\;\\mathrm{Measure}(X),\\ [\\mathrm{IsOpenPosMeasure}\\;\\mu],\\forall U\\subset X,\\; \\mathrm{Open}(U) \\Rightarrow \\mu(U)=0 \\Rightarrow U=\\emptyset.$$$

Lean4

/-- An open null set w.r.t. an `IsOpenPosMeasure` is empty. -/
theorem _root_.IsOpen.eq_empty_of_measure_zero (hU : IsOpen U) (h₀ : μ U = 0) : U = ∅ :=
  (hU.measure_eq_zero_iff μ).mp h₀

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