# Local extrema of functions on topological spaces #

## Main definitions #

This file defines special versions of Is*Filter f a l, *=Min/Max/Extr, from Mathlib.Order.Filter.Extr for two kinds of filters: nhdsWithin and nhds. These versions are called IsLocal*On and IsLocal*, respectively.

## Main statements #

Many lemmas in this file restate those from Mathlib.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:

• IsLocal*.on, IsLocal*On.on_subset: restrict to a subset;
• IsLocal*On.inter : intersect the set with another one;
• Is*On.localize : a global extremum is a local extremum too.
• Is[Local]*On.isLocal* : if we have IsLocal*On f s a and s ∈ 𝓝 a, then we have IsLocal* f a.
def IsLocalMinOn {α : Type u} {β : Type v} [] [] (f : αβ) (s : Set α) (a : α) :

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

Equations
Instances For
def IsLocalMaxOn {α : Type u} {β : Type v} [] [] (f : αβ) (s : Set α) (a : α) :

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

Equations
Instances For
def IsLocalExtrOn {α : Type u} {β : Type v} [] [] (f : αβ) (s : Set α) (a : α) :

IsLocalExtrOn f s a means IsLocalMinOn f s a ∨ IsLocalMaxOn f s a.

Equations
Instances For
def IsLocalMin {α : Type u} {β : Type v} [] [] (f : αβ) (a : α) :

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

Equations
Instances For
def IsLocalMax {α : Type u} {β : Type v} [] [] (f : αβ) (a : α) :

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

Equations
Instances For
def IsLocalExtr {α : Type u} {β : Type v} [] [] (f : αβ) (a : α) :

IsLocalExtrOn f s a means IsLocalMinOn f s a ∨ IsLocalMaxOn f s a.

Equations
Instances For
theorem IsLocalExtrOn.elim {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} {p : Prop} :
(IsLocalMinOn f s ap)(IsLocalMaxOn f s ap)p
theorem IsLocalExtr.elim {α : Type u} {β : Type v} [] [] {f : αβ} {a : α} {p : Prop} :
(p)(p)p

### Restriction to (sub)sets #

theorem IsLocalMin.on {α : Type u} {β : Type v} [] [] {f : αβ} {a : α} (h : ) (s : Set α) :
theorem IsLocalMax.on {α : Type u} {β : Type v} [] [] {f : αβ} {a : α} (h : ) (s : Set α) :
theorem IsLocalExtr.on {α : Type u} {β : Type v} [] [] {f : αβ} {a : α} (h : ) (s : Set α) :
theorem IsLocalMinOn.on_subset {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} {t : Set α} (hf : IsLocalMinOn f t a) (h : s t) :
theorem IsLocalMaxOn.on_subset {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} {t : Set α} (hf : IsLocalMaxOn f t a) (h : s t) :
theorem IsLocalExtrOn.on_subset {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} {t : Set α} (hf : ) (h : s t) :
theorem IsLocalMinOn.inter {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsLocalMinOn f s a) (t : Set α) :
IsLocalMinOn f (s t) a
theorem IsLocalMaxOn.inter {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsLocalMaxOn f s a) (t : Set α) :
IsLocalMaxOn f (s t) a
theorem IsLocalExtrOn.inter {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : ) (t : Set α) :
IsLocalExtrOn f (s t) a
theorem IsMinOn.localize {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsMinOn f s a) :
theorem IsMaxOn.localize {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) :
theorem IsExtrOn.localize {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsExtrOn f s a) :
theorem IsLocalMinOn.isLocalMin {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsLocalMinOn f s a) (hs : s nhds a) :
theorem IsLocalMaxOn.isLocalMax {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsLocalMaxOn f s a) (hs : s nhds a) :
theorem IsLocalExtrOn.isLocalExtr {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : ) (hs : s nhds a) :
theorem IsMinOn.isLocalMin {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsMinOn f s a) (hs : s nhds a) :
theorem IsMaxOn.isLocalMax {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) (hs : s nhds a) :
theorem IsExtrOn.isLocalExtr {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsExtrOn f s a) (hs : s nhds a) :
theorem IsLocalMinOn.not_nhds_le_map {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} [] (hf : IsLocalMinOn f s a) [(nhdsWithin (f a) (Set.Iio (f a))).NeBot] :
theorem IsLocalMaxOn.not_nhds_le_map {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} [] (hf : IsLocalMaxOn f s a) [(nhdsWithin (f a) (Set.Ioi (f a))).NeBot] :
theorem IsLocalExtrOn.not_nhds_le_map {α : Type u} {β : Type v} [] [] {f : αβ} {s : Set α} {a : α} [] (hf : ) [(nhdsWithin (f a) (Set.Iio (f a))).NeBot] [(nhdsWithin (f a) (Set.Ioi (f a))).NeBot] :

