Theorems · Definition · measure theory
MeasurableSpace.prod
{α : Type u_6} → {β : Type u_7} → MeasurableSpace α → MeasurableSpace β → MeasurableSpace (α × β)A MeasurableSpace structure on the product of two measurable spaces.
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- MeasurableSpace.comapproof · cited by 124
Cited by15
Results whose statement or proof uses this declaration.
- MeasureTheory.Integrable.comp_snd_map_prod_idstatement · cited by 4
- MeasurableEmbedding.prodMapproof · cited by 4
- ProbabilityTheory.compProd_trim_condExpKernelstatement · cited by 3
- MeasureTheory.IsStronglyPredictable.isStronglyProgressiveproof · cited by 3
- MeasureTheory.isStronglyProgressive_min_stopping_timeproof · cited by 2
- MeasureTheory.measurable_update_cylinderEvents'statement · cited by 2
- MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_idstatement · cited by 2
- ProbabilityTheory.Kernel.measurable_densityProcess_countableFiltration_auxstatement · cited by 2
- ProbabilityTheory.HasSubgaussianMGF.add_of_hasCondSubgaussianMGFproof · cited by 2
- MeasureTheory.measurable_inclusion_predictablestatement · cited by 1
- MeasurableSpace.comap_prodMapstatement · cited by 1
- ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trimstatement · cited by 1