Commit 2024-09-01 12:18 28e7b452

chore(Probability/Kernel): golf measurable_compProdFun (#16302) measurable_compProdFun is a statement about s-finite kernels, and used an auxiliary lemma measurable_compProdFun_of_finite for finite kernels. However, due to changes elsewhere, the proof of measurable_compProdFun_of_finite now works for s-finite kernels directly. measurable_compProdFun_of_finite is renamed to measurable_compProdFun and the old measurable_compProdFun is removed. This PR also contains a few cosmetic changes in the lemmas about compProdFun (fix a few linebreaks from mathport, replace => by ↦, etc.)