Commit 2024-05-17 06:05 ebfda4da

View on Github →

chore(*): golf, mostly using gcongr (#12944) Golf, mostly in MeasureTheory using gcongr. Also add some missing gcongr lemmas.

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

Modified Mathlib/Data/Set/Accumulate.lean

added theorem Set.accumulate_subset_accumulate

Modified Mathlib/Data/Set/Prod.lean

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

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

Modified Mathlib/MeasureTheory/Covering/Besicovitch.lean

added def Mathlib.Meta.Positivity.evalBesicovitchSatelliteConfigR

Modified Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

Modified Mathlib/MeasureTheory/Decomposition/UnsignedHahn.lean

Modified Mathlib/MeasureTheory/Function/AEMeasurableOrder.lean

Modified Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean

Modified Mathlib/MeasureTheory/Function/Egorov.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/Integral/Average.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/MeasureTheory/Integral/PeakFunction.lean

Modified Mathlib/MeasureTheory/Measure/Doubling.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/ModelTheory/Syntax.lean

added theorem FirstOrder.Language.distinctConstantsTheory_mono

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Filter/Prod.lean

Modified Mathlib/Order/Interval/Set/Basic.lean

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

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/EMetricSpace/Basic.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

Modified Mathlib/Topology/MetricSpace/PseudoMetric.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

Modified Mathlib/Topology/UniformSpace/Equicontinuity.lean