Commit 2023-01-31 21:53 1c27d1e2

View on Github →

feat: port Topology.LocalExtr (#1909)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/LocalExtr.lean

added theorem Filter.EventuallyEq.isLocalExtrOn_iff

added theorem Filter.EventuallyEq.isLocalExtr_iff

added theorem Filter.EventuallyEq.isLocalMaxOn_iff

added theorem Filter.EventuallyEq.isLocalMax_iff

added theorem Filter.EventuallyEq.isLocalMin_iff

added theorem Filter.EventuallyLe.isLocalMax

added theorem Filter.EventuallyLe.isLocalMaxOn

added theorem Filter.EventuallyLe.isLocalMin

added theorem Filter.EventuallyLe.isLocalMinOn

added theorem IsExtrOn.isLocalExtr

added theorem IsExtrOn.localize

added theorem IsLocalExtr.comp_continuous

added theorem IsLocalExtr.comp_continuousOn

added theorem IsLocalExtr.elim

added theorem IsLocalExtr.on

added def IsLocalExtr

added theorem IsLocalExtrOn.comp_continuousOn

added theorem IsLocalExtrOn.elim

added theorem IsLocalExtrOn.inter

added theorem IsLocalExtrOn.isLocalExtr

added theorem IsLocalExtrOn.not_nhds_le_map

added theorem IsLocalExtrOn.on_subset

added def IsLocalExtrOn

added theorem IsLocalMax.comp_continuous

added theorem IsLocalMax.comp_continuousOn

added theorem IsLocalMax.on

added def IsLocalMax

added theorem IsLocalMaxOn.comp_continuousOn

added theorem IsLocalMaxOn.inter

added theorem IsLocalMaxOn.isLocalMax

added theorem IsLocalMaxOn.not_nhds_le_map

added theorem IsLocalMaxOn.on_subset

added def IsLocalMaxOn

added theorem IsLocalMin.comp_continuous

added theorem IsLocalMin.comp_continuousOn

added theorem IsLocalMin.on

added def IsLocalMin

added theorem IsLocalMinOn.comp_continuousOn

added theorem IsLocalMinOn.inter

added theorem IsLocalMinOn.isLocalMin

added theorem IsLocalMinOn.not_nhds_le_map

added theorem IsLocalMinOn.on_subset

added def IsLocalMinOn

added theorem IsMaxOn.isLocalMax

added theorem IsMaxOn.localize

added theorem IsMinOn.isLocalMin

added theorem IsMinOn.localize

added theorem isLocalExtrOn_const

added theorem isLocalExtr_const

added theorem isLocalMaxOn_const

added theorem isLocalMax_const

added theorem isLocalMinOn_const

added theorem isLocalMin_const