Documentation

Mathlib.Topology.LocalExtr

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:

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
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
    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
      Instances For
        def IsLocalMin {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] (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} [TopologicalSpace α] [Preorder β] (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} [TopologicalSpace α] [Preorder β] (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} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} {p : Prop} :
              IsLocalExtrOn f s a(IsLocalMinOn f s ap) → (IsLocalMaxOn f s ap) → p
              theorem IsLocalExtr.elim {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {a : α} {p : Prop} :
              IsLocalExtr f a(IsLocalMin f ap) → (IsLocalMax f ap) → p

              Restriction to (sub)sets #

              theorem IsLocalMin.on {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {a : α} (h : IsLocalMin f a) (s : Set α) :
              theorem IsLocalMax.on {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {a : α} (h : IsLocalMax f a) (s : Set α) :
              theorem IsLocalExtr.on {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {a : α} (h : IsLocalExtr f a) (s : Set α) :
              theorem IsLocalMinOn.on_subset {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} {t : Set α} (hf : IsLocalMinOn f t a) (h : s t) :
              theorem IsLocalMaxOn.on_subset {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} {t : Set α} (hf : IsLocalMaxOn f t a) (h : s t) :
              theorem IsLocalExtrOn.on_subset {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} {t : Set α} (hf : IsLocalExtrOn f t a) (h : s t) :
              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) :
              theorem IsMaxOn.localize {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) :
              theorem IsExtrOn.localize {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsExtrOn 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) :
              theorem IsLocalMaxOn.isLocalMax {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsLocalMaxOn f s a) (hs : s nhds a) :
              theorem IsLocalExtrOn.isLocalExtr {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsLocalExtrOn f s a) (hs : s nhds a) :
              theorem IsMinOn.isLocalMin {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsMinOn f s a) (hs : s nhds a) :
              theorem IsMaxOn.isLocalMax {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) (hs : s nhds a) :
              theorem IsExtrOn.isLocalExtr {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsExtrOn f s a) (hs : s nhds a) :
              theorem IsLocalMinOn.not_nhds_le_map {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} [TopologicalSpace β] (hf : IsLocalMinOn f s a) [Filter.NeBot (nhdsWithin (f a) (Set.Iio (f a)))] :
              theorem IsLocalMaxOn.not_nhds_le_map {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} [TopologicalSpace β] (hf : IsLocalMaxOn f s a) [Filter.NeBot (nhdsWithin (f a) (Set.Ioi (f a)))] :
              theorem IsLocalExtrOn.not_nhds_le_map {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {s : Set α} {a : α} [TopologicalSpace β] (hf : IsLocalExtrOn f s a) [Filter.NeBot (nhdsWithin (f a) (Set.Iio (f a)))] [Filter.NeBot (nhdsWithin (f a) (Set.Ioi (f a)))] :

              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) :
              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) :
              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 : ((fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1) 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 : ((fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1) 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 : ((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} [TopologicalSpace α] [Preorder β] [Preorder γ] {f : αβ} {s : Set α} {a : α} [Preorder δ] {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} [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) :
              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 α] [OrderedAddCommMonoid β] {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 α] [OrderedAddCommMonoid β] {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 α] [OrderedAddCommMonoid β] {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 α] [OrderedAddCommMonoid β] {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 α] [OrderedAddCommGroup β] {f : αβ} {a : α} (hf : IsLocalMin f a) :
              IsLocalMax (fun x => -f x) a
              theorem IsLocalMax.neg {α : Type u} {β : Type v} [TopologicalSpace α] [OrderedAddCommGroup β] {f : αβ} {a : α} (hf : IsLocalMax f a) :
              IsLocalMin (fun x => -f x) a
              theorem IsLocalExtr.neg {α : Type u} {β : Type v} [TopologicalSpace α] [OrderedAddCommGroup β] {f : αβ} {a : α} (hf : IsLocalExtr f a) :
              IsLocalExtr (fun x => -f x) a
              theorem IsLocalMinOn.neg {α : Type u} {β : Type v} [TopologicalSpace α] [OrderedAddCommGroup β] {f : αβ} {a : α} {s : Set α} (hf : IsLocalMinOn f s a) :
              IsLocalMaxOn (fun x => -f x) s a
              theorem IsLocalMaxOn.neg {α : Type u} {β : Type v} [TopologicalSpace α] [OrderedAddCommGroup β] {f : αβ} {a : α} {s : Set α} (hf : IsLocalMaxOn f s a) :
              IsLocalMinOn (fun x => -f x) s a
              theorem IsLocalExtrOn.neg {α : Type u} {β : Type v} [TopologicalSpace α] [OrderedAddCommGroup β] {f : αβ} {a : α} {s : Set α} (hf : IsLocalExtrOn f s a) :
              IsLocalExtrOn (fun x => -f x) s a
              theorem IsLocalMin.sub {α : Type u} {β : Type v} [TopologicalSpace α] [OrderedAddCommGroup β] {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 α] [OrderedAddCommGroup β] {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 α] [OrderedAddCommGroup β] {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 α] [OrderedAddCommGroup β] {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} [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

              Pointwise min/max #

              theorem IsLocalMin.min {α : Type u} {β : Type v} [TopologicalSpace α] [LinearOrder β] {f : αβ} {g : αβ} {a : α} (hf : IsLocalMin f a) (hg : IsLocalMin g a) :
              IsLocalMin (fun x => 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 (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 (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 (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 (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 (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 (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 (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) :
              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) :
              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) :
              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) :
              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) :
              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) :
              theorem IsLocalMax.congr {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {g : αβ} {a : α} (h : IsLocalMax f a) (heq : f =ᶠ[nhds a] g) :
              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) :
              theorem IsLocalMin.congr {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {g : αβ} {a : α} (h : IsLocalMin f a) (heq : f =ᶠ[nhds a] g) :
              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) :
              theorem Filter.EventuallyEq.isLocalExtr_iff {α : Type u} {β : Type v} [TopologicalSpace α] [Preorder β] {f : αβ} {g : αβ} {a : α} (heq : f =ᶠ[nhds a] g) :