Commit 2025-05-27 14:09 44140d72

View on Github →

feat(Tactic/Finiteness): tag more lemmas (#25086) Tag a few more lemmas with finiteness, and add a few more lemmas for it. Now, finiteness should handle (basic cases of) ENNReal division, powers and maximum. From the Carleson project.

Estimated changes

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

added theorem ENNReal.rpow_ne_top_of_ne_zero

Modified Mathlib/Data/ENNReal/Inv.lean

added theorem ENNReal.div_ne_top

modified theorem ENNReal.inv_mul_ne_top

modified theorem ENNReal.mul_inv_ne_top

added theorem ENNReal.zpow_ne_top

Modified Mathlib/Data/ENNReal/Operations.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses/Finite.lean

added theorem MeasureTheory.measure_ball_ne_top

Modified Mathlib/Order/BoundedOrder/Lattice.lean

added theorem max_ne_top

Modified Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

Modified MathlibTest/finiteness.lean