Commit 2026-08-28 10:00 4b4d0e84

View on Github →

chore(Topology/Order/LocalExtr): rename several theorems (#41865) Per the mathlib naming conventions. Also discussed on Zulip [#mathlib4 > Renaming `IsLocalMin.on` and `IsMinOn.localize`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Renaming.20.60IsLocalMin.2Eon.60.20and.20.60IsMinOn.2Elocalize.60/with/611258354).

Estimated changes

added theorem IsExtrOn.isLocalExtrOn
deleted theorem IsExtrOn.localize
deleted theorem IsLocalExtr.on
added theorem IsLocalExtrOn.mono
deleted theorem IsLocalExtrOn.on_subset
deleted theorem IsLocalMax.on
added theorem IsLocalMaxOn.mono
deleted theorem IsLocalMaxOn.on_subset
deleted theorem IsLocalMin.on
added theorem IsLocalMinOn.mono
deleted theorem IsLocalMinOn.on_subset
added theorem IsMaxOn.isLocalMaxOn
deleted theorem IsMaxOn.localize
added theorem IsMinOn.isLocalMinOn
deleted theorem IsMinOn.localize