### Constant #

theorem isLocalMinOn_const {α : Type u} {β : Type v} [] [] {s : Set α} {a : α} {b : β} :
IsLocalMinOn (fun (x : α) => b) s a
theorem isLocalMaxOn_const {α : Type u} {β : Type v} [] [] {s : Set α} {a : α} {b : β} :
IsLocalMaxOn (fun (x : α) => b) s a
theorem isLocalExtrOn_const {α : Type u} {β : Type v} [] [] {s : Set α} {a : α} {b : β} :
IsLocalExtrOn (fun (x : α) => b) s a
theorem isLocalMin_const {α : Type u} {β : Type v} [] [] {a : α} {b : β} :
IsLocalMin (fun (x : α) => b) a
theorem isLocalMax_const {α : Type u} {β : Type v} [] [] {a : α} {b : β} :
IsLocalMax (fun (x : α) => b) a
theorem isLocalExtr_const {α : Type u} {β : Type v} [] [] {a : α} {b : β} :
IsLocalExtr (fun (x : α) => b) a

### Composition with (anti)monotone functions #

theorem IsLocalMin.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {a : α} (hf : ) {g : βγ} (hg : ) :
IsLocalMin (g f) a
theorem IsLocalMax.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {a : α} (hf : ) {g : βγ} (hg : ) :
IsLocalMax (g f) a
theorem IsLocalExtr.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {a : α} (hf : ) {g : βγ} (hg : ) :
theorem IsLocalMin.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {a : α} (hf : ) {g : βγ} (hg : ) :
IsLocalMax (g f) a
theorem IsLocalMax.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {a : α} (hf : ) {g : βγ} (hg : ) :
IsLocalMin (g f) a
theorem IsLocalExtr.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {a : α} (hf : ) {g : βγ} (hg : ) :
theorem IsLocalMinOn.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {s : Set α} {a : α} (hf : IsLocalMinOn f s a) {g : βγ} (hg : ) :
IsLocalMinOn (g f) s a
theorem IsLocalMaxOn.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {s : Set α} {a : α} (hf : IsLocalMaxOn f s a) {g : βγ} (hg : ) :
IsLocalMaxOn (g f) s a
theorem IsLocalExtrOn.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {s : Set α} {a : α} (hf : ) {g : βγ} (hg : ) :
IsLocalExtrOn (g f) s a
theorem IsLocalMinOn.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {s : Set α} {a : α} (hf : IsLocalMinOn f s a) {g : βγ} (hg : ) :
IsLocalMaxOn (g f) s a
theorem IsLocalMaxOn.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {s : Set α} {a : α} (hf : IsLocalMaxOn f s a) {g : βγ} (hg : ) :
IsLocalMinOn (g f) s a
theorem IsLocalExtrOn.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] [] {f : αβ} {s : Set α} {a : α} (hf : ) {g : βγ} (hg : ) :
IsLocalExtrOn (g f) s a
theorem IsLocalMin.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [] [] [] {f : αβ} {a : α} [] {op : βγδ} (hop : ((fun (x x_1 : β) => x x_1) (fun (x x_1 : γ) => x x_1) fun (x x_1 : δ) => x x_1) op op) (hf : ) {g : αγ} (hg : ) :
IsLocalMin (fun (x : α) => op (f x) (g x)) a
theorem IsLocalMax.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [] [] [] {f : αβ} {a : α} [] {op : βγδ} (hop : ((fun (x x_1 : β) => x x_1) (fun (x x_1 : γ) => x x_1) fun (x x_1 : δ) => x x_1) op op) (hf : ) {g : αγ} (hg : ) :
IsLocalMax (fun (x : α) => op (f x) (g x)) a
theorem IsLocalMinOn.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [] [] [] {f : αβ} {s : Set α} {a : α} [] {op : βγδ} (hop : ((fun (x x_1 : β) => x x_1) (fun (x x_1 : γ) => x x_1) fun (x x_1 : δ) => x x_1) op op) (hf : IsLocalMinOn f s a) {g : αγ} (hg : IsLocalMinOn g s a) :
IsLocalMinOn (fun (x : α) => op (f x) (g x)) s a
theorem IsLocalMaxOn.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [] [] [] {f : αβ} {s : Set α} {a : α} [] {op : βγδ} (hop : ((fun (x x_1 : β) => x x_1) (fun (x x_1 : γ) => x x_1) fun (x x_1 : δ) => x x_1) op op) (hf : IsLocalMaxOn f s a) {g : αγ} (hg : IsLocalMaxOn g s a) :
IsLocalMaxOn (fun (x : α) => op (f x) (g x)) s a

