Commit 2026-09-15 09:35 1e043bcd

View on Github →

chore(Order/Filter/Extr): rename various lemmas (#41863) Per the mathlib naming conventions

Estimated changes

Modified Mathlib/Analysis/Calculus/LocalExtr/LineDeriv.lean

Modified Mathlib/Analysis/Complex/AbsMax.lean

Modified Mathlib/Order/Filter/Extr.lean

added theorem IsExtrFilter.comp_of_tendsto

deleted theorem IsExtrFilter.comp_tendsto

deleted theorem IsExtrOn.comp_mapsTo

added theorem IsExtrOn.comp_of_mapsTo

added theorem IsExtrOn.of_subset

deleted theorem IsExtrOn.on_preimage

deleted theorem IsExtrOn.on_subset

added theorem IsExtrOn.preimage

added theorem IsMaxFilter.comp_of_tendsto

deleted theorem IsMaxFilter.comp_tendsto

deleted theorem IsMaxFilter.isExtr

added theorem IsMaxFilter.isExtrFilter

deleted theorem IsMaxOn.comp_mapsTo

added theorem IsMaxOn.comp_of_mapsTo

deleted theorem IsMaxOn.isExtr

added theorem IsMaxOn.isExtrOn

added theorem IsMaxOn.of_subset

deleted theorem IsMaxOn.on_preimage

deleted theorem IsMaxOn.on_subset

added theorem IsMaxOn.preimage

added theorem IsMinFilter.comp_of_tendsto

deleted theorem IsMinFilter.comp_tendsto

deleted theorem IsMinFilter.isExtr

added theorem IsMinFilter.isExtrFilter

deleted theorem IsMinOn.comp_mapsTo

added theorem IsMinOn.comp_of_mapsTo

deleted theorem IsMinOn.isExtr

added theorem IsMinOn.isExtrOn

added theorem IsMinOn.of_subset

deleted theorem IsMinOn.on_preimage

deleted theorem IsMinOn.on_subset

added theorem IsMinOn.preimage

Modified Mathlib/Topology/Order/LocalExtr.lean

Modified Mathlib/Topology/Order/Rolle.lean