Local extrema of functions on topological spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
This file defines special versions of is_*_filter f a l
, *=min/max/extr
,
from order/filter/extr
for two kinds of filters: nhds_within
and nhds
.
These versions are called is_local_*_on
and is_local_*
, respectively.
Main statements #
Many lemmas in this file restate those from order/filter/extr
, and you can find
a detailed documentation there. These convenience lemmas are provided only to make the dot notation
return propositions of expected types, not just is_*_filter
.
Here is the list of statements specific to these two types of filters:
is_local_min_on f s a
means that f a ≤ f x
for all x ∈ s
in some neighborhood of a
.
Equations
- is_local_min_on f s a = is_min_filter f (nhds_within a s) a
is_local_max_on f s a
means that f x ≤ f a
for all x ∈ s
in some neighborhood of a
.
Equations
- is_local_max_on f s a = is_max_filter f (nhds_within a s) a
is_local_extr_on f s a
means is_local_min_on f s a ∨ is_local_max_on f s a
.
Equations
- is_local_extr_on f s a = is_extr_filter f (nhds_within a s) a
is_local_min f a
means that f a ≤ f x
for all x
in some neighborhood of a
.
Equations
- is_local_min f a = is_min_filter f (nhds a) a
is_local_max f a
means that f x ≤ f a
for all x ∈ s
in some neighborhood of a
.
Equations
- is_local_max f a = is_max_filter f (nhds a) a
is_local_extr_on f s a
means is_local_min_on f s a ∨ is_local_max_on f s a
.
Equations
- is_local_extr f a = is_extr_filter f (nhds a) a