Theorems · Theorem · measure theory
AEMeasurable.ennreal_ofReal
∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α},
AEMeasurable f μ → AEMeasurable (fun x => ENNReal.ofReal (f x)) μ- Cited by
- 12 results in Mathlib
- Foundations
- Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement · cited by 9,879
- ENNReal.ofRealstatement · cited by 863
- AEMeasurablestatement and proof · cited by 840
- Continuous.measurableproof · cited by 181
- Measurable.comp_aemeasurableproof · cited by 99
- ENNReal.continuous_ofRealproof · cited by 16
Cited by12
Results whose statement or proof uses this declaration.
- MeasureTheory.tendsto_of_integral_tendsto_of_monotoneproof · cited by 3
- MeasureTheory.lpNorm_eq_integral_norm_rpow_toRealproof · cited by 3
- MeasureTheory.rnDeriv_tilted_leftproof · cited by 2
- MeasureTheory.setLIntegral_tilted'proof · cited by 2
- exists_eq_const_mul_setIntegral_of_ae_nonnegproof · cited by 2
- MeasureTheory.integrable_tilted_iffproof · cited by 1
- MeasureTheory.rnDeriv_tilted_rightproof · cited by 1
- MeasureTheory.condLExp_ofRealproof · cited by 1
- MeasureTheory.integral_tendsto_of_tendsto_of_monotoneproof · cited by 1
- MeasureTheory.isProbabilityMeasure_tiltedproof · cited by 0
- MeasureTheory.setLIntegral_tiltedproof · cited by 0
- MeasureTheory.absolutelyContinuous_tiltedproof · cited by 0