Documentation

Mathlib.Order.Filter.Extr

Minimum and maximum w.r.t. a filter and on a set #

Main Definitions #

This file defines six predicates of the form isAB, where A is Min, Max, or Extr, and B is Filter or On.

Similar predicates with on suffix are particular cases for l = 𝓟 s.

Main statements #

Change of the filter (set) argument #

Composition #

Algebraic operations #

Miscellaneous definitions #

Missing features (TODO) #

Definitions #

def IsMinFilter {α : Type u} {β : Type v} [Preorder β] (f : αβ) (l : Filter α) (a : α) :

IsMinFilter f l a means that f a ≤ f x for all x in some l-neighborhood of a

Equations
Instances For
    def IsMaxFilter {α : Type u} {β : Type v} [Preorder β] (f : αβ) (l : Filter α) (a : α) :

    is_maxFilter f l a means that f x ≤ f a for all x in some l-neighborhood of a

    Equations
    Instances For
      def IsExtrFilter {α : Type u} {β : Type v} [Preorder β] (f : αβ) (l : Filter α) (a : α) :

      IsExtrFilter f l a means IsMinFilter f l a or IsMaxFilter f l a

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

        IsMinOn f s a means that f a ≤ f x for all x ∈ s. Note that we do not assume a ∈ s.

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

          IsMaxOn f s a means that f x ≤ f a for all x ∈ s. Note that we do not assume a ∈ s.

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

            IsExtrOn f s a means IsMinOn f s a or IsMaxOn f s a

            Equations
            Instances For
              theorem IsExtrOn.elim {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} {p : Prop} :
              IsExtrOn f s a(IsMinOn f s ap)(IsMaxOn f s ap)p
              theorem isMinOn_iff {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsMinOn f s a xs, f a f x
              theorem isMaxOn_iff {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsMaxOn f s a xs, f x f a
              theorem isMinOn_univ_iff {α : Type u} {β : Type v} [Preorder β] {f : αβ} {a : α} :
              IsMinOn f Set.univ a ∀ (x : α), f a f x
              theorem isMaxOn_univ_iff {α : Type u} {β : Type v} [Preorder β] {f : αβ} {a : α} :
              IsMaxOn f Set.univ a ∀ (x : α), f x f a
              theorem IsMinFilter.tendsto_principal_Ici {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} (h : IsMinFilter f l a) :
              theorem IsMaxFilter.tendsto_principal_Iic {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} (h : IsMaxFilter f l a) :

              Conversion to IsExtr* #

              theorem IsMinFilter.isExtr {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsMinFilter f l aIsExtrFilter f l a
              theorem IsMaxFilter.isExtr {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsMaxFilter f l aIsExtrFilter f l a
              theorem IsMinOn.isExtr {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} (h : IsMinOn f s a) :
              IsExtrOn f s a
              theorem IsMaxOn.isExtr {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} (h : IsMaxOn f s a) :
              IsExtrOn f s a

              Constant function #

              theorem isMinFilter_const {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {a : α} {b : β} :
              IsMinFilter (fun (x : α) => b) l a
              theorem isMaxFilter_const {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {a : α} {b : β} :
              IsMaxFilter (fun (x : α) => b) l a
              theorem isExtrFilter_const {α : Type u} {β : Type v} [Preorder β] {l : Filter α} {a : α} {b : β} :
              IsExtrFilter (fun (x : α) => b) l a
              theorem isMinOn_const {α : Type u} {β : Type v} [Preorder β] {s : Set α} {a : α} {b : β} :
              IsMinOn (fun (x : α) => b) s a
              theorem isMaxOn_const {α : Type u} {β : Type v} [Preorder β] {s : Set α} {a : α} {b : β} :
              IsMaxOn (fun (x : α) => b) s a
              theorem isExtrOn_const {α : Type u} {β : Type v} [Preorder β] {s : Set α} {a : α} {b : β} :
              IsExtrOn (fun (x : α) => b) s a

              Order dual #

              theorem isMinFilter_dual_iff {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsMinFilter (OrderDual.toDual f) l a IsMaxFilter f l a
              theorem isMaxFilter_dual_iff {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsMaxFilter (OrderDual.toDual f) l a IsMinFilter f l a
              theorem isExtrFilter_dual_iff {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsExtrFilter (OrderDual.toDual f) l a IsExtrFilter f l a
              theorem IsMaxFilter.dual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsMaxFilter f l aIsMinFilter (OrderDual.toDual f) l a

              Alias of the reverse direction of isMinFilter_dual_iff.

              theorem IsMinFilter.undual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsMinFilter (OrderDual.toDual f) l aIsMaxFilter f l a

              Alias of the forward direction of isMinFilter_dual_iff.

              theorem IsMinFilter.dual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsMinFilter f l aIsMaxFilter (OrderDual.toDual f) l a

              Alias of the reverse direction of isMaxFilter_dual_iff.

              theorem IsMaxFilter.undual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsMaxFilter (OrderDual.toDual f) l aIsMinFilter f l a

              Alias of the forward direction of isMaxFilter_dual_iff.

              theorem IsExtrFilter.undual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsExtrFilter (OrderDual.toDual f) l aIsExtrFilter f l a

              Alias of the forward direction of isExtrFilter_dual_iff.

              theorem IsExtrFilter.dual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} :
              IsExtrFilter f l aIsExtrFilter (OrderDual.toDual f) l a

              Alias of the reverse direction of isExtrFilter_dual_iff.

              theorem isMinOn_dual_iff {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsMinOn (OrderDual.toDual f) s a IsMaxOn f s a
              theorem isMaxOn_dual_iff {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsMaxOn (OrderDual.toDual f) s a IsMinOn f s a
              theorem isExtrOn_dual_iff {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsExtrOn (OrderDual.toDual f) s a IsExtrOn f s a
              theorem IsMaxOn.dual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsMaxOn f s aIsMinOn (OrderDual.toDual f) s a

              Alias of the reverse direction of isMinOn_dual_iff.

              theorem IsMinOn.undual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsMinOn (OrderDual.toDual f) s aIsMaxOn f s a

              Alias of the forward direction of isMinOn_dual_iff.

              theorem IsMaxOn.undual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsMaxOn (OrderDual.toDual f) s aIsMinOn f s a

              Alias of the forward direction of isMaxOn_dual_iff.

              theorem IsMinOn.dual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsMinOn f s aIsMaxOn (OrderDual.toDual f) s a

              Alias of the reverse direction of isMaxOn_dual_iff.

              theorem IsExtrOn.undual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsExtrOn (OrderDual.toDual f) s aIsExtrOn f s a

              Alias of the forward direction of isExtrOn_dual_iff.

              theorem IsExtrOn.dual {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} :
              IsExtrOn f s aIsExtrOn (OrderDual.toDual f) s a

              Alias of the reverse direction of isExtrOn_dual_iff.

              Operations on the filter/set #

              theorem IsMinFilter.filter_mono {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} {l' : Filter α} (h : IsMinFilter f l a) (hl : l' l) :
              theorem IsMaxFilter.filter_mono {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} {l' : Filter α} (h : IsMaxFilter f l a) (hl : l' l) :
              theorem IsExtrFilter.filter_mono {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} {l' : Filter α} (h : IsExtrFilter f l a) (hl : l' l) :
              theorem IsMinFilter.filter_inf {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} (h : IsMinFilter f l a) (l' : Filter α) :
              IsMinFilter f (l l') a
              theorem IsMaxFilter.filter_inf {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} (h : IsMaxFilter f l a) (l' : Filter α) :
              IsMaxFilter f (l l') a
              theorem IsExtrFilter.filter_inf {α : Type u} {β : Type v} [Preorder β] {f : αβ} {l : Filter α} {a : α} (h : IsExtrFilter f l a) (l' : Filter α) :
              IsExtrFilter f (l l') a
              theorem IsMinOn.on_subset {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} {t : Set α} (hf : IsMinOn f t a) (h : s t) :
              IsMinOn f s a
              theorem IsMaxOn.on_subset {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} {t : Set α} (hf : IsMaxOn f t a) (h : s t) :
              IsMaxOn f s a
              theorem IsExtrOn.on_subset {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} {t : Set α} (hf : IsExtrOn f t a) (h : s t) :
              IsExtrOn f s a
              theorem IsMinOn.inter {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsMinOn f s a) (t : Set α) :
              IsMinOn f (s t) a
              theorem IsMaxOn.inter {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) (t : Set α) :
              IsMaxOn f (s t) a
              theorem IsExtrOn.inter {α : Type u} {β : Type v} [Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsExtrOn f s a) (t : Set α) :
              IsExtrOn f (s t) a

              Composition with (anti)monotone functions #

              theorem IsMinFilter.comp_mono {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {l : Filter α} {a : α} (hf : IsMinFilter f l a) {g : βγ} (hg : Monotone g) :
              IsMinFilter (g f) l a
              theorem IsMaxFilter.comp_mono {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {l : Filter α} {a : α} (hf : IsMaxFilter f l a) {g : βγ} (hg : Monotone g) :
              IsMaxFilter (g f) l a
              theorem IsExtrFilter.comp_mono {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {l : Filter α} {a : α} (hf : IsExtrFilter f l a) {g : βγ} (hg : Monotone g) :
              IsExtrFilter (g f) l a
              theorem IsMinFilter.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {l : Filter α} {a : α} (hf : IsMinFilter f l a) {g : βγ} (hg : Antitone g) :
              IsMaxFilter (g f) l a
              theorem IsMaxFilter.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {l : Filter α} {a : α} (hf : IsMaxFilter f l a) {g : βγ} (hg : Antitone g) :
              IsMinFilter (g f) l a
              theorem IsExtrFilter.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {l : Filter α} {a : α} (hf : IsExtrFilter f l a) {g : βγ} (hg : Antitone g) :
              IsExtrFilter (g f) l a
              theorem IsMinOn.comp_mono {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {s : Set α} {a : α} (hf : IsMinOn f s a) {g : βγ} (hg : Monotone g) :
              IsMinOn (g f) s a
              theorem IsMaxOn.comp_mono {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) {g : βγ} (hg : Monotone g) :
              IsMaxOn (g f) s a
              theorem IsExtrOn.comp_mono {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {s : Set α} {a : α} (hf : IsExtrOn f s a) {g : βγ} (hg : Monotone g) :
              IsExtrOn (g f) s a
              theorem IsMinOn.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {s : Set α} {a : α} (hf : IsMinOn f s a) {g : βγ} (hg : Antitone g) :
              IsMaxOn (g f) s a
              theorem IsMaxOn.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) {g : βγ} (hg : Antitone g) :
              IsMinOn (g f) s a
              theorem IsExtrOn.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [Preorder β] [Preorder γ] {f : αβ} {s : Set α} {a : α} (hf : IsExtrOn f s a) {g : βγ} (hg : Antitone g) :
              IsExtrOn (g f) s a
              theorem IsMinFilter.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [Preorder β] [Preorder γ] {f : αβ} {l : Filter α} {a : α} [Preorder δ] {op : βγδ} (hop : ((fun (x1 x2 : β) => x1 x2) (fun (x1 x2 : γ) => x1 x2) fun (x1 x2 : δ) => x1 x2) op op) (hf : IsMinFilter f l a) {g : αγ} (hg : IsMinFilter g l a) :
              IsMinFilter (fun (x : α) => op (f x) (g x)) l a
              theorem IsMaxFilter.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [Preorder β] [Preorder γ] {f : αβ} {l : Filter α} {a : α} [Preorder δ] {op : βγδ} (hop : ((fun (x1 x2 : β) => x1 x2) (fun (x1 x2 : γ) => x1 x2) fun (x1 x2 : δ) => x1 x2) op op) (hf : IsMaxFilter f l a) {g : αγ} (hg : IsMaxFilter g l a) :
              IsMaxFilter (fun (x : α) => op (f x) (g x)) l a
              theorem IsMinOn.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [Preorder β] [Preorder γ] {f : αβ} {s : Set α} {a : α} [Preorder δ] {op : βγδ} (hop : ((fun (x1 x2 : β) => x1 x2) (fun (x1 x2 : γ) => x1 x2) fun (x1 x2 : δ) => x1 x2) op op) (hf : IsMinOn f s a) {g : αγ} (hg : IsMinOn g s a) :
              IsMinOn (fun (x : α) => op (f x) (g x)) s a
              theorem IsMaxOn.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [Preorder β] [Preorder γ] {f : αβ} {s : Set α} {a : α} [Preorder δ] {op : βγδ} (hop : ((fun (x1 x2 : β) => x1 x2) (fun (x1 x2 : γ) => x1 x2) fun (x1 x2 : δ) => x1 x2) op op) (hf : IsMaxOn f s a) {g : αγ} (hg : IsMaxOn g s a) :
              IsMaxOn (fun (x : α) => op (f x) (g x)) s a

              Composition with Tendsto #

              theorem IsMinFilter.comp_tendsto {α : Type u} {β : Type v} {δ : Type x} [Preorder β] {f : αβ} {l : Filter α} {g : δα} {l' : Filter δ} {b : δ} (hf : IsMinFilter f l (g b)) (hg : Filter.Tendsto g l' l) :
              IsMinFilter (f g) l' b
              theorem IsMaxFilter.comp_tendsto {α : Type u} {β : Type v} {δ : Type x} [Preorder β] {f : αβ} {l : Filter α} {g : δα} {l' : Filter δ} {b : δ} (hf : IsMaxFilter f l (g b)) (hg : Filter.Tendsto g l' l) :
              IsMaxFilter (f g) l' b
              theorem IsExtrFilter.comp_tendsto {α : Type u} {β : Type v} {δ : Type x} [Preorder β] {f : αβ} {l : Filter α} {g : δα} {l' : Filter δ} {b : δ} (hf : IsExtrFilter f l (g b)) (hg : Filter.Tendsto g l' l) :
              IsExtrFilter (f g) l' b
              theorem IsMinOn.on_preimage {α : Type u} {β : Type v} {δ : Type x} [Preorder β] {f : αβ} {s : Set α} (g : δα) {b : δ} (hf : IsMinOn f s (g b)) :
              IsMinOn (f g) (g ⁻¹' s) b
              theorem IsMaxOn.on_preimage {α : Type u} {β : Type v} {δ : Type x} [Preorder β] {f : αβ} {s : Set α} (g : δα) {b : δ} (hf : IsMaxOn f s (g b)) :
              IsMaxOn (f g) (g ⁻¹' s) b
              theorem IsExtrOn.on_preimage {α : Type u} {β : Type v} {δ : Type x} [Preorder β] {f : αβ} {s : Set α} (g : δα) {b : δ} (hf : IsExtrOn f s (g b)) :
              IsExtrOn (f g) (g ⁻¹' s) b
              theorem IsMinOn.comp_mapsTo {α : Type u} {β : Type v} {δ : Type x} [Preorder β] {f : αβ} {s : Set α} {a : α} {t : Set δ} {g : δα} {b : δ} (hf : IsMinOn f s a) (hg : Set.MapsTo g t s) (ha : g b = a) :
              IsMinOn (f g) t b
              theorem IsMaxOn.comp_mapsTo {α : Type u} {β : Type v} {δ : Type x} [Preorder β] {f : αβ} {s : Set α} {a : α} {t : Set δ} {g : δα} {b : δ} (hf : IsMaxOn f s a) (hg : Set.MapsTo g t s) (ha : g b = a) :
              IsMaxOn (f g) t b
              theorem IsExtrOn.comp_mapsTo {α : Type u} {β : Type v} {δ : Type x} [Preorder β] {f : αβ} {s : Set α} {a : α} {t : Set δ} {g : δα} {b : δ} (hf : IsExtrOn f s a) (hg : Set.MapsTo g t s) (ha : g b = a) :
              IsExtrOn (f g) t b

              Pointwise addition #

              theorem IsMinFilter.add {α : Type u} {β : Type v} [OrderedAddCommMonoid β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) :
              IsMinFilter (fun (x : α) => f x + g x) l a
              theorem IsMaxFilter.add {α : Type u} {β : Type v} [OrderedAddCommMonoid β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) :
              IsMaxFilter (fun (x : α) => f x + g x) l a
              theorem IsMinOn.add {α : Type u} {β : Type v} [OrderedAddCommMonoid β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMinOn f s a) (hg : IsMinOn g s a) :
              IsMinOn (fun (x : α) => f x + g x) s a
              theorem IsMaxOn.add {α : Type u} {β : Type v} [OrderedAddCommMonoid β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) :
              IsMaxOn (fun (x : α) => f x + g x) s a

              Pointwise negation and subtraction #

              theorem IsMinFilter.neg {α : Type u} {β : Type v} [OrderedAddCommGroup β] {f : αβ} {a : α} {l : Filter α} (hf : IsMinFilter f l a) :
              IsMaxFilter (fun (x : α) => -f x) l a
              theorem IsMaxFilter.neg {α : Type u} {β : Type v} [OrderedAddCommGroup β] {f : αβ} {a : α} {l : Filter α} (hf : IsMaxFilter f l a) :
              IsMinFilter (fun (x : α) => -f x) l a
              theorem IsExtrFilter.neg {α : Type u} {β : Type v} [OrderedAddCommGroup β] {f : αβ} {a : α} {l : Filter α} (hf : IsExtrFilter f l a) :
              IsExtrFilter (fun (x : α) => -f x) l a
              theorem IsMinOn.neg {α : Type u} {β : Type v} [OrderedAddCommGroup β] {f : αβ} {a : α} {s : Set α} (hf : IsMinOn f s a) :
              IsMaxOn (fun (x : α) => -f x) s a
              theorem IsMaxOn.neg {α : Type u} {β : Type v} [OrderedAddCommGroup β] {f : αβ} {a : α} {s : Set α} (hf : IsMaxOn f s a) :
              IsMinOn (fun (x : α) => -f x) s a
              theorem IsExtrOn.neg {α : Type u} {β : Type v} [OrderedAddCommGroup β] {f : αβ} {a : α} {s : Set α} (hf : IsExtrOn f s a) :
              IsExtrOn (fun (x : α) => -f x) s a
              theorem IsMinFilter.sub {α : Type u} {β : Type v} [OrderedAddCommGroup β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMinFilter f l a) (hg : IsMaxFilter g l a) :
              IsMinFilter (fun (x : α) => f x - g x) l a
              theorem IsMaxFilter.sub {α : Type u} {β : Type v} [OrderedAddCommGroup β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMaxFilter f l a) (hg : IsMinFilter g l a) :
              IsMaxFilter (fun (x : α) => f x - g x) l a
              theorem IsMinOn.sub {α : Type u} {β : Type v} [OrderedAddCommGroup β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMinOn f s a) (hg : IsMaxOn g s a) :
              IsMinOn (fun (x : α) => f x - g x) s a
              theorem IsMaxOn.sub {α : Type u} {β : Type v} [OrderedAddCommGroup β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMaxOn f s a) (hg : IsMinOn g s a) :
              IsMaxOn (fun (x : α) => f x - g x) s a

              Pointwise sup/inf #

              theorem IsMinFilter.sup {α : Type u} {β : Type v} [SemilatticeSup β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) :
              IsMinFilter (fun (x : α) => f x g x) l a
              theorem IsMaxFilter.sup {α : Type u} {β : Type v} [SemilatticeSup β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) :
              IsMaxFilter (fun (x : α) => f x g x) l a
              theorem IsMinOn.sup {α : Type u} {β : Type v} [SemilatticeSup β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMinOn f s a) (hg : IsMinOn g s a) :
              IsMinOn (fun (x : α) => f x g x) s a
              theorem IsMaxOn.sup {α : Type u} {β : Type v} [SemilatticeSup β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) :
              IsMaxOn (fun (x : α) => f x g x) s a
              theorem IsMinFilter.inf {α : Type u} {β : Type v} [SemilatticeInf β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) :
              IsMinFilter (fun (x : α) => f x g x) l a
              theorem IsMaxFilter.inf {α : Type u} {β : Type v} [SemilatticeInf β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) :
              IsMaxFilter (fun (x : α) => f x g x) l a
              theorem IsMinOn.inf {α : Type u} {β : Type v} [SemilatticeInf β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMinOn f s a) (hg : IsMinOn g s a) :
              IsMinOn (fun (x : α) => f x g x) s a
              theorem IsMaxOn.inf {α : Type u} {β : Type v} [SemilatticeInf β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) :
              IsMaxOn (fun (x : α) => f x g x) s a

              Pointwise min/max #

              theorem IsMinFilter.min {α : Type u} {β : Type v} [LinearOrder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) :
              IsMinFilter (fun (x : α) => min (f x) (g x)) l a
              theorem IsMaxFilter.min {α : Type u} {β : Type v} [LinearOrder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) :
              IsMaxFilter (fun (x : α) => min (f x) (g x)) l a
              theorem IsMinOn.min {α : Type u} {β : Type v} [LinearOrder β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMinOn f s a) (hg : IsMinOn g s a) :
              IsMinOn (fun (x : α) => min (f x) (g x)) s a
              theorem IsMaxOn.min {α : Type u} {β : Type v} [LinearOrder β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) :
              IsMaxOn (fun (x : α) => min (f x) (g x)) s a
              theorem IsMinFilter.max {α : Type u} {β : Type v} [LinearOrder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) :
              IsMinFilter (fun (x : α) => max (f x) (g x)) l a
              theorem IsMaxFilter.max {α : Type u} {β : Type v} [LinearOrder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) :
              IsMaxFilter (fun (x : α) => max (f x) (g x)) l a
              theorem IsMinOn.max {α : Type u} {β : Type v} [LinearOrder β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMinOn f s a) (hg : IsMinOn g s a) :
              IsMinOn (fun (x : α) => max (f x) (g x)) s a
              theorem IsMaxOn.max {α : Type u} {β : Type v} [LinearOrder β] {f : αβ} {g : αβ} {a : α} {s : Set α} (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) :
              IsMaxOn (fun (x : α) => max (f x) (g x)) s a

              Relation with eventually comparisons of two functions #

              theorem Filter.EventuallyLE.isMaxFilter {α : Type u_1} {β : Type u_2} [Preorder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hle : g ≤ᶠ[l] f) (hfga : f a = g a) (h : IsMaxFilter f l a) :
              theorem IsMaxFilter.congr {α : Type u_1} {β : Type u_2} [Preorder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (h : IsMaxFilter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) :
              theorem Filter.EventuallyEq.isMaxFilter_iff {α : Type u_1} {β : Type u_2} [Preorder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
              theorem Filter.EventuallyLE.isMinFilter {α : Type u_1} {β : Type u_2} [Preorder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (hle : f ≤ᶠ[l] g) (hfga : f a = g a) (h : IsMinFilter f l a) :
              theorem IsMinFilter.congr {α : Type u_1} {β : Type u_2} [Preorder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (h : IsMinFilter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) :
              theorem Filter.EventuallyEq.isMinFilter_iff {α : Type u_1} {β : Type u_2} [Preorder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
              theorem IsExtrFilter.congr {α : Type u_1} {β : Type u_2} [Preorder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (h : IsExtrFilter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) :
              theorem Filter.EventuallyEq.isExtrFilter_iff {α : Type u_1} {β : Type u_2} [Preorder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :

              isMaxOn/isMinOn imply ciSup/ciInf #

              theorem IsMaxOn.iSup_eq {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] {f : βα} {s : Set β} {x₀ : β} (hx₀ : x₀ s) (h : IsMaxOn f s x₀) :
              ⨆ (x : s), f x = f x₀
              theorem IsMinOn.iInf_eq {α : Type u} {β : Type v} [ConditionallyCompleteLinearOrder α] {f : βα} {s : Set β} {x₀ : β} (hx₀ : x₀ s) (h : IsMinOn f s x₀) :
              ⨅ (x : s), f x = f x₀

              Value of Finset.sup / Finset.inf #

              theorem sup_eq_of_isMaxOn {α : Type u} {β : Type v} [SemilatticeSup β] [OrderBot β] {D : αβ} {s : Finset α} {a : α} (hmem : a s) (hmax : IsMaxOn D (↑s) a) :
              s.sup D = D a
              theorem sup_eq_of_max {α : Type u} {β : Type v} [SemilatticeSup β] [OrderBot β] {D : αβ} {s : Finset α} [Nonempty α] {b : β} (hb : b Set.range D) (hmem : Function.invFun D b s) (hmax : as, D a b) :
              s.sup D = b
              theorem inf_eq_of_isMinOn {α : Type u} {β : Type v} [SemilatticeInf β] [OrderTop β] {D : αβ} {s : Finset α} {a : α} (hmem : a s) (hmax : IsMinOn D (↑s) a) :
              s.inf D = D a
              theorem inf_eq_of_min {α : Type u} {β : Type v} [SemilatticeInf β] [OrderTop β] {D : αβ} {s : Finset α} [Nonempty α] {b : β} (hb : b Set.range D) (hmem : Function.invFun D b s) (hmin : as, b D a) :
              s.inf D = b