Theorems · Definition · measure theory
MeasureTheory.SimpleFunc.comp
{α : Type u_1} →
{β : Type u_2} →
{γ : Type u_3} →
[inst : MeasurableSpace α] →
[inst_1 : MeasurableSpace β] →
MeasureTheory.SimpleFunc β γ → (g : α → β) → Measurable g → MeasureTheory.SimpleFunc α γComposition of a SimpleFun and a measurable function is a SimpleFunc.
- Cited by
- 14 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.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- MeasurableSpacestatement and proof · cited by 13,106
- Measurablestatement and proof · cited by 1,499
- MeasureTheory.SimpleFuncstatement and proof · cited by 411
Cited by15
Results whose statement or proof uses this declaration.
- MeasureTheory.StronglyMeasurable.comp_measurableproof · cited by 52
- MeasureTheory.SimpleFunc.approxOnproof · cited by 39
- MeasureTheory.lintegral_mapproof · cited by 17
- MeasurableEmbedding.lintegral_mapproof · cited by 10
- MeasureTheory.SimpleFunc.range_comp_subset_rangestatement and proof · cited by 2
- MeasureTheory.setToFun_of_le_map_of_stronglyMeasurableproof · cited by 2
- MeasureTheory.SimpleFunc.lintegral_mapstatement and proof · cited by 2
- MeasureTheory.SimpleFunc.comp.congr_simpstatement and proof · cited by 1
- ProbabilityTheory.strong_law_ae_of_measurableproof · cited by 1
- ProbabilityTheory.strong_law_ae_simpleFunc_compproof · cited by 1
- MeasureTheory.StronglyMeasurable.setToFun_prod_rightproof · cited by 1
- MeasureTheory.SimpleFunc.approxOn_compstatement · cited by 1