Theorems · Theorem · measure theory

aemeasurable_sum_measure_iff

∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  [Countable ι] {μ : ι → MeasureTheory.Measure α},
  AEMeasurable f (MeasureTheory.Measure.sum μ) ↔ ∀ (i : ι), AEMeasurable f (μ i)

Defined in: Mathlib.MeasureTheory.Measure.AEMeasurable
Cited by: 1 results in Mathlib
Foundations: Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace Countable

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
AEMeasurablestatement and proof · cited by 840
Countablestatement and proof · cited by 633
MeasureTheory.Measure.sumstatement and proof · cited by 121
AEMeasurable.mono_measureproof · cited by 10
MeasureTheory.Measure.le_sumproof · cited by 9
AEMeasurable.sum_measureproof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

aemeasurable_add_measure_iffproof · cited by 1