Theorems · Theorem · measure theory
MeasureTheory.SimpleFunc.measurable
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
(f : MeasureTheory.SimpleFunc α β), Measurable ⇑fA simple function is measurable
- Cited by
- 20 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Setproof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- MeasurableSetproof · cited by 3,075
- Measurablestatement · cited by 1,499
- MeasureTheory.SimpleFuncstatement and proof · cited by 411
- MeasureTheory.SimpleFunc.measurableSet_preimageproof · cited by 13
Cited by20
Results whose statement or proof uses this declaration.
- MeasureTheory.StronglyMeasurable.measurableproof · cited by 74
- MeasureTheory.lintegral_const_mulproof · cited by 19
- MeasureTheory.lintegral_iSupproof · cited by 16
- MeasureTheory.lintegral_eq_iSup_eapprox_lintegralproof · cited by 7
- Measurable.ennreal_inductionproof · cited by 7
- Measurable.lintegral_kernel_prod_rightproof · cited by 5
- MeasureTheory.iSup_lintegral_measurable_le_eq_lintegralproof · cited by 4
- MeasureTheory.exists_le_lowerSemicontinuous_lintegral_geproof · cited by 2
- MeasureTheory.lintegral_add_auxproof · cited by 1
- MeasureTheory.Lp.simpleFunc.measurableproof · cited by 1
- intervalIntegral.integrableOn_deriv_right_of_nonnegproof · cited by 1