Theorem MeasurableEmbedding.prod_mk_left

Modification history

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_leftView on Github →