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:
def
is_local_min_on
{α : Type u}
{β : Type v}
[topological_space α]
[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
- is_local_min_on f s a = is_min_filter f (nhds_within a s) a
def
is_local_max_on
{α : Type u}
{β : Type v}
[topological_space α]
[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
- is_local_max_on f s a = is_max_filter f (nhds_within a s) a
def
is_local_extr_on
{α : Type u}
{β : Type v}
[topological_space α]
[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
- is_local_extr_on f s a = is_extr_filter f (nhds_within a s) a
def
is_local_min
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
(f : α → β)
(a : α) :
Prop
is_local_min f a means that f a ≤ f x for all x in some neighborhood of a.
Equations
- is_local_min f a = is_min_filter f (nhds a) a
def
is_local_max
{α : Type u}
{β : Type v}
[topological_space α]
[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
- is_local_max f a = is_max_filter f (nhds a) a
def
is_local_extr
{α : Type u}
{β : Type v}
[topological_space α]
[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
- is_local_extr f a = is_extr_filter f (nhds a) a
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 α) :
is_local_min_on f s a
theorem
is_local_max.on
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{a : α}
(h : is_local_max f a)
(s : set α) :
is_local_max_on f s a
theorem
is_local_extr.on
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{a : α}
(h : is_local_extr f a)
(s : set α) :
is_local_extr_on f s a
theorem
is_local_min_on.on_subset
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
{t : set α}
(hf : is_local_min_on f t a)
(h : s ⊆ t) :
is_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 α}
(hf : is_local_max_on f t a)
(h : s ⊆ t) :
is_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 α}
(hf : is_local_extr_on f t a)
(h : s ⊆ t) :
is_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 α) :
is_local_min_on f (s ∩ t) a
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 α) :
is_local_max_on f (s ∩ t) a
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 α) :
is_local_extr_on f (s ∩ t) a
theorem
is_min_on.localize
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(hf : is_min_on f s a) :
is_local_min_on f s a
theorem
is_max_on.localize
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(hf : is_max_on f s a) :
is_local_max_on f s a
theorem
is_extr_on.localize
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(hf : is_extr_on f s a) :
is_local_extr_on f s a
theorem
is_local_min_on.is_local_min
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(hf : is_local_min_on f s a)
(hs : s ∈ nhds a) :
is_local_min f a
theorem
is_local_max_on.is_local_max
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(hf : is_local_max_on f s a)
(hs : s ∈ nhds a) :
is_local_max f a
theorem
is_local_extr_on.is_local_extr
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(hf : is_local_extr_on f s a)
(hs : s ∈ nhds a) :
is_local_extr f a
theorem
is_min_on.is_local_min
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(hf : is_min_on f s a)
(hs : s ∈ nhds a) :
is_local_min f a
theorem
is_max_on.is_local_max
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(hf : is_max_on f s a)
(hs : s ∈ nhds a) :
is_local_max f a
theorem
is_extr_on.is_local_extr
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(hf : is_extr_on f s a)
(hs : s ∈ nhds a) :
is_local_extr f a
theorem
is_local_min_on.not_nhds_le_map
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
[topological_space β]
(hf : is_local_min_on f s a)
[(nhds_within (f a) (set.Iio (f a))).ne_bot] :
¬nhds (f a) ≤ filter.map f (nhds_within a s)
theorem
is_local_max_on.not_nhds_le_map
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
[topological_space β]
(hf : is_local_max_on f s a)
[(nhds_within (f a) (set.Ioi (f a))).ne_bot] :
¬nhds (f a) ≤ filter.map f (nhds_within a s)
theorem
is_local_extr_on.not_nhds_le_map
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f : α → β}
{s : set α}
{a : α}
[topological_space β]
(hf : is_local_extr_on f s a)
[(nhds_within (f a) (set.Iio (f a))).ne_bot]
[(nhds_within (f a) (set.Ioi (f a))).ne_bot] :
¬nhds (f a) ≤ filter.map f (nhds_within a s)
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 : β → γ}
(hg : monotone g) :
is_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 : β → γ}
(hg : monotone g) :
is_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 : β → γ}
(hg : monotone g) :
is_local_extr (g ∘ f) a
theorem
is_local_min.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[preorder β]
[preorder γ]
{f : α → β}
{a : α}
(hf : is_local_min f a)
{g : β → γ}
(hg : antitone g) :
is_local_max (g ∘ f) a
theorem
is_local_max.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[preorder β]
[preorder γ]
{f : α → β}
{a : α}
(hf : is_local_max f a)
{g : β → γ}
(hg : antitone g) :
is_local_min (g ∘ f) a
theorem
is_local_extr.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[preorder β]
[preorder γ]
{f : α → β}
{a : α}
(hf : is_local_extr f a)
{g : β → γ}
(hg : antitone g) :
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 : β → γ}
(hg : monotone g) :
is_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 : β → γ}
(hg : monotone g) :
is_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 : β → γ}
(hg : monotone g) :
is_local_extr_on (g ∘ f) s a
theorem
is_local_min_on.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[preorder β]
[preorder γ]
{f : α → β}
{s : set α}
{a : α}
(hf : is_local_min_on f s a)
{g : β → γ}
(hg : antitone g) :
is_local_max_on (g ∘ f) s a
theorem
is_local_max_on.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[preorder β]
[preorder γ]
{f : α → β}
{s : set α}
{a : α}
(hf : is_local_max_on f s a)
{g : β → γ}
(hg : antitone g) :
is_local_min_on (g ∘ f) s a
theorem
is_local_extr_on.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[topological_space α]
[preorder β]
[preorder γ]
{f : α → β}
{s : set α}
{a : α}
(hf : is_local_extr_on f s a)
{g : β → γ}
(hg : antitone g) :
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 : α → γ}
(hg : is_local_min g 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}
[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 : α → γ}
(hg : is_local_max g 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}
[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 : α → γ}
(hg : is_local_min_on g s 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}
[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 : α → γ}
(hg : is_local_max_on g s 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}
[topological_space α]
[preorder β]
{f : α → β}
[topological_space δ]
{g : δ → α}
{b : δ}
(hf : is_local_min f (g b))
(hg : continuous_at g b) :
is_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 : δ}
(hf : is_local_max f (g b))
(hg : continuous_at g b) :
is_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 : δ}
(hf : is_local_extr f (g b))
(hg : continuous_at g b) :
is_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 : δ}
(hf : is_local_min f (g b))
(hg : continuous_on g s)
(hb : b ∈ s) :
is_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 : δ}
(hf : is_local_max f (g b))
(hg : continuous_on g s)
(hb : b ∈ s) :
is_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 : δ}
(hf : is_local_extr f (g b))
(hg : continuous_on g s)
(hb : b ∈ s) :
is_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 : δ}
(hf : is_local_min_on f t (g b))
(hst : s ⊆ g ⁻¹' t)
(hg : continuous_on g s)
(hb : b ∈ s) :
is_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 : δ}
(hf : is_local_max_on f t (g b))
(hst : s ⊆ g ⁻¹' t)
(hg : continuous_on g s)
(hb : b ∈ s) :
is_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 : δ}
(hf : is_local_extr_on f t (g b))
(hst : s ⊆ g ⁻¹' t)
(hg : continuous_on g s)
(hb : b ∈ s) :
is_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 : α}
(hf : is_local_min f a)
(hg : is_local_min g a) :
is_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 : α}
(hf : is_local_max f a)
(hg : is_local_max g a) :
is_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 α}
(hf : is_local_min_on f s a)
(hg : is_local_min_on g s a) :
is_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 α}
(hf : is_local_max_on f s a)
(hg : is_local_max_on g s 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}
[topological_space α]
[ordered_add_comm_group β]
{f : α → β}
{a : α}
(hf : is_local_min f a) :
is_local_max (λ (x : α), -f x) a
theorem
is_local_max.neg
{α : Type u}
{β : Type v}
[topological_space α]
[ordered_add_comm_group β]
{f : α → β}
{a : α}
(hf : is_local_max f a) :
is_local_min (λ (x : α), -f x) a
theorem
is_local_extr.neg
{α : Type u}
{β : Type v}
[topological_space α]
[ordered_add_comm_group β]
{f : α → β}
{a : α}
(hf : is_local_extr f a) :
is_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 α}
(hf : is_local_min_on f s a) :
is_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 α}
(hf : is_local_max_on f s a) :
is_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 α}
(hf : is_local_extr_on f s a) :
is_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 : α}
(hf : is_local_min f a)
(hg : is_local_max g a) :
is_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 : α}
(hf : is_local_max f a)
(hg : is_local_min g a) :
is_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 α}
(hf : is_local_min_on f s a)
(hg : is_local_max_on g s a) :
is_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 α}
(hf : is_local_max_on f s a)
(hg : is_local_min_on g s a) :
is_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 : α}
(hf : is_local_min f a)
(hg : is_local_min g a) :
is_local_min (λ (x : α), f x ⊔ g x) a
theorem
is_local_max.sup
{α : Type u}
{β : Type v}
[topological_space α]
[semilattice_sup β]
{f g : α → β}
{a : α}
(hf : is_local_max f a)
(hg : is_local_max g a) :
is_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 α}
(hf : is_local_min_on f s a)
(hg : is_local_min_on g s a) :
is_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 α}
(hf : is_local_max_on f s a)
(hg : is_local_max_on g s a) :
is_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 : α}
(hf : is_local_min f a)
(hg : is_local_min g a) :
is_local_min (λ (x : α), f x ⊓ g x) a
theorem
is_local_max.inf
{α : Type u}
{β : Type v}
[topological_space α]
[semilattice_inf β]
{f g : α → β}
{a : α}
(hf : is_local_max f a)
(hg : is_local_max g a) :
is_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 α}
(hf : is_local_min_on f s a)
(hg : is_local_min_on g s a) :
is_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 α}
(hf : is_local_max_on f s a)
(hg : is_local_max_on g s a) :
is_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 : α}
(hf : is_local_min f a)
(hg : is_local_min g a) :
is_local_min (λ (x : α), linear_order.min (f x) (g x)) a
theorem
is_local_max.min
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order β]
{f g : α → β}
{a : α}
(hf : is_local_max f a)
(hg : is_local_max g a) :
is_local_max (λ (x : α), linear_order.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 α}
(hf : is_local_min_on f s a)
(hg : is_local_min_on g s 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}
[topological_space α]
[linear_order β]
{f g : α → β}
{a : α}
{s : set α}
(hf : is_local_max_on f s a)
(hg : is_local_max_on g s a) :
is_local_max_on (λ (x : α), linear_order.min (f x) (g x)) s a
theorem
is_local_min.max
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order β]
{f g : α → β}
{a : α}
(hf : is_local_min f a)
(hg : is_local_min g a) :
is_local_min (λ (x : α), linear_order.max (f x) (g x)) a
theorem
is_local_max.max
{α : Type u}
{β : Type v}
[topological_space α]
[linear_order β]
{f g : α → β}
{a : α}
(hf : is_local_max f a)
(hg : is_local_max g a) :
is_local_max (λ (x : α), linear_order.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 α}
(hf : is_local_min_on f s a)
(hg : is_local_min_on g s 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}
[topological_space α]
[linear_order β]
{f g : α → β}
{a : α}
{s : set α}
(hf : is_local_max_on f s a)
(hg : is_local_max_on g s 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}
[topological_space α]
[preorder β]
{s : set α}
{f g : α → β}
{a : α}
(hle : g ≤ᶠ[nhds_within a s] f)
(hfga : f a = g a)
(h : is_local_max_on f s a) :
is_local_max_on g s a
theorem
is_local_max_on.congr
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{s : set α}
{f g : α → β}
{a : α}
(h : is_local_max_on f s a)
(heq : f =ᶠ[nhds_within a s] g)
(hmem : a ∈ s) :
is_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 : α}
(heq : f =ᶠ[nhds_within a s] g)
(hmem : a ∈ 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 : α}
(hle : f ≤ᶠ[nhds_within a s] g)
(hfga : f a = g a)
(h : is_local_min_on f s a) :
is_local_min_on g s a
theorem
is_local_min_on.congr
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{s : set α}
{f g : α → β}
{a : α}
(h : is_local_min_on f s a)
(heq : f =ᶠ[nhds_within a s] g)
(hmem : a ∈ s) :
is_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 : α}
(heq : f =ᶠ[nhds_within a s] g)
(hmem : a ∈ 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 : α}
(h : is_local_extr_on f s a)
(heq : f =ᶠ[nhds_within a s] g)
(hmem : a ∈ s) :
is_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 : α}
(heq : f =ᶠ[nhds_within a s] g)
(hmem : a ∈ 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 : α}
(hle : g ≤ᶠ[nhds a] f)
(hfga : f a = g a)
(h : is_local_max f a) :
is_local_max g a
theorem
is_local_max.congr
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f g : α → β}
{a : α}
(h : is_local_max f a)
(heq : f =ᶠ[nhds a] g) :
is_local_max g a
theorem
filter.eventually_eq.is_local_max_iff
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f g : α → β}
{a : α}
(heq : f =ᶠ[nhds a] g) :
is_local_max f a ↔ is_local_max g a
theorem
filter.eventually_le.is_local_min
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f g : α → β}
{a : α}
(hle : f ≤ᶠ[nhds a] g)
(hfga : f a = g a)
(h : is_local_min f a) :
is_local_min g a
theorem
is_local_min.congr
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f g : α → β}
{a : α}
(h : is_local_min f a)
(heq : f =ᶠ[nhds a] g) :
is_local_min g a
theorem
filter.eventually_eq.is_local_min_iff
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f g : α → β}
{a : α}
(heq : f =ᶠ[nhds a] g) :
is_local_min f a ↔ is_local_min g a
theorem
is_local_extr.congr
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f g : α → β}
{a : α}
(h : is_local_extr f a)
(heq : f =ᶠ[nhds a] g) :
is_local_extr g a
theorem
filter.eventually_eq.is_local_extr_iff
{α : Type u}
{β : Type v}
[topological_space α]
[preorder β]
{f g : α → β}
{a : α}
(heq : f =ᶠ[nhds a] g) :
is_local_extr f a ↔ is_local_extr g a