Theorem MeasurableEmbedding.prod_mk_right

Modification history

2024-10-27 19:30
Mathlib/MeasureTheory/MeasurableSpace/Prod.lean
chore(MeasureTheory/Constructions/Prod/Basic: split (#18286) …
Modified MeasurableEmbedding.prod_mk_rightView on Github →
2024-01-18 15:15
Mathlib/MeasureTheory/Constructions/Prod/Basic.lean
feat(Probability): condKernel and condDistrib applied to singletons of non-zero measure (#9351) …
Added MeasurableEmbedding.prod_mk_rightView on Github →