Commit 2026-10-28 12:53 572247c4

View on Github →

chore: rename ENNReal.toReal_mono' (#43856) This PR addresses tech debt by renaming ENNReal.toReal_mono' to ENNReal.toReal_mono_of_top_imp_top (and similarly renaming the related ENNReal.toReal_le_add'). This change makes the naming scheme more similar to ENNReal.le_of_top_imp_top_of_toNNReal_le I chose these names myself, but used LLM assistance to scan the library for instances of the lemmas.

Estimated changes

Modified Mathlib/Basic/ENNReal/Operations.lean

deleted theorem ENNReal.toReal_le_add'

added theorem ENNReal.toReal_le_add_of_top_imp_top

Modified Mathlib/Basic/ENNReal/Real.lean

deleted theorem ENNReal.toReal_mono'

added theorem ENNReal.toReal_mono_of_top_imp_top

Modified Mathlib/Topology/MetricSpace/Bounded.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

Modified Mathlib/Topology/MetricSpace/Thickening.lean

Modified scripts/nolints_prime_decls.txt