# 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.

• isMinFilter f l a means that f a ≤ f x in some l-neighborhood of a;
• isMaxFilter f l a means that f x ≤ f a in some l-neighborhood of a;
• isExtrFilter f l a means isMinFilter f l a or isMaxFilter f l a.

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

## Main statements #

### Change of the filter (set) argument #

• is*Filter.filter_mono : replace the filter with a smaller one;
• is*Filter.filter_inf : replace a filter l with l ⊓ l';
• is*On.on_subset : restrict to a smaller set;
• is*Pn.inter : replace a set s with s ∩ t.

### Composition #

• is**.comp_mono : if x is an extremum for f and g is a monotone function, then x is an extremum for g ∘ f;
• is**.comp_antitone : similarly for the case of antitone g;
• is**.bicomp_mono : if x is an extremum of the same type for f and g and a binary operation op is monotone in both arguments, then x is an extremum of the same type for fun x => op (f x) (g x).
• is*Filter.comp_tendsto : if g x is an extremum for f w.r.t. l' and Tendsto g l l', then x is an extremum for f ∘ g w.r.t. l.
• is*On.on_preimage : if g x is an extremum for f on s, then x is an extremum for f ∘ g on g ⁻¹' s.

### Algebraic operations #

• is**.add : if x is an extremum of the same type for two functions, then it is an extremum of the same type for their sum;
• is**.neg : if x is an extremum for f, then it is an extremum of the opposite type for -f;
• is**.sub : if x is a minimum for f and a maximum for g, then it is a minimum for f - g and a maximum for g - f;
• is**.max, is**.min, is**.sup, is**.inf : similarly for is**.add for pointwise max, min, sup, inf, respectively.

### Miscellaneous definitions #

• is**_const : any point is both a minimum and maximum for a constant function;
• isMin/Max*.isExt : any minimum/maximum point is an extremum;
• is**.dual, is**.undual: conversion between codomains α and dual α;

## Missing features (TODO) #

• Multiplication and division;
• is**.bicompl : if x is a minimum for f, y is a minimum for g, and op is a monotone binary operation, then (x, y) is a minimum for uncurry (bicompl op f g). From this point of view, is**.bicomp is a composition
• It would be nice to have a tactic that specializes comp_(anti)mono or bicomp_mono based on a proof of monotonicity of a given (binary) function. The tactic should maintain a meta list of known (anti)monotone (binary) functions with their names, as well as a list of special types of filters, and define the missing lemmas once one of these two lists grows.

### Definitions #

def IsMinFilter {α : Type u} {β : Type v} [] (f : αβ) (l : ) (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} [] (f : αβ) (l : ) (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} [] (f : αβ) (l : ) (a : α) :

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

Equations
Instances For
def IsMinOn {α : Type u} {β : Type v} [] (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} [] (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} [] (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} [] {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} [] {f : αβ} {s : Set α} {a : α} :
IsMinOn f s a xs, f a f x
theorem isMaxOn_iff {α : Type u} {β : Type v} [] {f : αβ} {s : Set α} {a : α} :
IsMaxOn f s a xs, f x f a
theorem isMinOn_univ_iff {α : Type u} {β : Type v} [] {f : αβ} {a : α} :
IsMinOn f Set.univ a ∀ (x : α), f a f x
theorem isMaxOn_univ_iff {α : Type u} {β : Type v} [] {f : αβ} {a : α} :
IsMaxOn f Set.univ a ∀ (x : α), f x f a
theorem IsMinFilter.tendsto_principal_Ici {α : Type u} {β : Type v} [] {f : αβ} {l : } {a : α} (h : IsMinFilter f l a) :
theorem IsMaxFilter.tendsto_principal_Iic {α : Type u} {β : Type v} [] {f : αβ} {l : } {a : α} (h : IsMaxFilter f l a) :

### Conversion to IsExtr*#

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

### Constant function #

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

### Order dual #

