mathlib documentation

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:

def is_local_min_on {α : Type u} {β : Type v} [topological_space α] [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} [topological_space α] [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} [topological_space α] [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} [topological_space α] [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} [topological_space α] [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} [topological_space α] [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} [topological_space α] [preorder β] {f : α → β} {s : set α} {a : α} {p : Prop} :
is_local_extr_on f s a(is_local_min_on f s a → p)(is_local_max_on f s a → p) → p

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

Restriction to (sub)sets

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Constant

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

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

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

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

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

theorem is_local_extr_const {α : Type u} {β : Type v} [topological_space α] [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} [topological_space α] [preorder β] [preorder γ] {f : α → β} {a : α} (hf : is_local_min f a) {g : β → γ} :
monotone gis_local_min (g f) a

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

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

theorem is_local_min.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [preorder β] [preorder γ] {f : α → β} {a : α} (hf : is_local_min f 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} [topological_space α] [preorder β] [preorder γ] {f : α → β} {a : α} (hf : is_local_max f 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} [topological_space α] [preorder β] [preorder γ] {f : α → β} {a : α} (hf : is_local_extr f 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} [topological_space α] [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : is_local_min_on f s a) {g : β → γ} :
monotone gis_local_min_on (g f) s a

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

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

theorem is_local_min_on.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : is_local_min_on f s 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} [topological_space α] [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : is_local_max_on f s 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} [topological_space α] [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : is_local_extr_on f s 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} [topological_space α] [preorder β] [preorder γ] {f : α → β} {a : α} [preorder δ] {op : β → γ → δ} (hop : (has_le.le has_le.le has_le.le) op op) (hf : is_local_min f a) {g : α → γ} :
is_local_min 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} [topological_space α] [preorder β] [preorder γ] {f : α → β} {a : α} [preorder δ] {op : β → γ → δ} (hop : (has_le.le has_le.le has_le.le) op op) (hf : is_local_max f a) {g : α → γ} :
is_local_max 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} [topological_space α] [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} [preorder δ] {op : β → γ → δ} (hop : (has_le.le has_le.le has_le.le) op op) (hf : is_local_min_on f s a) {g : α → γ} :
is_local_min_on g s 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} [topological_space α] [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} [preorder δ] {op : β → γ → δ} (hop : (has_le.le has_le.le has_le.le) op op) (hf : is_local_max_on f s a) {g : α → γ} :
is_local_max_on g s 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} [topological_space α] [preorder β] {f : α → β} [topological_space δ] {g : δ → α} {b : δ} :
is_local_min f (g b)continuous_at g bis_local_min (f g) b

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

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

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

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

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

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

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

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

Pointwise addition

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

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

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

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

Pointwise negation and subtraction

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

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

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

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

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

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

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

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

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

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

Pointwise sup/inf

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

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

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

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

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

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

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

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

Pointwise min/max

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

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

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

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

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

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

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

theorem is_local_max_on.max {α : Type u} {β : Type v} [topological_space α] [linear_order β] {f g : α → β} {a : α} {s : set α} :
is_local_max_on f s ais_local_max_on g s 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} [topological_space α] [preorder β] {s : set α} {f g : α → β} {a : α} :
g ≤ᶠ[𝓝[s] a] ff a = g ais_local_max_on f s ais_local_max_on g s a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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