sum_apply_eq_zero' — Mathlib

English

If S is a measurable set, then sum μ S = 0 iff μ_i S = 0 for all i.

Русский

Для измеримого множества S равенство сумме равного нулю эквивалентно тому, что для всех i μ_i(S) = 0.

LaTeX

$$$ (\sum_i μ_i)(S) = 0 \iff \forall i, μ_i(S) = 0 $$$

Lean4

theorem sum_apply_eq_zero' {μ : ι → Measure α} {s : Set α} (hs : MeasurableSet s) : sum μ s = 0 ↔ ∀ i, μ i s = 0 := by
  simp [hs]

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