measure_null_iff_singleton — Mathlib

English

Let s be a set with μ(s) = 0. Then μ(s) = 0 iff every singleton contained in s has zero measure.

Русский

Пусть с — множество с μ(с) = 0. Тогда μ(с) = 0 тогда же, когда μ({x}) = 0 для всех x ∈ с.

LaTeX

$$$\\\\mu(s) = 0 \\\\Longleftrightarrow \\\\forall x\\\\in s,\\\\ \\\\mu({x}) = 0$$$

Lean4

theorem measure_null_iff_singleton (hs : s.Countable) : μ s = 0 ↔ ∀ x ∈ s, μ { x } = 0 := by
  rw [← measure_biUnion_null_iff hs, biUnion_of_singleton]

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