aestronglyMeasurable_iUnion_iff — Mathlib

English

For AEStronglyMeasurable f, restricting to the uIoc(a,b) is equivalent to splitting into Ioc(a,b) and Ioc(b,a).

Русский

Для AEStronglyMeasurable f ограничение на uIoc(a,b) эквивалентно разложению на Ioc(a,b) и Ioc(b,a).

LaTeX

$$$\text{AEStronglyMeasurable}(f, μ.restrict(uIoc(a,b))) \iff \left( \text{AEStronglyMeasurable}(f, μ.restrict(Ioc(a,b))) \wedge \text{AEStronglyMeasurable}(f, μ.restrict(Ioc(b,a))) \right).$$$

Lean4

@[simp]
theorem _root_.aestronglyMeasurable_iUnion_iff [PseudoMetrizableSpace β] {s : ι → Set α} :
    AEStronglyMeasurable f (μ.restrict (⋃ i, s i)) ↔ ∀ i, AEStronglyMeasurable f (μ.restrict (s i)) :=
  ⟨fun h _ => h.mono_measure <| restrict_mono (subset_iUnion _ _) le_rfl, AEStronglyMeasurable.iUnion⟩

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