# mathlib3documentation

topology.local_extr

# 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_*.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 β] (f : α β) (s : set α) (a : α) :
Prop

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

Equations
• a = s) a
def is_local_max_on {α : Type u} {β : Type v} [preorder β] (f : α β) (s : set α) (a : α) :
Prop

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

Equations
• a = s) a
def is_local_extr_on {α : Type u} {β : Type v} [preorder β] (f : α β) (s : set α) (a : α) :
Prop

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

Equations
• a = s) a
def is_local_min {α : Type u} {β : Type v} [preorder β] (f : α β) (a : α) :
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 β] (f : α β) (a : α) :
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 β] (f : α β) (a : α) :
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 α} (hf : a) (h : s t) :
a
theorem is_local_max_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} {t : set α} (hf : a) (h : s t) :
a
theorem is_local_extr_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} {t : set α} (hf : a) (h : s 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 : α} (hf : s a) :
a
theorem is_max_on.localize {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : s a) :
a
theorem is_extr_on.localize {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : s a) :
a
theorem is_local_min_on.is_local_min {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : a) (hs : s nhds a) :
a
theorem is_local_max_on.is_local_max {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : a) (hs : s nhds a) :
a
theorem is_local_extr_on.is_local_extr {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : a) (hs : s nhds a) :
theorem is_min_on.is_local_min {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : s a) (hs : s nhds a) :
a
theorem is_max_on.is_local_max {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : s a) (hs : s nhds a) :
a
theorem is_extr_on.is_local_extr {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : s a) (hs : s nhds a) :
theorem is_local_min_on.not_nhds_le_map {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : a) [(nhds_within (f a) (set.Iio (f a))).ne_bot] :
¬nhds (f a) s)
theorem is_local_max_on.not_nhds_le_map {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : a) [(nhds_within (f a) (set.Ioi (f a))).ne_bot] :
¬nhds (f a) s)
theorem is_local_extr_on.not_nhds_le_map {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : a) [(nhds_within (f a) (set.Iio (f a))).ne_bot] [(nhds_within (f a) (set.Ioi (f a))).ne_bot] :
¬nhds (f a) s)

