Commit 2024-09-01 12:32 fc860709

View on Github →

chore(Measure): add gcongr lemmas (#16379)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Prod/Basic.lean

added theorem MeasureTheory.Measure.fst_mono

added theorem MeasureTheory.Measure.snd_mono

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

added theorem MeasureTheory.Measure.restrict_mono_measure

added theorem MeasureTheory.Measure.restrict_mono_set

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

modified theorem MeasureTheory.Measure.IicSnd_le_fst