Theorems · Theorem · measure theory
Measurable.const_mul
∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f : α → M}
[MeasurableMul M], Measurable f → ∀ (c : M), Measurable fun x => c * f x- Defined in
- Mathlib.MeasureTheory.Group.Arithmetic
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- Measurablestatement and proof · cited by 1,499
- Measurable.compproof · cited by 234
- MeasurableMulstatement and proof · cited by 71
- MeasurableMul.measurable_const_mulproof · cited by 12
Cited by19
Results whose statement or proof uses this declaration.
- Measurable.lintegral_prod_right'proof · cited by 4
- MeasureTheory.Measure.mconv_absolutelyContinuousproof · cited by 3
- MeasureTheory.charFun_map_eq_charFunDual_smulproof · cited by 3
- MeasureTheory.Measure.measurable_lintegralproof · cited by 3
- ProbabilityTheory.measurable_gammaPDFRealproof · cited by 3
- ProbabilityTheory.measurable_uncurry_gaussianPDFRealproof · cited by 3
- integrable_rpow_mul_exp_neg_mul_sqproof · cited by 2
- MeasureTheory.Measure.lintegral_joinproof · cited by 2
- ProbabilityTheory.measurable_cauchyPDFRealproof · cited by 2
- ProbabilityTheory.IndepFun.exp_mulproof · cited by 2
- ProbabilityTheory.measurable_paretoPDFRealproof · cited by 2
- MeasureTheory.measureReal_abs_gt_le_integral_charFunproof · cited by 2