# mathlib3documentation

order.filter.extr

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

## Main Definitions #

This file defines six predicates of the form is_A_B, where A is min, max, or extr, and B is filter or on.

• is_min_filter f l a means that f a ≤ f x in some l-neighborhood of a;
• is_max_filter f l a means that f x ≤ f a in some l-neighborhood of a;
• is_extr_filter f l a means is_min_filter f l a or is_max_filter 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_*_on.inter : replace a set s wtih 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 λ 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 an 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;
• is_min/max_*.is_ext : 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 is_min_filter {α : Type u} {β : Type v} [preorder β] (f : α β) (l : filter α) (a : α) :
Prop

is_min_filter f l a means that f a ≤ f x in some l-neighborhood of a

Equations
def is_max_filter {α : Type u} {β : Type v} [preorder β] (f : α β) (l : filter α) (a : α) :
Prop

is_max_filter f l a means that f x ≤ f a in some l-neighborhood of a

Equations
def is_extr_filter {α : Type u} {β : Type v} [preorder β] (f : α β) (l : filter α) (a : α) :
Prop

is_extr_filter f l a means is_min_filter f l a or is_max_filter f l a

Equations
def is_min_on {α : Type u} {β : Type v} [preorder β] (f : α β) (s : set α) (a : α) :
Prop

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

Equations
• s a = a
def is_max_on {α : Type u} {β : Type v} [preorder β] (f : α β) (s : set α) (a : α) :
Prop

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

Equations
• s a = a
def is_extr_on {α : Type u} {β : Type v} [preorder β] (f : α β) (s : set α) (a : α) :
Prop

is_extr_on f s a means is_min_on f s a or is_max_on f s a