theorem isMinFilter_dual_iff {α : Type u} {β : Type v} [] {f : αβ} {l : } {a : α} :
IsMinFilter (OrderDual.toDual f) l a IsMaxFilter f l a
theorem isMaxFilter_dual_iff {α : Type u} {β : Type v} [] {f : αβ} {l : } {a : α} :
IsMaxFilter (OrderDual.toDual f) l a IsMinFilter f l a
theorem isExtrFilter_dual_iff {α : Type u} {β : Type v} [] {f : αβ} {l : } {a : α} :
IsExtrFilter (OrderDual.toDual f) l a IsExtrFilter f l a
theorem IsMaxFilter.dual {α : Type u} {β : Type v} [] {f : αβ} {l : } {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} [] {f : αβ} {l : } {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} [] {f : αβ} {l : } {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} [] {f : αβ} {l : } {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} [] {f : αβ} {l : } {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} [] {f : αβ} {l : } {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} [] {f : αβ} {s : Set α} {a : α} :
IsMinOn (OrderDual.toDual f) s a IsMaxOn f s a
theorem isMaxOn_dual_iff {α : Type u} {β : Type v} [] {f : αβ} {s : Set α} {a : α} :
IsMaxOn (OrderDual.toDual f) s a IsMinOn f s a
theorem isExtrOn_dual_iff {α : Type u} {β : Type v} [] {f : αβ} {s : Set α} {a : α} :
IsExtrOn (OrderDual.toDual f) s a IsExtrOn f s a
theorem IsMaxOn.dual {α : Type u} {β : Type v} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {f : αβ} {l : } {a : α} {l' : } (h : IsMinFilter f l a) (hl : l' l) :
theorem IsMaxFilter.filter_mono {α : Type u} {β : Type v} [] {f : αβ} {l : } {a : α} {l' : } (h : IsMaxFilter f l a) (hl : l' l) :
theorem IsExtrFilter.filter_mono {α : Type u} {β : Type v} [] {f : αβ} {l : } {a : α} {l' : } (h : IsExtrFilter f l a) (hl : l' l) :
theorem IsMinFilter.filter_inf {α : Type u} {β : Type v} [] {f : αβ} {l : } {a : α} (h : IsMinFilter f l a) (l' : ) :
IsMinFilter f (l l') a
theorem IsMaxFilter.filter_inf {α : Type u} {β : Type v} [] {f : αβ} {l : } {a : α} (h : IsMaxFilter f l a) (l' : ) :
IsMaxFilter f (l l') a
theorem IsExtrFilter.filter_inf {α : Type u} {β : Type v} [] {f : αβ} {l : } {a : α} (h : IsExtrFilter f l a) (l' : ) :
IsExtrFilter f (l l') a
theorem IsMinOn.on_subset {α : Type u} {β : Type v} [] {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} [] {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} [] {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} [] {f : αβ} {s : Set α} {a : α} (hf : IsMinOn f s a) (t : Set α) :
IsMinOn f (s t) a
theorem IsMaxOn.inter {α : Type u} {β : Type v} [] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) (t : Set α) :
IsMaxOn f (s t) a
theorem IsExtrOn.inter {α : Type u} {β : Type v} [] {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} [] [] {f : αβ} {l : } {a : α} (hf : IsMinFilter f l a) {g : βγ} (hg : ) :
IsMinFilter (g f) l a
theorem IsMaxFilter.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {l : } {a : α} (hf : IsMaxFilter f l a) {g : βγ} (hg : ) :
IsMaxFilter (g f) l a
theorem IsExtrFilter.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {l : } {a : α} (hf : IsExtrFilter f l a) {g : βγ} (hg : ) :
IsExtrFilter (g f) l a
theorem IsMinFilter.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {l : } {a : α} (hf : IsMinFilter f l a) {g : βγ} (hg : ) :
IsMaxFilter (g f) l a
theorem IsMaxFilter.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {l : } {a : α} (hf : IsMaxFilter f l a) {g : βγ} (hg : ) :
IsMinFilter (g f) l a
theorem IsExtrFilter.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {l : } {a : α} (hf : IsExtrFilter f l a) {g : βγ} (hg : ) :
IsExtrFilter (g f) l a
theorem IsMinOn.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsMinOn f s a) {g : βγ} (hg : ) :
IsMinOn (g f) s a
theorem IsMaxOn.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) {g : βγ} (hg : ) :
IsMaxOn (g f) s a
theorem IsExtrOn.comp_mono {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsExtrOn f s a) {g : βγ} (hg : ) :
IsExtrOn (g f) s a
theorem IsMinOn.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsMinOn f s a) {g : βγ} (hg : ) :
IsMaxOn (g f) s a
theorem IsMaxOn.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) {g : βγ} (hg : ) :
IsMinOn (g f) s a
theorem IsExtrOn.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [] [] {f : αβ} {s : Set α} {a : α} (hf : IsExtrOn f s a) {g : βγ} (hg : ) :
IsExtrOn (g f) s a
theorem IsMinFilter.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [] [] {f : αβ} {l : } {a : α} [] {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} [] [] {f : αβ} {l : } {a : α} [] {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} [] [] {f : αβ} {s : Set α} {a : α} [] {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} [] [] {f : αβ} {s : Set α} {a : α} [] {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} [] {f : αβ} {l : } {g : δα} {l' : } {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} [] {f : αβ} {l : } {g : δα} {l' : } {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} [] {f : αβ} {l : } {g : δα} {l' : } {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} [] {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} [] {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} [] {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} [] {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} [] {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} [] {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

theorem IsMinFilter.add {α : Type u} {β : Type v} {f : αβ} {g : αβ} {a : α} {l : } (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} {f : αβ} {g : αβ} {a : α} {l : } (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} {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} {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} {f : αβ} {a : α} {l : } (hf : IsMinFilter f l a) :
IsMaxFilter (fun (x : α) => -f x) l a
theorem IsMaxFilter.neg {α : Type u} {β : Type v} {f : αβ} {a : α} {l : } (hf : IsMaxFilter f l a) :
IsMinFilter (fun (x : α) => -f x) l a
theorem IsExtrFilter.neg {α : Type u} {β : Type v} {f : αβ} {a : α} {l : } (hf : IsExtrFilter f l a) :
IsExtrFilter (fun (x : α) => -f x) l a
theorem IsMinOn.neg {α : Type u} {β : Type v} {f : αβ} {a : α} {s : Set α} (hf : IsMinOn f s a) :
IsMaxOn (fun (x : α) => -f x) s a
theorem IsMaxOn.neg {α : Type u} {β : Type v} {f : αβ} {a : α} {s : Set α} (hf : IsMaxOn f s a) :
IsMinOn (fun (x : α) => -f x) s a
theorem IsExtrOn.neg {α : Type u} {β : Type v} {f : αβ} {a : α} {s : Set α} (hf : IsExtrOn f s a) :
IsExtrOn (fun (x : α) => -f x) s a
theorem IsMinFilter.sub {α : Type u} {β : Type v} {f : αβ} {g : αβ} {a : α} {l : } (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} {f : αβ} {g : αβ} {a : α} {l : } (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} {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} {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} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {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} [] {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} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {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} [] {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} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {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} [] {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} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {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} [] {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} [] {f : αβ} {g : αβ} {a : α} {l : } (hle : g ≤ᶠ[l] f) (hfga : f a = g a) (h : IsMaxFilter f l a) :
theorem IsMaxFilter.congr {α : Type u_1} {β : Type u_2} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {f : αβ} {g : αβ} {a : α} {l : } (heq : f =ᶠ[l] g) (hfga : f a = g a) :
theorem Filter.EventuallyLE.isMinFilter {α : Type u_1} {β : Type u_2} [] {f : αβ} {g : αβ} {a : α} {l : } (hle : f ≤ᶠ[l] g) (hfga : f a = g a) (h : IsMinFilter f l a) :
theorem IsMinFilter.congr {α : Type u_1} {β : Type u_2} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {f : αβ} {g : αβ} {a : α} {l : } (heq : f =ᶠ[l] g) (hfga : f a = g a) :
theorem IsExtrFilter.congr {α : Type u_1} {β : Type u_2} [] {f : αβ} {g : αβ} {a : α} {l : } (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} [] {f : αβ} {g : αβ} {a : α} {l : } (heq : f =ᶠ[l] g) (hfga : f a = g a) :

### isMaxOn/isMinOn imply ciSup/ciInf#

theorem IsMaxOn.iSup_eq {α : Type u} {β : Type v} {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} {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} [] [] {D : αβ} {s : } {a : α} (hmem : a s) (hmax : IsMaxOn D (↑s) a) :
s.sup D = D a
theorem sup_eq_of_max {α : Type u} {β : Type v} [] [] {D : αβ} {s : } [] {b : β} (hb : b ) (hmem : s) (hmax : as, D a b) :
s.sup D = b
theorem inf_eq_of_isMinOn {α : Type u} {β : Type v} [] [] {D : αβ} {s : } {a : α} (hmem : a s) (hmax : IsMinOn D (↑s) a) :
s.inf D = D a
theorem inf_eq_of_min {α : Type u} {β : Type v} [] [] {D : αβ} {s : } [] {b : β} (hb : b ) (hmem : s) (hmin : as, b D a) :
s.inf D = b