Commit 2024-10-16 14:29 617ce534

View on Github →

chore(MeasureTheory): let gcongr know about spanningSets (#17824) From GibbsMeasure

Estimated changes

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

added theorem MeasureTheory.spanningSets_mono