aestronglyMeasurable_add_measure_iff

English

For AEStronglyMeasurable f, AEStronglyMeasurable with respect to μ + ν is equivalent to AEStronglyMeasurable with respect to μ and to ν separately.

Русский

Для функции f равномерно AEStronglyMeasurable относительно суммы мер μ+ν эквивалентно AEStronglyMeasurable относительно μ и относительно ν по отдельности.

LaTeX

$$$\text{AEStronglyMeasurable}(f, μ+ν) \iff (\text{AEStronglyMeasurable}(f, μ) \land \text{AEStronglyMeasurable}(f, ν)).$$$

Lean4

@[simp]
theorem _root_.aestronglyMeasurable_add_measure_iff [PseudoMetrizableSpace β] {ν : Measure α} :
    AEStronglyMeasurable f (μ + ν) ↔ AEStronglyMeasurable f μ ∧ AEStronglyMeasurable f ν :=
  by
  rw [← sum_cond, aestronglyMeasurable_sum_measure_iff, Bool.forall_bool, and_comm]
  rfl

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