Commit 2024-12-12 03:19 2ec7e0af

View on Github →

chore(MeasurableSpace/Prod): rename a lemma (#19901) Also use Prod.map in the statement and golf a proof using aesop.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Prod.lean

added theorem MeasurableEmbedding.prodMap

deleted theorem MeasurableEmbedding.prod_mk

Modified Mathlib/Probability/Kernel/Composition/Basic.lean

Modified Mathlib/Probability/Kernel/Disintegration/StandardBorel.lean