### Composition with ContinuousAt#

theorem IsLocalMin.comp_continuous {α : Type u} {β : Type v} {δ : Type x} [] [] {f : αβ} [] {g : δα} {b : δ} (hf : IsLocalMin f (g b)) (hg : ) :
IsLocalMin (f g) b
theorem IsLocalMax.comp_continuous {α : Type u} {β : Type v} {δ : Type x} [] [] {f : αβ} [] {g : δα} {b : δ} (hf : IsLocalMax f (g b)) (hg : ) :
IsLocalMax (f g) b
theorem IsLocalExtr.comp_continuous {α : Type u} {β : Type v} {δ : Type x} [] [] {f : αβ} [] {g : δα} {b : δ} (hf : IsLocalExtr f (g b)) (hg : ) :
theorem IsLocalMin.comp_continuousOn {α : Type u} {β : Type v} {δ : Type x} [] [] {f : αβ} [] {s : Set δ} {g : δα} {b : δ} (hf : IsLocalMin f (g b)) (hg : ) (hb : b s) :
IsLocalMinOn (f g) s b
theorem IsLocalMax.comp_continuousOn {α : Type u} {β : Type v} {δ : Type x} [] [] {f : αβ} [] {s : Set δ} {g : δα} {b : δ} (hf : IsLocalMax f (g b)) (hg : ) (hb : b s) :
IsLocalMaxOn (f g) s b
theorem IsLocalExtr.comp_continuousOn {α : Type u} {β : Type v} {δ : Type x} [] [] {f : αβ} [] {s : Set δ} (g : δα) {b : δ} (hf : IsLocalExtr f (g b)) (hg : ) (hb : b s) :
IsLocalExtrOn (f g) s b
theorem IsLocalMinOn.comp_continuousOn {α : Type u} {β : Type v} {δ : Type x} [] [] {f : αβ} [] {t : Set α} {s : Set δ} {g : δα} {b : δ} (hf : IsLocalMinOn f t (g b)) (hst : s g ⁻¹' t) (hg : ) (hb : b s) :
IsLocalMinOn (f g) s b
theorem IsLocalMaxOn.comp_continuousOn {α : Type u} {β : Type v} {δ : Type x} [] [] {f : αβ} [] {t : Set α} {s : Set δ} {g : δα} {b : δ} (hf : IsLocalMaxOn f t (g b)) (hst : s g ⁻¹' t) (hg : ) (hb : b s) :
IsLocalMaxOn (f g) s b
theorem IsLocalExtrOn.comp_continuousOn {α : Type u} {β : Type v} {δ : Type x} [] [] {f : αβ} [] {t : Set α} {s : Set δ} (g : δα) {b : δ} (hf : IsLocalExtrOn f t (g b)) (hst : s g ⁻¹' t) (hg : ) (hb : b s) :
IsLocalExtrOn (f g) s b

theorem IsLocalMin.add {α : Type u} {β : Type v} [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMin (fun (x : α) => f x + g x) a
theorem IsLocalMax.add {α : Type u} {β : Type v} [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMax (fun (x : α) => f x + g x) a
theorem IsLocalMinOn.add {α : Type u} {β : Type v} [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMinOn f s a) (hg : IsLocalMinOn g s a) :
IsLocalMinOn (fun (x : α) => f x + g x) s a
theorem IsLocalMaxOn.add {α : Type u} {β : Type v} [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMaxOn f s a) (hg : IsLocalMaxOn g s a) :
IsLocalMaxOn (fun (x : α) => f x + g x) s a

### Pointwise negation and subtraction #

theorem IsLocalMin.neg {α : Type u} {β : Type v} [] {f : αβ} {a : α} (hf : ) :
IsLocalMax (fun (x : α) => -f x) a
theorem IsLocalMax.neg {α : Type u} {β : Type v} [] {f : αβ} {a : α} (hf : ) :
IsLocalMin (fun (x : α) => -f x) a
theorem IsLocalExtr.neg {α : Type u} {β : Type v} [] {f : αβ} {a : α} (hf : ) :
IsLocalExtr (fun (x : α) => -f x) a
theorem IsLocalMinOn.neg {α : Type u} {β : Type v} [] {f : αβ} {a : α} {s : Set α} (hf : IsLocalMinOn f s a) :
IsLocalMaxOn (fun (x : α) => -f x) s a
theorem IsLocalMaxOn.neg {α : Type u} {β : Type v} [] {f : αβ} {a : α} {s : Set α} (hf : IsLocalMaxOn f s a) :
IsLocalMinOn (fun (x : α) => -f x) s a
theorem IsLocalExtrOn.neg {α : Type u} {β : Type v} [] {f : αβ} {a : α} {s : Set α} (hf : ) :
IsLocalExtrOn (fun (x : α) => -f x) s a
theorem IsLocalMin.sub {α : Type u} {β : Type v} [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMin (fun (x : α) => f x - g x) a
theorem IsLocalMax.sub {α : Type u} {β : Type v} [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMax (fun (x : α) => f x - g x) a
theorem IsLocalMinOn.sub {α : Type u} {β : Type v} [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMinOn f s a) (hg : IsLocalMaxOn g s a) :
IsLocalMinOn (fun (x : α) => f x - g x) s a
theorem IsLocalMaxOn.sub {α : Type u} {β : Type v} [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMaxOn f s a) (hg : IsLocalMinOn g s a) :
IsLocalMaxOn (fun (x : α) => f x - g x) s a

### Pointwise sup/inf#

theorem IsLocalMin.sup {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMin (fun (x : α) => f x g x) a
theorem IsLocalMax.sup {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMax (fun (x : α) => f x g x) a
theorem IsLocalMinOn.sup {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMinOn f s a) (hg : IsLocalMinOn g s a) :
IsLocalMinOn (fun (x : α) => f x g x) s a
theorem IsLocalMaxOn.sup {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMaxOn f s a) (hg : IsLocalMaxOn g s a) :
IsLocalMaxOn (fun (x : α) => f x g x) s a
theorem IsLocalMin.inf {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMin (fun (x : α) => f x g x) a
theorem IsLocalMax.inf {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMax (fun (x : α) => f x g x) a
theorem IsLocalMinOn.inf {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMinOn f s a) (hg : IsLocalMinOn g s a) :
IsLocalMinOn (fun (x : α) => f x g x) s a
theorem IsLocalMaxOn.inf {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMaxOn f s a) (hg : IsLocalMaxOn g s a) :
IsLocalMaxOn (fun (x : α) => f x g x) s a

### Pointwise min/max#

theorem IsLocalMin.min {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMin (fun (x : α) => min (f x) (g x)) a
theorem IsLocalMax.min {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMax (fun (x : α) => min (f x) (g x)) a
theorem IsLocalMinOn.min {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMinOn f s a) (hg : IsLocalMinOn g s a) :
IsLocalMinOn (fun (x : α) => min (f x) (g x)) s a
theorem IsLocalMaxOn.min {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMaxOn f s a) (hg : IsLocalMaxOn g s a) :
IsLocalMaxOn (fun (x : α) => min (f x) (g x)) s a
theorem IsLocalMin.max {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMin (fun (x : α) => max (f x) (g x)) a
theorem IsLocalMax.max {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (hf : ) (hg : ) :
IsLocalMax (fun (x : α) => max (f x) (g x)) a
theorem IsLocalMinOn.max {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMinOn f s a) (hg : IsLocalMinOn g s a) :
IsLocalMinOn (fun (x : α) => max (f x) (g x)) s a
theorem IsLocalMaxOn.max {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsLocalMaxOn f s a) (hg : IsLocalMaxOn g s a) :
IsLocalMaxOn (fun (x : α) => max (f x) (g x)) s a

### Relation with eventually comparisons of two functions #

theorem Filter.EventuallyLE.isLocalMaxOn {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} {g : αβ} {a : α} (hle : g ≤ᶠ[] f) (hfga : f a = g a) (h : IsLocalMaxOn f s a) :
theorem IsLocalMaxOn.congr {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} {g : αβ} {a : α} (h : IsLocalMaxOn f s a) (heq : f =ᶠ[] g) (hmem : a s) :
theorem Filter.EventuallyEq.isLocalMaxOn_iff {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} {g : αβ} {a : α} (heq : f =ᶠ[] g) (hmem : a s) :
theorem Filter.EventuallyLE.isLocalMinOn {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} {g : αβ} {a : α} (hle : f ≤ᶠ[] g) (hfga : f a = g a) (h : IsLocalMinOn f s a) :
theorem IsLocalMinOn.congr {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} {g : αβ} {a : α} (h : IsLocalMinOn f s a) (heq : f =ᶠ[] g) (hmem : a s) :
theorem Filter.EventuallyEq.isLocalMinOn_iff {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} {g : αβ} {a : α} (heq : f =ᶠ[] g) (hmem : a s) :
theorem IsLocalExtrOn.congr {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} {g : αβ} {a : α} (h : ) (heq : f =ᶠ[] g) (hmem : a s) :
theorem Filter.EventuallyEq.isLocalExtrOn_iff {α : Type u} {β : Type v} [] [] {s : Set α} {f : αβ} {g : αβ} {a : α} (heq : f =ᶠ[] g) (hmem : a s) :
theorem Filter.EventuallyLE.isLocalMax {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (hle : g ≤ᶠ[nhds a] f) (hfga : f a = g a) (h : ) :
theorem IsLocalMax.congr {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (h : ) (heq : f =ᶠ[nhds a] g) :
theorem Filter.EventuallyEq.isLocalMax_iff {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (heq : f =ᶠ[nhds a] g) :
theorem Filter.EventuallyLE.isLocalMin {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (hle : f ≤ᶠ[nhds a] g) (hfga : f a = g a) (h : ) :
theorem IsLocalMin.congr {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (h : ) (heq : f =ᶠ[nhds a] g) :
theorem Filter.EventuallyEq.isLocalMin_iff {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (heq : f =ᶠ[nhds a] g) :
theorem IsLocalExtr.congr {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (h : ) (heq : f =ᶠ[nhds a] g) :
theorem Filter.EventuallyEq.isLocalExtr_iff {α : Type u} {β : Type v} [] [] {f : αβ} {g : αβ} {a : α} (heq : f =ᶠ[nhds a] g) :