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.lean 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.lean, and you can find
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
IsLocalMinOn
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
(f : α → β)
(s : Set α)
(a : α)
:
IsLocalMinOn f s a means that f a ≤ f x for all x ∈ s in some neighborhood of a.
Equations
- IsLocalMinOn f s a = IsMinFilter f (nhdsWithin a s) a
Instances For
def
IsLocalMaxOn
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
(f : α → β)
(s : Set α)
(a : α)
:
IsLocalMaxOn f s a means that f x ≤ f a for all x ∈ s in some neighborhood of a.
Equations
- IsLocalMaxOn f s a = IsMaxFilter f (nhdsWithin a s) a
Instances For
def
IsLocalExtrOn
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
(f : α → β)
(s : Set α)
(a : α)
:
IsLocalExtrOn f s a means IsLocalMinOn f s a ∨ IsLocalMaxOn f s a.
Equations
- IsLocalExtrOn f s a = IsExtrFilter f (nhdsWithin a s) a
Instances For
IsLocalMin f a means that f a ≤ f x for all x in some neighborhood of a.
Equations
- IsLocalMin f a = IsMinFilter f (nhds a) a
Instances For
IsLocalMax f a means that f x ≤ f a for all x ∈ s in some neighborhood of a.
Equations
- IsLocalMax f a = IsMaxFilter f (nhds a) a
Instances For
IsLocalExtr f s a means IsLocalMin f s a ∨ IsLocalMax f s a.
Equations
- IsLocalExtr f a = IsExtrFilter f (nhds a) a
Instances For
theorem
IsLocalExtrOn.elim
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
{p : Prop}
:
IsLocalExtrOn f s a → (IsLocalMinOn f s a → p) → (IsLocalMaxOn f s a → p) → p
theorem
IsLocalExtr.elim
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{a : α}
{p : Prop}
:
IsLocalExtr f a → (IsLocalMin f a → p) → (IsLocalMax f a → p) → p
Restriction to (sub)sets #
theorem
IsLocalMin.on
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{a : α}
(h : IsLocalMin f a)
(s : Set α)
:
IsLocalMinOn f s a
theorem
IsLocalMax.on
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{a : α}
(h : IsLocalMax f a)
(s : Set α)
:
IsLocalMaxOn f s a
theorem
IsLocalExtr.on
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{a : α}
(h : IsLocalExtr f a)
(s : Set α)
:
IsLocalExtrOn f s a
theorem
IsLocalMinOn.on_subset
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
{t : Set α}
(hf : IsLocalMinOn f t a)
(h : s ⊆ t)
:
IsLocalMinOn f s a
theorem
IsLocalMaxOn.on_subset
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
{t : Set α}
(hf : IsLocalMaxOn f t a)
(h : s ⊆ t)
:
IsLocalMaxOn f s a
theorem
IsLocalExtrOn.on_subset
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
{t : Set α}
(hf : IsLocalExtrOn f t a)
(h : s ⊆ t)
:
IsLocalExtrOn f s a
theorem
IsLocalMinOn.inter
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalMinOn f s a)
(t : Set α)
:
IsLocalMinOn f (s ∩ t) a
theorem
IsLocalMaxOn.inter
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalMaxOn f s a)
(t : Set α)
:
IsLocalMaxOn f (s ∩ t) a
theorem
IsLocalExtrOn.inter
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalExtrOn f s a)
(t : Set α)
:
IsLocalExtrOn f (s ∩ t) a
theorem
IsMinOn.localize
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsMinOn f s a)
:
IsLocalMinOn f s a
theorem
IsMaxOn.localize
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsMaxOn f s a)
:
IsLocalMaxOn f s a
theorem
IsExtrOn.localize
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsExtrOn f s a)
:
IsLocalExtrOn f s a
theorem
IsLocalMinOn.isLocalMin
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalMinOn f s a)
(hs : s ∈ nhds a)
:
IsLocalMin f a
theorem
IsLocalMaxOn.isLocalMax
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalMaxOn f s a)
(hs : s ∈ nhds a)
:
IsLocalMax f a
theorem
IsLocalExtrOn.isLocalExtr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalExtrOn f s a)
(hs : s ∈ nhds a)
:
IsLocalExtr f a
theorem
isLocalMinOn_univ_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{a : α}
:
theorem
isLocalMaxOn_univ_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{a : α}
:
theorem
isLocalExtrOn_univ_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{a : α}
:
theorem
IsMinOn.isLocalMin
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsMinOn f s a)
(hs : s ∈ nhds a)
:
IsLocalMin f a
theorem
IsMaxOn.isLocalMax
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsMaxOn f s a)
(hs : s ∈ nhds a)
:
IsLocalMax f a
theorem
IsExtrOn.isLocalExtr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsExtrOn f s a)
(hs : s ∈ nhds a)
:
IsLocalExtr f a
theorem
IsLocalMinOn.not_nhds_le_map
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
[TopologicalSpace β]
(hf : IsLocalMinOn f s a)
[(nhdsWithin (f a) (Set.Iio (f a))).NeBot]
:
theorem
IsLocalMaxOn.not_nhds_le_map
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
[TopologicalSpace β]
(hf : IsLocalMaxOn f s a)
[(nhdsWithin (f a) (Set.Ioi (f a))).NeBot]
:
theorem
IsLocalExtrOn.not_nhds_le_map
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
{s : Set α}
{a : α}
[TopologicalSpace β]
(hf : IsLocalExtrOn f s a)
[(nhdsWithin (f a) (Set.Iio (f a))).NeBot]
[(nhdsWithin (f a) (Set.Ioi (f a))).NeBot]
:
Constant #
theorem
isLocalMinOn_const
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{a : α}
{b : β}
:
IsLocalMinOn (fun (x : α) => b) s a
theorem
isLocalMaxOn_const
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{a : α}
{b : β}
:
IsLocalMaxOn (fun (x : α) => b) s a
theorem
isLocalExtrOn_const
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{a : α}
{b : β}
:
IsLocalExtrOn (fun (x : α) => b) s a
theorem
isLocalMin_const
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{a : α}
{b : β}
:
IsLocalMin (fun (x : α) => b) a
theorem
isLocalMax_const
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{a : α}
{b : β}
:
IsLocalMax (fun (x : α) => b) a
theorem
isLocalExtr_const
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{a : α}
{b : β}
:
IsLocalExtr (fun (x : α) => b) a
Composition with (anti)monotone functions #
theorem
IsLocalMin.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{a : α}
(hf : IsLocalMin f a)
{g : β → γ}
(hg : Monotone g)
:
IsLocalMin (g ∘ f) a
theorem
IsLocalMax.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{a : α}
(hf : IsLocalMax f a)
{g : β → γ}
(hg : Monotone g)
:
IsLocalMax (g ∘ f) a
theorem
IsLocalExtr.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{a : α}
(hf : IsLocalExtr f a)
{g : β → γ}
(hg : Monotone g)
:
IsLocalExtr (g ∘ f) a
theorem
IsLocalMin.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{a : α}
(hf : IsLocalMin f a)
{g : β → γ}
(hg : Antitone g)
:
IsLocalMax (g ∘ f) a
theorem
IsLocalMax.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{a : α}
(hf : IsLocalMax f a)
{g : β → γ}
(hg : Antitone g)
:
IsLocalMin (g ∘ f) a
theorem
IsLocalExtr.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{a : α}
(hf : IsLocalExtr f a)
{g : β → γ}
(hg : Antitone g)
:
IsLocalExtr (g ∘ f) a
theorem
IsLocalMinOn.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalMinOn f s a)
{g : β → γ}
(hg : Monotone g)
:
IsLocalMinOn (g ∘ f) s a
theorem
IsLocalMaxOn.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalMaxOn f s a)
{g : β → γ}
(hg : Monotone g)
:
IsLocalMaxOn (g ∘ f) s a
theorem
IsLocalExtrOn.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalExtrOn f s a)
{g : β → γ}
(hg : Monotone g)
:
IsLocalExtrOn (g ∘ f) s a
theorem
IsLocalMinOn.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalMinOn f s a)
{g : β → γ}
(hg : Antitone g)
:
IsLocalMaxOn (g ∘ f) s a
theorem
IsLocalMaxOn.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalMaxOn f s a)
{g : β → γ}
(hg : Antitone g)
:
IsLocalMinOn (g ∘ f) s a
theorem
IsLocalExtrOn.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{s : Set α}
{a : α}
(hf : IsLocalExtrOn f s a)
{g : β → γ}
(hg : Antitone g)
:
IsLocalExtrOn (g ∘ f) s a
theorem
IsLocalMin.bicomp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{a : α}
[Preorder δ]
{op : β → γ → δ}
(hop :
Relator.LiftFun (fun (x1 x2 : β) => x1 ≤ x2) (Relator.LiftFun (fun (x1 x2 : γ) => x1 ≤ x2) fun (x1 x2 : δ) => x1 ≤ x2)
op op)
(hf : IsLocalMin f a)
{g : α → γ}
(hg : IsLocalMin g a)
:
IsLocalMin (fun (x : α) => op (f x) (g x)) a
theorem
IsLocalMax.bicomp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{a : α}
[Preorder δ]
{op : β → γ → δ}
(hop :
Relator.LiftFun (fun (x1 x2 : β) => x1 ≤ x2) (Relator.LiftFun (fun (x1 x2 : γ) => x1 ≤ x2) fun (x1 x2 : δ) => x1 ≤ x2)
op op)
(hf : IsLocalMax f a)
{g : α → γ}
(hg : IsLocalMax g a)
:
IsLocalMax (fun (x : α) => op (f x) (g x)) a
theorem
IsLocalMinOn.bicomp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{s : Set α}
{a : α}
[Preorder δ]
{op : β → γ → δ}
(hop :
Relator.LiftFun (fun (x1 x2 : β) => x1 ≤ x2) (Relator.LiftFun (fun (x1 x2 : γ) => x1 ≤ x2) fun (x1 x2 : δ) => x1 ≤ x2)
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}
[TopologicalSpace α]
[Preorder β]
[Preorder γ]
{f : α → β}
{s : Set α}
{a : α}
[Preorder δ]
{op : β → γ → δ}
(hop :
Relator.LiftFun (fun (x1 x2 : β) => x1 ≤ x2) (Relator.LiftFun (fun (x1 x2 : γ) => x1 ≤ x2) fun (x1 x2 : δ) => x1 ≤ x2)
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}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
[TopologicalSpace δ]
{g : δ → α}
{b : δ}
(hf : IsLocalMin f (g b))
(hg : ContinuousAt g b)
:
IsLocalMin (f ∘ g) b
theorem
IsLocalMax.comp_continuous
{α : Type u}
{β : Type v}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
[TopologicalSpace δ]
{g : δ → α}
{b : δ}
(hf : IsLocalMax f (g b))
(hg : ContinuousAt g b)
:
IsLocalMax (f ∘ g) b
theorem
IsLocalExtr.comp_continuous
{α : Type u}
{β : Type v}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
[TopologicalSpace δ]
{g : δ → α}
{b : δ}
(hf : IsLocalExtr f (g b))
(hg : ContinuousAt g b)
:
IsLocalExtr (f ∘ g) b
theorem
IsLocalMin.comp_continuousOn
{α : Type u}
{β : Type v}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
[TopologicalSpace δ]
{s : Set δ}
{g : δ → α}
{b : δ}
(hf : IsLocalMin f (g b))
(hg : ContinuousOn g s)
(hb : b ∈ s)
:
IsLocalMinOn (f ∘ g) s b
theorem
IsLocalMax.comp_continuousOn
{α : Type u}
{β : Type v}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
[TopologicalSpace δ]
{s : Set δ}
{g : δ → α}
{b : δ}
(hf : IsLocalMax f (g b))
(hg : ContinuousOn g s)
(hb : b ∈ s)
:
IsLocalMaxOn (f ∘ g) s b
theorem
IsLocalExtr.comp_continuousOn
{α : Type u}
{β : Type v}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
[TopologicalSpace δ]
{s : Set δ}
(g : δ → α)
{b : δ}
(hf : IsLocalExtr f (g b))
(hg : ContinuousOn g s)
(hb : b ∈ s)
:
IsLocalExtrOn (f ∘ g) s b
theorem
IsLocalMinOn.comp_continuousOn
{α : Type u}
{β : Type v}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
[TopologicalSpace δ]
{t : Set α}
{s : Set δ}
{g : δ → α}
{b : δ}
(hf : IsLocalMinOn f t (g b))
(hst : s ⊆ g ⁻¹' t)
(hg : ContinuousOn g s)
(hb : b ∈ s)
:
IsLocalMinOn (f ∘ g) s b
theorem
IsLocalMaxOn.comp_continuousOn
{α : Type u}
{β : Type v}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
[TopologicalSpace δ]
{t : Set α}
{s : Set δ}
{g : δ → α}
{b : δ}
(hf : IsLocalMaxOn f t (g b))
(hst : s ⊆ g ⁻¹' t)
(hg : ContinuousOn g s)
(hb : b ∈ s)
:
IsLocalMaxOn (f ∘ g) s b
theorem
IsLocalExtrOn.comp_continuousOn
{α : Type u}
{β : Type v}
{δ : Type x}
[TopologicalSpace α]
[Preorder β]
{f : α → β}
[TopologicalSpace δ]
{t : Set α}
{s : Set δ}
(g : δ → α)
{b : δ}
(hf : IsLocalExtrOn f t (g b))
(hst : s ⊆ g ⁻¹' t)
(hg : ContinuousOn g s)
(hb : b ∈ s)
:
IsLocalExtrOn (f ∘ g) s b
Pointwise addition #
theorem
IsLocalMin.add
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommMonoid β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f g : α → β}
{a : α}
(hf : IsLocalMin f a)
(hg : IsLocalMin g a)
:
IsLocalMin (fun (x : α) => f x + g x) a
theorem
IsLocalMax.add
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommMonoid β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f g : α → β}
{a : α}
(hf : IsLocalMax f a)
(hg : IsLocalMax g a)
:
IsLocalMax (fun (x : α) => f x + g x) a
theorem
IsLocalMinOn.add
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommMonoid β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{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}
[TopologicalSpace α]
[AddCommMonoid β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{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}
[TopologicalSpace α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f : α → β}
{a : α}
(hf : IsLocalMin f a)
:
IsLocalMax (fun (x : α) => -f x) a
theorem
IsLocalMax.neg
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f : α → β}
{a : α}
(hf : IsLocalMax f a)
:
IsLocalMin (fun (x : α) => -f x) a
theorem
IsLocalExtr.neg
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f : α → β}
{a : α}
(hf : IsLocalExtr f a)
:
IsLocalExtr (fun (x : α) => -f x) a
theorem
IsLocalMinOn.neg
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f : α → β}
{a : α}
{s : Set α}
(hf : IsLocalMinOn f s a)
:
IsLocalMaxOn (fun (x : α) => -f x) s a
theorem
IsLocalMaxOn.neg
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f : α → β}
{a : α}
{s : Set α}
(hf : IsLocalMaxOn f s a)
:
IsLocalMinOn (fun (x : α) => -f x) s a
theorem
IsLocalExtrOn.neg
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f : α → β}
{a : α}
{s : Set α}
(hf : IsLocalExtrOn f s a)
:
IsLocalExtrOn (fun (x : α) => -f x) s a
theorem
IsLocalMin.sub
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f g : α → β}
{a : α}
(hf : IsLocalMin f a)
(hg : IsLocalMax g a)
:
IsLocalMin (fun (x : α) => f x - g x) a
theorem
IsLocalMax.sub
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f g : α → β}
{a : α}
(hf : IsLocalMax f a)
(hg : IsLocalMin g a)
:
IsLocalMax (fun (x : α) => f x - g x) a
theorem
IsLocalMinOn.sub
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{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}
[TopologicalSpace α]
[AddCommGroup β]
[PartialOrder β]
[IsOrderedAddMonoid β]
{f g : α → β}
{a : α}
{s : Set α}
(hf : IsLocalMaxOn f s a)
(hg : IsLocalMinOn g s a)
:
IsLocalMaxOn (fun (x : α) => f x - g x) s a
theorem
IsLocalMin.sup
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[SemilatticeSup β]
{f g : α → β}
{a : α}
(hf : IsLocalMin f a)
(hg : IsLocalMin g a)
:
IsLocalMin (fun (x : α) => f x ⊔ g x) a
theorem
IsLocalMax.sup
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[SemilatticeSup β]
{f g : α → β}
{a : α}
(hf : IsLocalMax f a)
(hg : IsLocalMax g a)
:
IsLocalMax (fun (x : α) => f x ⊔ g x) a
theorem
IsLocalMinOn.sup
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[SemilatticeSup β]
{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}
[TopologicalSpace α]
[SemilatticeSup β]
{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}
[TopologicalSpace α]
[SemilatticeInf β]
{f g : α → β}
{a : α}
(hf : IsLocalMin f a)
(hg : IsLocalMin g a)
:
IsLocalMin (fun (x : α) => f x ⊓ g x) a
theorem
IsLocalMax.inf
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[SemilatticeInf β]
{f g : α → β}
{a : α}
(hf : IsLocalMax f a)
(hg : IsLocalMax g a)
:
IsLocalMax (fun (x : α) => f x ⊓ g x) a
theorem
IsLocalMinOn.inf
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[SemilatticeInf β]
{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}
[TopologicalSpace α]
[SemilatticeInf β]
{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.min
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
(hf : IsLocalMin f a)
(hg : IsLocalMin g a)
:
IsLocalMin (fun (x : α) => Min.min (f x) (g x)) a
theorem
IsLocalMax.min
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
(hf : IsLocalMax f a)
(hg : IsLocalMax g a)
:
IsLocalMax (fun (x : α) => Min.min (f x) (g x)) a
theorem
IsLocalMinOn.min
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
{s : Set α}
(hf : IsLocalMinOn f s a)
(hg : IsLocalMinOn g s a)
:
IsLocalMinOn (fun (x : α) => Min.min (f x) (g x)) s a
theorem
IsLocalMaxOn.min
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
{s : Set α}
(hf : IsLocalMaxOn f s a)
(hg : IsLocalMaxOn g s a)
:
IsLocalMaxOn (fun (x : α) => Min.min (f x) (g x)) s a
theorem
IsLocalMin.max
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
(hf : IsLocalMin f a)
(hg : IsLocalMin g a)
:
IsLocalMin (fun (x : α) => Max.max (f x) (g x)) a
theorem
IsLocalMax.max
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
(hf : IsLocalMax f a)
(hg : IsLocalMax g a)
:
IsLocalMax (fun (x : α) => Max.max (f x) (g x)) a
theorem
IsLocalMinOn.max
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
{s : Set α}
(hf : IsLocalMinOn f s a)
(hg : IsLocalMinOn g s a)
:
IsLocalMinOn (fun (x : α) => Max.max (f x) (g x)) s a
theorem
IsLocalMaxOn.max
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[LinearOrder β]
{f g : α → β}
{a : α}
{s : Set α}
(hf : IsLocalMaxOn f s a)
(hg : IsLocalMaxOn g s a)
:
IsLocalMaxOn (fun (x : α) => Max.max (f x) (g x)) s a
Relation with eventually comparisons of two functions #
theorem
Filter.EventuallyLE.isLocalMaxOn
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{f g : α → β}
{a : α}
(hle : g ≤ᶠ[nhdsWithin a s] f)
(hfga : f a = g a)
(h : IsLocalMaxOn f s a)
:
IsLocalMaxOn g s a
theorem
IsLocalMaxOn.congr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{f g : α → β}
{a : α}
(h : IsLocalMaxOn f s a)
(heq : f =ᶠ[nhdsWithin a s] g)
(hmem : a ∈ s)
:
IsLocalMaxOn g s a
theorem
Filter.EventuallyEq.isLocalMaxOn_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{f g : α → β}
{a : α}
(heq : f =ᶠ[nhdsWithin a s] g)
(hmem : a ∈ s)
:
theorem
Filter.EventuallyLE.isLocalMinOn
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{f g : α → β}
{a : α}
(hle : f ≤ᶠ[nhdsWithin a s] g)
(hfga : f a = g a)
(h : IsLocalMinOn f s a)
:
IsLocalMinOn g s a
theorem
IsLocalMinOn.congr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{f g : α → β}
{a : α}
(h : IsLocalMinOn f s a)
(heq : f =ᶠ[nhdsWithin a s] g)
(hmem : a ∈ s)
:
IsLocalMinOn g s a
theorem
Filter.EventuallyEq.isLocalMinOn_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{f g : α → β}
{a : α}
(heq : f =ᶠ[nhdsWithin a s] g)
(hmem : a ∈ s)
:
theorem
IsLocalExtrOn.congr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{f g : α → β}
{a : α}
(h : IsLocalExtrOn f s a)
(heq : f =ᶠ[nhdsWithin a s] g)
(hmem : a ∈ s)
:
IsLocalExtrOn g s a
theorem
Filter.EventuallyEq.isLocalExtrOn_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{s : Set α}
{f g : α → β}
{a : α}
(heq : f =ᶠ[nhdsWithin a s] g)
(hmem : a ∈ s)
:
theorem
Filter.EventuallyLE.isLocalMax
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f g : α → β}
{a : α}
(hle : g ≤ᶠ[nhds a] f)
(hfga : f a = g a)
(h : IsLocalMax f a)
:
IsLocalMax g a
theorem
IsLocalMax.congr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f g : α → β}
{a : α}
(h : IsLocalMax f a)
(heq : f =ᶠ[nhds a] g)
:
IsLocalMax g a
theorem
Filter.EventuallyEq.isLocalMax_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f g : α → β}
{a : α}
(heq : f =ᶠ[nhds a] g)
:
theorem
Filter.EventuallyLE.isLocalMin
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f g : α → β}
{a : α}
(hle : f ≤ᶠ[nhds a] g)
(hfga : f a = g a)
(h : IsLocalMin f a)
:
IsLocalMin g a
theorem
IsLocalMin.congr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f g : α → β}
{a : α}
(h : IsLocalMin f a)
(heq : f =ᶠ[nhds a] g)
:
IsLocalMin g a
theorem
Filter.EventuallyEq.isLocalMin_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f g : α → β}
{a : α}
(heq : f =ᶠ[nhds a] g)
:
theorem
IsLocalExtr.congr
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f g : α → β}
{a : α}
(h : IsLocalExtr f a)
(heq : f =ᶠ[nhds a] g)
:
IsLocalExtr g a
theorem
Filter.EventuallyEq.isLocalExtr_iff
{α : Type u}
{β : Type v}
[TopologicalSpace α]
[Preorder β]
{f g : α → β}
{a : α}
(heq : f =ᶠ[nhds a] g)
:
theorem
isLocalMax_of_mono_anti'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
{β : Type u_2}
[Preorder β]
{b : α}
{f : α → β}
{a : Set α}
(ha : a ∈ nhdsWithin b (Set.Iic b))
{c : Set α}
(hc : c ∈ nhdsWithin b (Set.Ici b))
(h₀ : MonotoneOn f a)
(h₁ : AntitoneOn f c)
:
IsLocalMax f b
If f is monotone to the left and antitone to the right, then it has a local maximum.
theorem
isLocalMin_of_anti_mono'
{α : Type u_1}
[TopologicalSpace α]
[LinearOrder α]
{β : Type u_2}
[Preorder β]
{b : α}
{f : α → β}
{a : Set α}
(ha : a ∈ nhdsWithin b (Set.Iic b))
{c : Set α}
(hc : c ∈ nhdsWithin b (Set.Ici b))
(h₀ : AntitoneOn f a)
(h₁ : MonotoneOn f c)
:
IsLocalMin f b
If f is antitone to the left and monotone to the right, then it has a local minimum.