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.
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_*.on, is_local_*_on.on_subset: restrict to a subset;
is_local_*_on.inter : intersect the set with another one;
is_*_on.localize : a global extremum is a local extremum too.
is_[local_]*_on.is_local_* : if we have is_local_*_on f s a and s ∈ 𝓝 a,
then we have is_local_* f a.