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 haveis_local_*_on f s aands ∈ 𝓝 a, then we haveis_local_* f a.
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
- 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 β] :
(α → β) → 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
- 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 β] :
(α → β) → 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
- is_local_extr_on f s a = is_extr_filter f (nhds_within a s) a
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
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
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 α} :
is_local_min_on f t a → 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 α} :
is_local_max_on f t a → 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 α} :
is_local_extr_on f t a → 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 : α} :
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 : α} :
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 : α} :
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 : α} :
is_local_min_on f s a → 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 : α} :
is_local_max_on f s a → 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 : α} :
is_local_extr_on f s a → 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 : α} :
is_min_on f s a → 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 : α} :
is_max_on f s a → 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 : α} :
is_extr_on f s a → s ∈ nhds a → is_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 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 : β → γ} :
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 : β → γ} :
monotone g → is_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 ≤ y → g 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 ≤ y → g 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 ≤ y → g 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 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 : β → γ} :
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 : β → γ} :
monotone g → is_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 ≤ y → g 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 ≤ y → g 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 ≤ y → g 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 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 : α → γ} :
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 : α → γ} :
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 : α → γ} :
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 : δ} :
is_local_min f (g b) → 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 : δ} :
is_local_max f (g b) → 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 : δ} :
is_local_extr f (g b) → 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 : δ} :
is_local_min f (g b) → continuous_on g s → 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 : δ} :
is_local_max f (g b) → continuous_on g s → 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 : δ} :
is_local_extr f (g b) → continuous_on g s → 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 : δ} :
is_local_min_on f t (g b) → s ⊆ g ⁻¹' t → continuous_on g s → 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 : δ} :
is_local_max_on f t (g b) → s ⊆ g ⁻¹' t → continuous_on g s → 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 : δ} :
is_local_extr_on f t (g b) → s ⊆ g ⁻¹' t → continuous_on g s → 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 : α} :
is_local_min f a → 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 : α} :
is_local_max f a → 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 α} :
is_local_min_on f s a → 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 α} :
is_local_max_on f s a → 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 : α} :
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 : α} :
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 : α} :
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 α} :
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 α} :
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 α} :
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 : α} :
is_local_min f a → 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 : α} :
is_local_max f a → 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 α} :
is_local_min_on f s a → 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 α} :
is_local_max_on f s a → 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 : α} :
is_local_min f a → 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 : α} :
is_local_max f a → 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 α} :
is_local_min_on f s a → 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 α} :
is_local_max_on f s a → 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 : α} :
is_local_min f a → 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 : α} :
is_local_max f a → 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 α} :
is_local_min_on f s a → 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 α} :
is_local_max_on f s a → is_local_max_on g s a → is_local_max_on (λ (x : α), f x ⊓ g x) s a
theorem
is_local_min.min
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order β]
{f g : α → β}
{a : α} :
is_local_min f a → is_local_min g a → is_local_min (λ (x : α), min (f x) (g x)) a
theorem
is_local_max.min
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order β]
{f g : α → β}
{a : α} :
is_local_max f a → is_local_max g a → is_local_max (λ (x : α), min (f x) (g x)) a
theorem
is_local_min_on.min
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order β]
{f g : α → β}
{a : α}
{s : set α} :
is_local_min_on f s a → is_local_min_on g s a → is_local_min_on (λ (x : α), min (f x) (g x)) s a
theorem
is_local_max_on.min
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order β]
{f g : α → β}
{a : α}
{s : set α} :
is_local_max_on f s a → is_local_max_on g s a → is_local_max_on (λ (x : α), min (f x) (g x)) s a
theorem
is_local_min.max
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order β]
{f g : α → β}
{a : α} :
is_local_min f a → is_local_min g a → is_local_min (λ (x : α), max (f x) (g x)) a
theorem
is_local_max.max
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order β]
{f g : α → β}
{a : α} :
is_local_max f a → is_local_max g a → is_local_max (λ (x : α), max (f x) (g x)) a
theorem
is_local_min_on.max
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order β]
{f g : α → β}
{a : α}
{s : set α} :
is_local_min_on f s a → is_local_min_on g s a → is_local_min_on (λ (x : α), max (f x) (g x)) s a
theorem
is_local_max_on.max
{α : Type u}
{β : Type v}
[topological_space α]
[decidable_linear_order β]
{f g : α → β}
{a : α}
{s : set α} :
is_local_max_on f s a → is_local_max_on g s a → is_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 ≤ᶠ[nhds_within a s] f → f a = g a → 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 : α} :
is_local_max_on f s a → f =ᶠ[nhds_within a s] g → 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 : α} :
f =ᶠ[nhds_within a s] g → 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 : α} :
f ≤ᶠ[nhds_within a s] g → f a = g a → 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 : α} :
is_local_min_on f s a → f =ᶠ[nhds_within a s] g → 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 : α} :
f =ᶠ[nhds_within a s] g → 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 : α} :
is_local_extr_on f s a → f =ᶠ[nhds_within a s] g → 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 : α} :
f =ᶠ[nhds_within a s] g → 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 : α} :
g ≤ᶠ[nhds a] f → f a = g a → 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 : α} :
is_local_max f a → 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 : α} :
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 : α} :
f ≤ᶠ[nhds a] g → f a = g a → 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 : α} :
is_local_min f a → 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 : α} :
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 : α} :
is_local_extr f a → 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 : α} :
f =ᶠ[nhds a] g → (is_local_extr f a ↔ is_local_extr g a)