Commit 2026-08-12 18:02 a13cd555

chore(MeasureTheory): Move lemmas and deprecate duplicates (#42338) This PR moves a few lemmas around in MeasureTheory.Measure; basically, if a lemma can be expressed and proved elementarily, it is moved upstream. For instance, if a lemma has μ ≤ ν has an hypothesis, it may be proved as a special case of a lemma about absolutely continuous measures, but may also be proved as easily by more elementary considerations, which means it can be moved to more suitable files upstream (e.g. to MeasureTheory.Measure.MeasureSpace instead of MeasureTheory.Measure.AbsolutelyContinuous). This also slightly simplifies imports and allowed me to detect two exact duplicates.