# mathlibdocumentation

topology.local_extr

# Local extrema of functions on topological spaces

## 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_*.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.
def is_local_min_on {α : Type u} {β : Type v} [preorder β] :
(α → β)set αα → Prop

is_local_min_on f s a means that f a ≤ f x for all x ∈ s in some neighborhood of a.

Equations
def is_local_max_on {α : Type u} {β : Type v} [preorder β] :
(α → β)set αα → Prop

is_local_max_on f s a means that f x ≤ f a for all x ∈ s in some neighborhood of a.

Equations
def is_local_extr_on {α : Type u} {β : Type v} [preorder β] :
(α → β)set αα → Prop

is_local_extr_on f s a means is_local_min_on f s a ∨ is_local_max_on f s a.

Equations
def is_local_min {α : Type u} {β : Type v} [preorder β] :
(α → β)α → Prop

is_local_min f a means that f a ≤ f x for all x in some neighborhood of a.

Equations
def is_local_max {α : Type u} {β : Type v} [preorder β] :
(α → β)α → Prop

is_local_max f a means that f x ≤ f a for all x ∈ s in some neighborhood of a.

Equations
def is_local_extr {α : Type u} {β : Type v} [preorder β] :
(α → β)α → Prop

is_local_extr_on f s a means is_local_min_on f s a ∨ is_local_max_on f s a.

Equations
theorem is_local_extr_on.elim {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} {p : Prop} :
a s a → p) s a → p) → p

theorem is_local_extr.elim {α : Type u} {β : Type v} [preorder β] {f : α → β} {a : α} {p : Prop} :
a → p) a → p) → p

### Restriction to (sub)sets

theorem is_local_min.on {α : Type u} {β : Type v} [preorder β] {f : α → β} {a : α} (h : a) (s : set α) :
a

theorem is_local_max.on {α : Type u} {β : Type v} [preorder β] {f : α → β} {a : α} (h : a) (s : set α) :
a

theorem is_local_extr.on {α : Type u} {β : Type v} [preorder β] {f : α → β} {a : α} (h : a) (s : set α) :
a

theorem is_local_min_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} {t : set α} :
as t a

theorem is_local_max_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} {t : set α} :
as t a

theorem is_local_extr_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} {t : set α} :
as t a

theorem is_local_min_on.inter {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} (hf : a) (t : set α) :
(s t) a

theorem is_local_max_on.inter {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} (hf : a) (t : set α) :
(s t) a

theorem is_local_extr_on.inter {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} (hf : a) (t : set α) :
(s t) a

