Theorems · Theorem · measure theory
MeasureTheory.SimpleFunc.tsum_eapproxDiff
∀ {α : Type u_1} [inst : MeasurableSpace α] (f : α → ENNReal),
Measurable f → ∀ (a : α), ∑' (n : ℕ), ↑((MeasureTheory.SimpleFunc.eapproxDiff f n) a) = f a- Cited by
- 1 results in Mathlib
- Foundations
- Depth 132 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- MeasurableSpacestatement and proof · cited by 13,106
- ENNRealstatement and proof · cited by 9,879
- NNRealstatement · cited by 4,310
- iSupproof · cited by 2,415
- SummationFilter.unconditionalstatement · cited by 2,068
- Measurablestatement and proof · cited by 1,499
- ENNReal.ofNNRealstatement and proof · cited by 1,279
- tsumstatement · cited by 1,148
- MeasureTheory.SimpleFuncstatement · cited by 411
- Filter.tendsto_add_atTop_natproof · cited by 19
- MeasureTheory.SimpleFunc.iSup_eapprox_applyproof · cited by 8
Cited by1
Results whose statement or proof uses this declaration.
- MeasureTheory.exists_le_lowerSemicontinuous_lintegral_geproof · cited by 2