Equations
• s a = a
theorem is_extr_on.elim {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} {p : Prop} :
s a s a p) s a p) p
theorem is_min_on_iff {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
s a (x : α), x s f a f x
theorem is_max_on_iff {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
s a (x : α), x s f x f a
theorem is_min_on_univ_iff {α : Type u} {β : Type v} [preorder β] {f : α β} {a : α} :
(x : α), f a f x
theorem is_max_on_univ_iff {α : Type u} {β : Type v} [preorder β] {f : α β} {a : α} :
(x : α), f x f a
theorem is_min_filter.tendsto_principal_Ici {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} (h : a) :
theorem is_max_filter.tendsto_principal_Iic {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} (h : a) :

### Conversion to is_extr_*#

theorem is_min_filter.is_extr {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a
theorem is_max_filter.is_extr {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a
theorem is_min_on.is_extr {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (h : s a) :
s a
theorem is_max_on.is_extr {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (h : s a) :
s a

### Constant function #

theorem is_min_filter_const {α : Type u} {β : Type v} [preorder β] {l : filter α} {a : α} {b : β} :
is_min_filter (λ (_x : α), b) l a
theorem is_max_filter_const {α : Type u} {β : Type v} [preorder β] {l : filter α} {a : α} {b : β} :
is_max_filter (λ (_x : α), b) l a
theorem is_extr_filter_const {α : Type u} {β : Type v} [preorder β] {l : filter α} {a : α} {b : β} :
is_extr_filter (λ (_x : α), b) l a
theorem is_min_on_const {α : Type u} {β : Type v} [preorder β] {s : set α} {a : α} {b : β} :
is_min_on (λ (_x : α), b) s a
theorem is_max_on_const {α : Type u} {β : Type v} [preorder β] {s : set α} {a : α} {b : β} :
is_max_on (λ (_x : α), b) s a
theorem is_extr_on_const {α : Type u} {β : Type v} [preorder β] {s : set α} {a : α} {b : β} :
is_extr_on (λ (_x : α), b) s a

### Order dual #

theorem is_min_filter_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a
theorem is_max_filter_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a
theorem is_extr_filter_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a
theorem is_min_filter.undual {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a

Alias of the forward direction of is_min_filter_dual_iff.

theorem is_max_filter.dual {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a

Alias of the reverse direction of is_min_filter_dual_iff.

theorem is_max_filter.undual {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a

Alias of the forward direction of is_max_filter_dual_iff.

theorem is_min_filter.dual {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a

Alias of the reverse direction of is_max_filter_dual_iff.

theorem is_extr_filter.undual {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a

Alias of the forward direction of is_extr_filter_dual_iff.

theorem is_extr_filter.dual {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} :
a a

Alias of the reverse direction of is_extr_filter_dual_iff.

theorem is_min_on_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
a s a
theorem is_max_on_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
a s a
theorem is_extr_on_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
a s a
theorem is_min_on.undual {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
a s a

Alias of the forward direction of is_min_on_dual_iff.

theorem is_max_on.dual {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
s a a

Alias of the reverse direction of is_min_on_dual_iff.

theorem is_max_on.undual {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
a s a

Alias of the forward direction of is_max_on_dual_iff.

theorem is_min_on.dual {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
s a a

Alias of the reverse direction of is_max_on_dual_iff.

theorem is_extr_on.dual {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
s a a

Alias of the reverse direction of is_extr_on_dual_iff.

theorem is_extr_on.undual {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} :
a s a

Alias of the forward direction of is_extr_on_dual_iff.

### Operations on the filter/set #

theorem is_min_filter.filter_mono {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} {l' : filter α} (h : a) (hl : l' l) :
l' a
theorem is_max_filter.filter_mono {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} {l' : filter α} (h : a) (hl : l' l) :
l' a
theorem is_extr_filter.filter_mono {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} {l' : filter α} (h : a) (hl : l' l) :
l' a
theorem is_min_filter.filter_inf {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} (h : a) (l' : filter α) :
(l l') a
theorem is_max_filter.filter_inf {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} (h : a) (l' : filter α) :
(l l') a
theorem is_extr_filter.filter_inf {α : Type u} {β : Type v} [preorder β] {f : α β} {l : filter α} {a : α} (h : a) (l' : filter α) :
(l l') a
theorem is_min_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} {t : set α} (hf : t a) (h : s t) :
s a
theorem is_max_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} {t : set α} (hf : t a) (h : s t) :
s a
theorem is_extr_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} {t : set α} (hf : t a) (h : s t) :
s a
theorem is_min_on.inter {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : s a) (t : set α) :
(s t) a
theorem is_max_on.inter {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : s a) (t : set α) :
(s t) a
theorem is_extr_on.inter {α : Type u} {β : Type v} [preorder β] {f : α β} {s : set α} {a : α} (hf : s a) (t : set α) :
(s t) a

### Composition with (anti)monotone functions #

theorem is_min_filter.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {l : filter α} {a : α} (hf : a) {g : β γ} (hg : monotone g) :
is_min_filter (g f) l a
theorem is_max_filter.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {l : filter α} {a : α} (hf : a) {g : β γ} (hg : monotone g) :
is_max_filter (g f) l a
theorem is_extr_filter.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {l : filter α} {a : α} (hf : a) {g : β γ} (hg : monotone g) :
theorem is_min_filter.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {l : filter α} {a : α} (hf : a) {g : β γ} (hg : antitone g) :
is_max_filter (g f) l a
theorem is_max_filter.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {l : filter α} {a : α} (hf : a) {g : β γ} (hg : antitone g) :
is_min_filter (g f) l a
theorem is_extr_filter.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {l : filter α} {a : α} (hf : a) {g : β γ} (hg : antitone g) :
theorem is_min_on.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : s a) {g : β γ} (hg : monotone g) :
is_min_on (g f) s a
theorem is_max_on.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : s a) {g : β γ} (hg : monotone g) :
is_max_on (g f) s a
theorem is_extr_on.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : s a) {g : β γ} (hg : monotone g) :
is_extr_on (g f) s a
theorem is_min_on.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : s a) {g : β γ} (hg : antitone g) :
is_max_on (g f) s a
theorem is_max_on.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : s a) {g : β γ} (hg : antitone g) :
is_min_on (g f) s a
theorem is_extr_on.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} (hf : s a) {g : β γ} (hg : antitone g) :
is_extr_on (g f) s a
theorem is_min_filter.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [preorder β] [preorder γ] {f : α β} {l : filter α} {a : α} [preorder δ] {op : β γ δ} (hop : op op) (hf : a) {g : α γ} (hg : a) :
is_min_filter (λ (x : α), op (f x) (g x)) l a
theorem is_max_filter.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [preorder β] [preorder γ] {f : α β} {l : filter α} {a : α} [preorder δ] {op : β γ δ} (hop : op op) (hf : a) {g : α γ} (hg : a) :
is_max_filter (λ (x : α), op (f x) (g x)) l a
theorem is_min_on.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} [preorder δ] {op : β γ δ} (hop : op op) (hf : s a) {g : α γ} (hg : s a) :
is_min_on (λ (x : α), op (f x) (g x)) s a
theorem is_max_on.bicomp_mono {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [preorder β] [preorder γ] {f : α β} {s : set α} {a : α} [preorder δ] {op : β γ δ} (hop : op op) (hf : s a) {g : α γ} (hg : s a) :
is_max_on (λ (x : α), op (f x) (g x)) s a

### Composition with tendsto#

theorem is_min_filter.comp_tendsto {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {l : filter α} {g : δ α} {l' : filter δ} {b : δ} (hf : (g b)) (hg : l' l) :
is_min_filter (f g) l' b
theorem is_max_filter.comp_tendsto {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {l : filter α} {g : δ α} {l' : filter δ} {b : δ} (hf : (g b)) (hg : l' l) :
is_max_filter (f g) l' b
theorem is_extr_filter.comp_tendsto {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {l : filter α} {g : δ α} {l' : filter δ} {b : δ} (hf : (g b)) (hg : l' l) :
is_extr_filter (f g) l' b
theorem is_min_on.on_preimage {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {s : set α} (g : δ α) {b : δ} (hf : s (g b)) :
is_min_on (f g) (g ⁻¹' s) b
theorem is_max_on.on_preimage {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {s : set α} (g : δ α) {b : δ} (hf : s (g b)) :
is_max_on (f g) (g ⁻¹' s) b
theorem is_extr_on.on_preimage {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {s : set α} (g : δ α) {b : δ} (hf : s (g b)) :
is_extr_on (f g) (g ⁻¹' s) b
theorem is_min_on.comp_maps_to {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {s : set α} {a : α} {t : set δ} {g : δ α} {b : δ} (hf : s a) (hg : t s) (ha : g b = a) :
is_min_on (f g) t b
theorem is_max_on.comp_maps_to {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {s : set α} {a : α} {t : set δ} {g : δ α} {b : δ} (hf : s a) (hg : t s) (ha : g b = a) :
is_max_on (f g) t b
theorem is_extr_on.comp_maps_to {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α β} {s : set α} {a : α} {t : set δ} {g : δ α} {b : δ} (hf : s a) (hg : t s) (ha : g b = a) :
is_extr_on (f g) t b

theorem is_min_filter.add {α : Type u} {β : Type v} {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_min_filter (λ (x : α), f x + g x) l a
theorem is_max_filter.add {α : Type u} {β : Type v} {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_max_filter (λ (x : α), f x + g x) l a
theorem is_min_on.add {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_min_on (λ (x : α), f x + g x) s a
theorem is_max_on.add {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_max_on (λ (x : α), f x + g x) s a

### Pointwise negation and subtraction #

theorem is_min_filter.neg {α : Type u} {β : Type v} {f : α β} {a : α} {l : filter α} (hf : a) :
is_max_filter (λ (x : α), -f x) l a
theorem is_max_filter.neg {α : Type u} {β : Type v} {f : α β} {a : α} {l : filter α} (hf : a) :
is_min_filter (λ (x : α), -f x) l a
theorem is_extr_filter.neg {α : Type u} {β : Type v} {f : α β} {a : α} {l : filter α} (hf : a) :
is_extr_filter (λ (x : α), -f x) l a
theorem is_min_on.neg {α : Type u} {β : Type v} {f : α β} {a : α} {s : set α} (hf : s a) :
is_max_on (λ (x : α), -f x) s a
theorem is_max_on.neg {α : Type u} {β : Type v} {f : α β} {a : α} {s : set α} (hf : s a) :
is_min_on (λ (x : α), -f x) s a
theorem is_extr_on.neg {α : Type u} {β : Type v} {f : α β} {a : α} {s : set α} (hf : s a) :
is_extr_on (λ (x : α), -f x) s a
theorem is_min_filter.sub {α : Type u} {β : Type v} {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_min_filter (λ (x : α), f x - g x) l a
theorem is_max_filter.sub {α : Type u} {β : Type v} {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_max_filter (λ (x : α), f x - g x) l a
theorem is_min_on.sub {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_min_on (λ (x : α), f x - g x) s a
theorem is_max_on.sub {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_max_on (λ (x : α), f x - g x) s a

### Pointwise sup/inf#

theorem is_min_filter.sup {α : Type u} {β : Type v} {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_min_filter (λ (x : α), f x g x) l a
theorem is_max_filter.sup {α : Type u} {β : Type v} {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_max_filter (λ (x : α), f x g x) l a
theorem is_min_on.sup {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_min_on (λ (x : α), f x g x) s a
theorem is_max_on.sup {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_max_on (λ (x : α), f x g x) s a
theorem is_min_filter.inf {α : Type u} {β : Type v} {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_min_filter (λ (x : α), f x g x) l a
theorem is_max_filter.inf {α : Type u} {β : Type v} {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_max_filter (λ (x : α), f x g x) l a
theorem is_min_on.inf {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_min_on (λ (x : α), f x g x) s a
theorem is_max_on.inf {α : Type u} {β : Type v} {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_max_on (λ (x : α), f x g x) s a

### Pointwise min/max#

theorem is_min_filter.min {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_min_filter (λ (x : α), linear_order.min (f x) (g x)) l a
theorem is_max_filter.min {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_max_filter (λ (x : α), linear_order.min (f x) (g x)) l a
theorem is_min_on.min {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_min_on (λ (x : α), linear_order.min (f x) (g x)) s a
theorem is_max_on.min {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_max_on (λ (x : α), linear_order.min (f x) (g x)) s a
theorem is_min_filter.max {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_min_filter (λ (x : α), linear_order.max (f x) (g x)) l a
theorem is_max_filter.max {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {l : filter α} (hf : a) (hg : a) :
is_max_filter (λ (x : α), linear_order.max (f x) (g x)) l a
theorem is_min_on.max {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_min_on (λ (x : α), linear_order.max (f x) (g x)) s a
theorem is_max_on.max {α : Type u} {β : Type v} [linear_order β] {f g : α β} {a : α} {s : set α} (hf : s a) (hg : s a) :
is_max_on (λ (x : α), linear_order.max (f x) (g x)) s a

### Relation with eventually comparisons of two functions #

theorem filter.eventually_le.is_max_filter {α : Type u_1} {β : Type u_2} [preorder β] {f g : α β} {a : α} {l : filter α} (hle : g ≤ᶠ[l] f) (hfga : f a = g a) (h : a) :
a
theorem is_max_filter.congr {α : Type u_1} {β : Type u_2} [preorder β] {f g : α β} {a : α} {l : filter α} (h : a) (heq : f =ᶠ[l] g) (hfga : f a = g a) :
a
theorem filter.eventually_eq.is_max_filter_iff {α : Type u_1} {β : Type u_2} [preorder β] {f g : α β} {a : α} {l : filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
a a
theorem filter.eventually_le.is_min_filter {α : Type u_1} {β : Type u_2} [preorder β] {f g : α β} {a : α} {l : filter α} (hle : f ≤ᶠ[l] g) (hfga : f a = g a) (h : a) :
a
theorem is_min_filter.congr {α : Type u_1} {β : Type u_2} [preorder β] {f g : α β} {a : α} {l : filter α} (h : a) (heq : f =ᶠ[l] g) (hfga : f a = g a) :
a
theorem filter.eventually_eq.is_min_filter_iff {α : Type u_1} {β : Type u_2} [preorder β] {f g : α β} {a : α} {l : filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
a a
theorem is_extr_filter.congr {α : Type u_1} {β : Type u_2} [preorder β] {f g : α β} {a : α} {l : filter α} (h : a) (heq : f =ᶠ[l] g) (hfga : f a = g a) :
a
theorem filter.eventually_eq.is_extr_filter_iff {α : Type u_1} {β : Type u_2} [preorder β] {f g : α β} {a : α} {l : filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
a a

### is_max_on/is_min_on imply csupr/cinfi#

theorem is_max_on.supr_eq {α : Type u} {β : Type v} {f : β α} {s : set β} {x₀ : β} (hx₀ : x₀ s) (h : s x₀) :
( (x : s), f x) = f x₀
theorem is_min_on.infi_eq {α : Type u} {β : Type v} {f : β α} {s : set β} {x₀ : β} (hx₀ : x₀ s) (h : s x₀) :
( (x : s), f x) = f x₀