measure_iUnion_toMeasurable — Mathlib

English

For any index set, the measure of the union of toMeasurable μ(s_i) equals that of the union of s_i.

Русский

Для любого множества индексов мерa объединения toMeasurable μ(s_i) равна мере объединения s_i.

LaTeX

$$$ \mu\left(\bigcup_i toMeasurable(\mu, s_i)\right) = μ\left(\bigcup_i s_i\right) $$$

Lean4

@[simp]
theorem measure_iUnion_toMeasurable {ι : Sort*} [Countable ι] (s : ι → Set α) :
    μ (⋃ i, toMeasurable μ (s i)) = μ (⋃ i, s i) :=
  Eq.symm <| measure_iUnion_congr_of_subset (fun _i => subset_toMeasurable _ _) fun _i ↦ (measure_toMeasurable _).le

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