Theorems · Theorem · measure theory
measurable_pi_lambda
∀ {α : Type u_1} {δ : Type u_4} {X : δ → Type u_6} [inst : MeasurableSpace α] [inst_1 : (a : δ) → MeasurableSpace (X a)]
(f : α → (a : δ) → X a), (∀ (a : δ), Measurable fun c => f c a) → Measurable f- Cited by
- 27 results in Mathlib
- Foundations
- Depth 70 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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_pi_iffproof · cited by 21
Cited by27
Results whose statement or proof uses this declaration.
- Finset.measurable_restrictproof · cited by 17
- Finset.measurable_restrict₂proof · cited by 14
- measurable_IicProdIocproof · cited by 9
- Set.measurable_restrictproof · cited by 5
- MeasurableSet.cylinderproof · cited by 4
- aemeasurable_pi_iffproof · cited by 3
- measurable_IocProdIocproof · cited by 3
- Measure.ext_of_integral_prod_mul_boundedContinuousFunctionproof · cited by 3
- MeasureTheory.inter_mem_measurableCylindersproof · cited by 3
- MeasureTheory.IsProjectiveLimit.measure_cylinderproof · cited by 2
- MeasureTheory.Measure.infinitePi_map_piproof · cited by 2
- ProbabilityTheory.iIndepFun_uncurryproof · cited by 2