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} [Preorder β] (f : α → β) (l : Filter α) (a : α) : Prop

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

Equations

• IsMinFilter f l a = ∀ᶠ (x : α) in l, f a ≤ f x

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

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

Equations

• IsMaxFilter f l a = ∀ᶠ (x : α) in l, f x ≤ f a

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

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

Equations

• IsExtrFilter f l a = (IsMinFilter f l a ∨ IsMaxFilter f l a)

def IsMinOn {α : Type u} {β : Type v} [Preorder β] (f : α → β) (s : Set α) (a : α) : Prop

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

Equations

• IsMinOn f s a = IsMinFilter f (Filter.principal s) a

def IsMaxOn {α : Type u} {β : Type v} [Preorder β] (f : α → β) (s : Set α) (a : α) : Prop

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

Equations

• IsMaxOn f s a = IsMaxFilter f (Filter.principal s) a

def IsExtrOn {α : Type u} {β : Type v} [Preorder β] (f : α → β) (s : Set α) (a : α) : Prop

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

Equations

• IsExtrOn f s a = IsExtrFilter f (Filter.principal s) a

theorem IsExtrOn.elim {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} {p : Prop} : IsExtrOn f s a → (IsMinOn f s a → p) → (IsMaxOn f s a → p) → p

theorem isMinOn_iff {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} : IsMinOn f s a ↔ ∀ x ∈ s, f a ≤ f x

theorem isMaxOn_iff {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} : IsMaxOn f s a ↔ ∀ x ∈ s, 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) : Filter.Tendsto f l (Filter.principal (Set.Ici (f a)))

theorem IsMaxFilter.tendsto_principal_Iic {α : Type u} {β : Type v} [Preorder β] {f : α → β} {l : Filter α} {a : α} (h : IsMaxFilter f l a) : Filter.Tendsto f l (Filter.principal (Set.Iic (f a)))

Conversion to IsExtr*

theorem IsMinFilter.isExtr {α : Type u} {β : Type v} [Preorder β] {f : α → β} {l : Filter α} {a : α} : IsMinFilter f l a → IsExtrFilter f l a

theorem IsMaxFilter.isExtr {α : Type u} {β : Type v} [Preorder β] {f : α → β} {l : Filter α} {a : α} : IsMaxFilter f l a → IsExtrFilter 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 a → IsMinFilter (⇑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 a → IsMaxFilter 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 a → IsMaxFilter (⇑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 a → IsMinFilter 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 a → IsExtrFilter 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 a → IsExtrFilter (⇑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 a → IsMinOn (⇑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 a → IsMaxOn 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 a → IsMinOn 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 a → IsMaxOn (⇑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 a → IsExtrOn 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 a → IsExtrOn (⇑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) : IsMinFilter f l' a

theorem IsMaxFilter.filter_mono {α : Type u} {β : Type v} [Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α} (h : IsMaxFilter f l a) (hl : l' ≤ l) : IsMaxFilter f l' a

theorem IsExtrFilter.filter_mono {α : Type u} {β : Type v} [Preorder β] {f : α → β} {l : Filter α} {a : α} {l' : Filter α} (h : IsExtrFilter f l a) (hl : l' ≤ l) : IsExtrFilter f l' a

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 : Relator.LiftFun (fun (x1 x2 : β) => x1 ≤ x2) (Relator.LiftFun (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 : Relator.LiftFun (fun (x1 x2 : β) => x1 ≤ x2) (Relator.LiftFun (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 : Relator.LiftFun (fun (x1 x2 : β) => x1 ≤ x2) (Relator.LiftFun (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 : Relator.LiftFun (fun (x1 x2 : β) => x1 ≤ x2) (Relator.LiftFun (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} [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] {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} [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] {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} [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] {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} [AddCommMonoid β] [PartialOrder β] [IsOrderedAddMonoid β] {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} [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α} {l : Filter α} (hf : IsMinFilter f l a) : IsMaxFilter (fun (x : α) => -f x) l a

theorem IsMaxFilter.neg {α : Type u} {β : Type v} [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α} {l : Filter α} (hf : IsMaxFilter f l a) : IsMinFilter (fun (x : α) => -f x) l a

theorem IsExtrFilter.neg {α : Type u} {β : Type v} [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α} {l : Filter α} (hf : IsExtrFilter f l a) : IsExtrFilter (fun (x : α) => -f x) l a

theorem IsMinOn.neg {α : Type u} {β : Type v} [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α} {s : Set α} (hf : IsMinOn f s a) : IsMaxOn (fun (x : α) => -f x) s a

theorem IsMaxOn.neg {α : Type u} {β : Type v} [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α} {s : Set α} (hf : IsMaxOn f s a) : IsMinOn (fun (x : α) => -f x) s a

theorem IsExtrOn.neg {α : Type u} {β : Type v} [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α} {s : Set α} (hf : IsExtrOn f s a) : IsExtrOn (fun (x : α) => -f x) s a

theorem IsMinFilter.sub {α : Type u} {β : Type v} [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {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} [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {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} [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {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} [AddCommGroup β] [PartialOrder β] [IsOrderedAddMonoid β] {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.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.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.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.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.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.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.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.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) : IsMaxFilter g 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) : IsMaxFilter g l 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) : IsMaxFilter f l a ↔ IsMaxFilter g l 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) : IsMinFilter g 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) : IsMinFilter g l 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) : IsMinFilter f l a ↔ IsMinFilter g l 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) : IsExtrFilter g l 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) : IsExtrFilter f l a ↔ IsExtrFilter g l 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 : ∀ a ∈ s, 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 : ∀ a ∈ s, b ≤ D a) : s.inf D = b