iUnion — Mathlib

English

AEStronglyMeasurable of f restricted to the union equals AEStronglyMeasurable restricted to each s_i, i.e., equivalence between the union and all the pieces.

Русский

AEStronglyMeasurable функции f на объединении равносильно AEStronglyMeasurable на каждом s_i.

LaTeX

$$$\text{AEStronglyMeasurable}(f, μ.restrict(\bigcup_i s_i)) \iff \forall i, \text{AEStronglyMeasurable}(f, μ.restrict(s_i)).$$$

Lean4

@[fun_prop, measurability]
protected theorem iUnion [PseudoMetrizableSpace β] {s : ι → Set α}
    (h : ∀ i, AEStronglyMeasurable f (μ.restrict (s i))) : AEStronglyMeasurable f (μ.restrict (⋃ i, s i)) :=
  (sum_measure h).mono_measure <| restrict_iUnion_le

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