theorem is_min_on.localize {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
s a a

theorem is_max_on.localize {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
s a a

theorem is_extr_on.localize {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
s a a

theorem is_local_min_on.is_local_min {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
as 𝓝 a a

theorem is_local_max_on.is_local_max {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
as 𝓝 a a

theorem is_local_extr_on.is_local_extr {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
as 𝓝 a

theorem is_min_on.is_local_min {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
s as 𝓝 a a

theorem is_max_on.is_local_max {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
s as 𝓝 a a

theorem is_extr_on.is_local_extr {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
s as 𝓝 a

### Constant

theorem is_local_min_on_const {α : Type u} {β : Type v} [preorder β] {s : set α} {a : α} {b : β} :
is_local_min_on (λ (_x : α), b) s a

theorem is_local_max_on_const {α : Type u} {β : Type v} [preorder β] {s : set α} {a : α} {b : β} :
is_local_max_on (λ (_x : α), b) s a

theorem is_local_extr_on_const {α : Type u} {β : Type v} [preorder β] {s : set α} {a : α} {b : β} :
is_local_extr_on (λ (_x : α), b) s a

theorem is_local_min_const {α : Type u} {β : Type v} [preorder β] {a : α} {b : β} :
is_local_min (λ (_x : α), b) a

theorem is_local_max_const {α : Type u} {β : Type v} [preorder β] {a : α} {b : β} :
is_local_max (λ (_x : α), b) a

theorem is_local_extr_const {α : Type u} {β : Type v} [preorder β] {a : α} {b : β} :
is_local_extr (λ (_x : α), b) a

### Composition with (anti)monotone functions

theorem is_local_min.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {a : α} (hf : a) {g : β → γ} :
is_local_min (g f) a

theorem is_local_max.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {a : α} (hf : a) {g : β → γ} :
is_local_max (g f) a

theorem is_local_extr.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {a : α} (hf : a) {g : β → γ} :
is_local_extr (g f) a

theorem is_local_min.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {a : α} (hf : a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_local_max (g f) a

theorem is_local_max.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {a : α} (hf : a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_local_min (g f) a

theorem is_local_extr.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {a : α} (hf : a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_local_extr (g f) a

theorem is_local_min_on.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : a) {g : β → γ} :
is_local_min_on (g f) s a

theorem is_local_max_on.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : a) {g : β → γ} :
is_local_max_on (g f) s a

theorem is_local_extr_on.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : a) {g : β → γ} :
is_local_extr_on (g f) s a

theorem is_local_min_on.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_local_max_on (g f) s a

theorem is_local_max_on.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_local_min_on (g f) s a

theorem is_local_extr_on.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_local_extr_on (g f) s a

theorem is_local_min.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [preorder β] [preorder γ] {f : α → β} {a : α} [preorder δ] {op : β → γ → δ} (hop : op op) (hf : a) {g : α → γ} :
ais_local_min (λ (x : α), op (f x) (g x)) a

theorem is_local_max.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [preorder β] [preorder γ] {f : α → β} {a : α} [preorder δ] {op : β → γ → δ} (hop : op op) (hf : a) {g : α → γ} :
ais_local_max (λ (x : α), op (f x) (g x)) a

theorem is_local_min_on.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} [preorder δ] {op : β → γ → δ} (hop : op op) (hf : a) {g : α → γ} :
ais_local_min_on (λ (x : α), op (f x) (g x)) s a

theorem is_local_max_on.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} [preorder δ] {op : β → γ → δ} (hop : op op) (hf : a) {g : α → γ} :
ais_local_max_on (λ (x : α), op (f x) (g x)) s a

### Composition with continuous_at

theorem is_local_min.comp_continuous {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α → β} {g : δ → α} {b : δ} :
(g b)is_local_min (f g) b

theorem is_local_max.comp_continuous {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α → β} {g : δ → α} {b : δ} :
(g b)is_local_max (f g) b

theorem is_local_extr.comp_continuous {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α → β} {g : δ → α} {b : δ} :
(g b)is_local_extr (f g) b

theorem is_local_min.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α → β} {s : set δ} {g : δ → α} {b : δ} :
(g b)b sis_local_min_on (f g) s b

theorem is_local_max.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α → β} {s : set δ} {g : δ → α} {b : δ} :
(g b)b sis_local_max_on (f g) s b

theorem is_local_extr.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α → β} {s : set δ} (g : δ → α) {b : δ} :
(g b)b sis_local_extr_on (f g) s b

theorem is_local_min_on.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α → β} {t : set α} {s : set δ} {g : δ → α} {b : δ} :
(g b)s g ⁻¹' tb sis_local_min_on (f g) s b

theorem is_local_max_on.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α → β} {t : set α} {s : set δ} {g : δ → α} {b : δ} :
(g b)s g ⁻¹' tb sis_local_max_on (f g) s b

theorem is_local_extr_on.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α → β} {t : set α} {s : set δ} (g : δ → α) {b : δ} :
(g b)s g ⁻¹' tb sis_local_extr_on (f g) s b

theorem is_local_min.add {α : Type u} {β : Type v} {f g : α → β} {a : α} :
a ais_local_min (λ (x : α), f x + g x) a

theorem is_local_max.add {α : Type u} {β : Type v} {f g : α → β} {a : α} :
a ais_local_max (λ (x : α), f x + g x) a

theorem is_local_min_on.add {α : Type u} {β : Type v} {f g : α → β} {a : α} {s : set α} :
a ais_local_min_on (λ (x : α), f x + g x) s a

theorem is_local_max_on.add {α : Type u} {β : Type v} {f g : α → β} {a : α} {s : set α} :
a ais_local_max_on (λ (x : α), f x + g x) s a

### Pointwise negation and subtraction

theorem is_local_min.neg {α : Type u} {β : Type v} {f : α → β} {a : α} :
ais_local_max (λ (x : α), -f x) a

theorem is_local_max.neg {α : Type u} {β : Type v} {f : α → β} {a : α} :
ais_local_min (λ (x : α), -f x) a

theorem is_local_extr.neg {α : Type u} {β : Type v} {f : α → β} {a : α} :
is_local_extr (λ (x : α), -f x) a

theorem is_local_min_on.neg {α : Type u} {β : Type v} {f : α → β} {a : α} {s : set α} :
ais_local_max_on (λ (x : α), -f x) s a

theorem is_local_max_on.neg {α : Type u} {β : Type v} {f : α → β} {a : α} {s : set α} :
ais_local_min_on (λ (x : α), -f x) s a

theorem is_local_extr_on.neg {α : Type u} {β : Type v} {f : α → β} {a : α} {s : set α} :
ais_local_extr_on (λ (x : α), -f x) s a

theorem is_local_min.sub {α : Type u} {β : Type v} {f g : α → β} {a : α} :
a ais_local_min (λ (x : α), f x - g x) a

theorem is_local_max.sub {α : Type u} {β : Type v} {f g : α → β} {a : α} :
a ais_local_max (λ (x : α), f x - g x) a

theorem is_local_min_on.sub {α : Type u} {β : Type v} {f g : α → β} {a : α} {s : set α} :
a ais_local_min_on (λ (x : α), f x - g x) s a

theorem is_local_max_on.sub {α : Type u} {β : Type v} {f g : α → β} {a : α} {s : set α} :
a ais_local_max_on (λ (x : α), f x - g x) s a

### Pointwise sup/inf

theorem is_local_min.sup {α : Type u} {β : Type v} {f g : α → β} {a : α} :
a ais_local_min (λ (x : α), f x g x) a

theorem is_local_max.sup {α : Type u} {β : Type v} {f g : α → β} {a : α} :
a ais_local_max (λ (x : α), f x g x) a

theorem is_local_min_on.sup {α : Type u} {β : Type v} {f g : α → β} {a : α} {s : set α} :
a ais_local_min_on (λ (x : α), f x g x) s a

theorem is_local_max_on.sup {α : Type u} {β : Type v} {f g : α → β} {a : α} {s : set α} :
a ais_local_max_on (λ (x : α), f x g x) s a

theorem is_local_min.inf {α : Type u} {β : Type v} {f g : α → β} {a : α} :
a ais_local_min (λ (x : α), f x g x) a

theorem is_local_max.inf {α : Type u} {β : Type v} {f g : α → β} {a : α} :
a ais_local_max (λ (x : α), f x g x) a

theorem is_local_min_on.inf {α : Type u} {β : Type v} {f g : α → β} {a : α} {s : set α} :
a ais_local_min_on (λ (x : α), f x g x) s a

theorem is_local_max_on.inf {α : Type u} {β : Type v} {f g : α → β} {a : α} {s : set α} :
a ais_local_max_on (λ (x : α), f x g x) s a

### Pointwise min/max

theorem is_local_min.min {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} :
a ais_local_min (λ (x : α), min (f x) (g x)) a

theorem is_local_max.min {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} :
a ais_local_max (λ (x : α), min (f x) (g x)) a

theorem is_local_min_on.min {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {s : set α} :
a ais_local_min_on (λ (x : α), min (f x) (g x)) s a

theorem is_local_max_on.min {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {s : set α} :
a ais_local_max_on (λ (x : α), min (f x) (g x)) s a

theorem is_local_min.max {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} :
a ais_local_min (λ (x : α), max (f x) (g x)) a

theorem is_local_max.max {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} :
a ais_local_max (λ (x : α), max (f x) (g x)) a

theorem is_local_min_on.max {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {s : set α} :
a ais_local_min_on (λ (x : α), max (f x) (g x)) s a

theorem is_local_max_on.max {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {s : set α} :
a ais_local_max_on (λ (x : α), max (f x) (g x)) s a

### Relation with eventually comparisons of two functions

theorem filter.eventually_le.is_local_max_on {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α → β} {a : α} :
g ≤ᶠ[𝓝[s] a] ff a = g a a a

theorem is_local_max_on.congr {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α → β} {a : α} :
af =ᶠ[𝓝[s] a] ga s a

theorem filter.eventually_eq.is_local_max_on_iff {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α → β} {a : α} :
f =ᶠ[𝓝[s] a] ga s s a a)

theorem filter.eventually_le.is_local_min_on {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α → β} {a : α} :
f ≤ᶠ[𝓝[s] a] gf a = g a a a

theorem is_local_min_on.congr {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α → β} {a : α} :
af =ᶠ[𝓝[s] a] ga s a

theorem filter.eventually_eq.is_local_min_on_iff {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α → β} {a : α} :
f =ᶠ[𝓝[s] a] ga s s a a)

theorem is_local_extr_on.congr {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α → β} {a : α} :
af =ᶠ[𝓝[s] a] ga s a

theorem filter.eventually_eq.is_local_extr_on_iff {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α → β} {a : α} :
f =ᶠ[𝓝[s] a] ga s s a a)

theorem filter.eventually_le.is_local_max {α : Type u} {β : Type v} [preorder β] {f g : α → β} {a : α} :
g ≤ᶠ[𝓝 a] ff a = g a a a

theorem is_local_max.congr {α : Type u} {β : Type v} [preorder β] {f g : α → β} {a : α} :
af =ᶠ[𝓝 a] g a

theorem filter.eventually_eq.is_local_max_iff {α : Type u} {β : Type v} [preorder β] {f g : α → β} {a : α} :
f =ᶠ[𝓝 a] g a a)

theorem filter.eventually_le.is_local_min {α : Type u} {β : Type v} [preorder β] {f g : α → β} {a : α} :
f ≤ᶠ[𝓝 a] gf a = g a a a

theorem is_local_min.congr {α : Type u} {β : Type v} [preorder β] {f g : α → β} {a : α} :
af =ᶠ[𝓝 a] g a

theorem filter.eventually_eq.is_local_min_iff {α : Type u} {β : Type v} [preorder β] {f g : α → β} {a : α} :
f =ᶠ[𝓝 a] g a a)

theorem is_local_extr.congr {α : Type u} {β : Type v} [preorder β] {f g : α → β} {a : α} :
f =ᶠ[𝓝 a] g

theorem filter.eventually_eq.is_local_extr_iff {α : Type u} {β : Type v} [preorder β] {f g : α → β} {a : α} :
f =ᶠ[𝓝 a] g a a)