forall_measure_inter_spanningSets_eq_zero

English

μ(s) = 0 iff μ(s ∩ spanningSets(μ, n)) = 0 for all n, i.e. vanishing on each finite piece implies vanishing overall.

Русский

μ(s) = 0 тогда и только тогда, когда μ( s ∩ spanningSets(μ, n) ) = 0 для всех n.

LaTeX

$$ (∀ n, μ(s ∩ spanningSets(μ, n)) = 0) ⇔ μ(s) = 0 $$

Lean4

/-- A set in a σ-finite space has zero measure if and only if its intersection with
all members of the countable family of finite measure spanning sets has zero measure. -/
theorem forall_measure_inter_spanningSets_eq_zero [MeasurableSpace α] {μ : Measure α} [SigmaFinite μ] (s : Set α) :
    (∀ n, μ (s ∩ spanningSets μ n) = 0) ↔ μ s = 0 :=
  by
  nth_rw 2 [show s = ⋃ n, s ∩ spanningSets μ n by rw [← inter_iUnion, iUnion_spanningSets, inter_univ]]
  rw [measure_iUnion_null_iff]

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