### 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 : β γ} (hg : monotone g) :
theorem is_local_max.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {a : α} (hf : a) {g : β γ} (hg : monotone g) :
theorem is_local_extr.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {a : α} (hf : a) {g : β γ} (hg : monotone g) :
theorem is_local_min.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {a : α} (hf : a) {g : β γ} (hg : antitone g) :
theorem is_local_max.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {a : α} (hf : a) {g : β γ} (hg : antitone g) :
theorem is_local_extr.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {a : α} (hf : a) {g : β γ} (hg : antitone g) :
theorem is_local_min_on.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : a) {g : β γ} (hg : monotone g) :
theorem is_local_max_on.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : a) {g : β γ} (hg : monotone g) :
theorem is_local_extr_on.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : a) {g : β γ} (hg : monotone g) :
theorem is_local_min_on.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : a) {g : β γ} (hg : antitone g) :
theorem is_local_max_on.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : a) {g : β γ} (hg : antitone g) :
theorem is_local_extr_on.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : a) {g : β γ} (hg : antitone g) :
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 : α γ} (hg : a) :
is_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 : α γ} (hg : a) :
is_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 : α γ} (hg : a) :
is_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 : α γ} (hg : a) :
is_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 : δ} (hf : (g b)) (hg : b) :
theorem is_local_max.comp_continuous {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {g : δ α} {b : δ} (hf : (g b)) (hg : b) :
theorem is_local_extr.comp_continuous {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {g : δ α} {b : δ} (hf : (g b)) (hg : b) :
theorem is_local_min.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {s : set δ} {g : δ α} {b : δ} (hf : (g b)) (hg : s) (hb : b s) :
theorem is_local_max.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {s : set δ} {g : δ α} {b : δ} (hf : (g b)) (hg : s) (hb : b s) :
theorem is_local_extr.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {s : set δ} (g : δ α) {b : δ} (hf : (g b)) (hg : s) (hb : b s) :
theorem is_local_min_on.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {t : set α} {s : set δ} {g : δ α} {b : δ} (hf : (g b)) (hst : s g ⁻¹' t) (hg : s) (hb : b s) :
theorem is_local_max_on.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {t : set α} {s : set δ} {g : δ α} {b : δ} (hf : (g b)) (hst : s g ⁻¹' t) (hg : s) (hb : b s) :
theorem is_local_extr_on.comp_continuous_on {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {t : set α} {s : set δ} (g : δ α) {b : δ} (hf : (g b)) (hst : s g ⁻¹' t) (hg : s) (hb : b s) :

### Pointwise addition #

theorem is_local_min.add {α : Type u} {β : Type v} {f g : α β} {a : α} (hf : a) (hg : a) :
is_local_min (λ (x : α), f x + g x) a
theorem is_local_max.add {α : Type u} {β : Type v} {f g : α β} {a : α} (hf : a) (hg : a) :
is_local_max (λ (x : α), f x + g x) a
theorem is_local_min_on.add {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : a) (hg : a) :
is_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 α} (hf : a) (hg : a) :
is_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 : α} (hf : a) :
is_local_max (λ (x : α), -f x) a
theorem is_local_max.neg {α : Type u} {β : Type v} {f : α β} {a : α} (hf : a) :
is_local_min (λ (x : α), -f x) a
theorem is_local_extr.neg {α : Type u} {β : Type v} {f : α β} {a : α} (hf : a) :
is_local_extr (λ (x : α), -f x) a
theorem is_local_min_on.neg {α : Type u} {β : Type v} {f : α β} {a : α} {s : set α} (hf : a) :
is_local_max_on (λ (x : α), -f x) s a
theorem is_local_max_on.neg {α : Type u} {β : Type v} {f : α β} {a : α} {s : set α} (hf : a) :
is_local_min_on (λ (x : α), -f x) s a
theorem is_local_extr_on.neg {α : Type u} {β : Type v} {f : α β} {a : α} {s : set α} (hf : a) :
is_local_extr_on (λ (x : α), -f x) s a
theorem is_local_min.sub {α : Type u} {β : Type v} {f g : α β} {a : α} (hf : a) (hg : a) :
is_local_min (λ (x : α), f x - g x) a
theorem is_local_max.sub {α : Type u} {β : Type v} {f g : α β} {a : α} (hf : a) (hg : a) :
is_local_max (λ (x : α), f x - g x) a
theorem is_local_min_on.sub {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : a) (hg : a) :
is_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 α} (hf : a) (hg : a) :
is_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 : α} (hf : a) (hg : a) :
is_local_min (λ (x : α), f x g x) a
theorem is_local_max.sup {α : Type u} {β : Type v} {f g : α β} {a : α} (hf : a) (hg : a) :
is_local_max (λ (x : α), f x g x) a
theorem is_local_min_on.sup {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : a) (hg : a) :
is_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 α} (hf : a) (hg : a) :
is_local_max_on (λ (x : α), f x g x) s a
theorem is_local_min.inf {α : Type u} {β : Type v} {f g : α β} {a : α} (hf : a) (hg : a) :
is_local_min (λ (x : α), f x g x) a
theorem is_local_max.inf {α : Type u} {β : Type v} {f g : α β} {a : α} (hf : a) (hg : a) :
is_local_max (λ (x : α), f x g x) a
theorem is_local_min_on.inf {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : a) (hg : a) :
is_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 α} (hf : a) (hg : a) :
is_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 : α} (hf : a) (hg : a) :
is_local_min (λ (x : α), linear_order.min (f x) (g x)) a
theorem is_local_max.min {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} (hf : a) (hg : a) :
is_local_max (λ (x : α), linear_order.min (f x) (g x)) a
theorem is_local_min_on.min {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {s : set α} (hf : a) (hg : a) :
is_local_min_on (λ (x : α), linear_order.min (f x) (g x)) s a
theorem is_local_max_on.min {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {s : set α} (hf : a) (hg : a) :
is_local_max_on (λ (x : α), linear_order.min (f x) (g x)) s a
theorem is_local_min.max {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} (hf : a) (hg : a) :
is_local_min (λ (x : α), linear_order.max (f x) (g x)) a
theorem is_local_max.max {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} (hf : a) (hg : a) :
is_local_max (λ (x : α), linear_order.max (f x) (g x)) a
theorem is_local_min_on.max {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {s : set α} (hf : a) (hg : a) :
is_local_min_on (λ (x : α), linear_order.max (f x) (g x)) s a
theorem is_local_max_on.max {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {s : set α} (hf : a) (hg : a) :
is_local_max_on (λ (x : α), linear_order.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 : α} (hle : g ≤ᶠ[ s] f) (hfga : f a = g a) (h : a) :
a
theorem is_local_max_on.congr {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α β} {a : α} (h : a) (heq : f =ᶠ[ s] g) (hmem : a s) :
a
theorem filter.eventually_eq.is_local_max_on_iff {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α β} {a : α} (heq : f =ᶠ[ s] g) (hmem : a s) :
a a
theorem filter.eventually_le.is_local_min_on {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α β} {a : α} (hle : f ≤ᶠ[ s] g) (hfga : f a = g a) (h : a) :
a
theorem is_local_min_on.congr {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α β} {a : α} (h : a) (heq : f =ᶠ[ s] g) (hmem : a s) :
a
theorem filter.eventually_eq.is_local_min_on_iff {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α β} {a : α} (heq : f =ᶠ[ s] g) (hmem : a s) :
a a
theorem is_local_extr_on.congr {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α β} {a : α} (h : a) (heq : f =ᶠ[ s] g) (hmem : a s) :
a
theorem filter.eventually_eq.is_local_extr_on_iff {α : Type u} {β : Type v} [preorder β] {s : set α} {f g : α β} {a : α} (heq : f =ᶠ[ s] g) (hmem : a s) :
a a
theorem filter.eventually_le.is_local_max {α : Type u} {β : Type v} [preorder β] {f g : α β} {a : α} (hle : g ≤ᶠ[nhds a] f) (hfga : f a = g a) (h : a) :
a
theorem is_local_max.congr {α : Type u} {β : Type v} [preorder β] {f g : α β} {a : α} (h : a) (heq : f =ᶠ[nhds a] g) :
a
theorem filter.eventually_eq.is_local_max_iff {α : Type u} {β : Type v} [preorder β] {f g : α β} {a : α} (heq : f =ᶠ[nhds a] g) :
a a
theorem filter.eventually_le.is_local_min {α : Type u} {β : Type v} [preorder β] {f g : α β} {a : α} (hle : f ≤ᶠ[nhds a] g) (hfga : f a = g a) (h : a) :
a
theorem is_local_min.congr {α : Type u} {β : Type v} [preorder β] {f g : α β} {a : α} (h : a) (heq : f =ᶠ[nhds a] g) :
a
theorem filter.eventually_eq.is_local_min_iff {α : Type u} {β : Type v} [preorder β] {f g : α β} {a : α} (heq : f =ᶠ[nhds a] g) :
a a
theorem is_local_extr.congr {α : Type u} {β : Type v} [preorder β] {f g : α β} {a : α} (h : a) (heq : f =ᶠ[nhds a] g) :
theorem filter.eventually_eq.is_local_extr_iff {α : Type u} {β : Type v} [preorder β] {f g : α β} {a : α} (heq : f =ᶠ[nhds a] g) :