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 →