Commit 2023-10-24 16:07 5fcd5523

View on Github →

chore: gcongr tagging (#7889) Tag lemmas about tsub (truncated subtraction), nnreal and ennreal powers, and measures for gcongr.

Estimated changes

Modified Mathlib/Algebra/Order/Sub/Defs.lean

modified theorem tsub_le_tsub

modified theorem tsub_le_tsub_left

modified theorem tsub_le_tsub_right

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

modified theorem ENNReal.rpow_le_rpow

modified theorem ENNReal.rpow_le_rpow_of_exponent_le

modified theorem ENNReal.rpow_lt_rpow

modified theorem NNReal.rpow_le_rpow

modified theorem NNReal.rpow_le_rpow_of_exponent_le

modified theorem NNReal.rpow_lt_rpow

modified theorem NNReal.rpow_lt_rpow_of_exponent_lt

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

modified theorem MeasureTheory.measure_mono