Documentation

Mathlib.Order.Filter.Extr

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Conversion to IsExtr* #

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

Constant function #

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

Order dual #

theorem isMinFilter_dual_iff {α : Type u} {β : Type v} [inst : Preorder β] {f : αβ} {l : Filter α} {a : α} :
IsMinFilter (OrderDual.toDual f) l a IsMaxFilter f l a
theorem isMaxFilter_dual_iff {α : Type u} {β : Type v} [inst : Preorder β] {f : αβ} {l : Filter α} {a : α} :
IsMaxFilter (OrderDual.toDual f) l a IsMinFilter f l a
theorem isExtrFilter_dual_iff {α : Type u} {β : Type v} [inst : Preorder β] {f : αβ} {l : Filter α} {a : α} :
IsExtrFilter (OrderDual.toDual f) l a IsExtrFilter f l a
theorem IsMaxFilter.dual {α : Type u} {β : Type v} [inst : 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} [inst : Preorder β] {f : αβ} {l : Filter α} {a : α} :
IsMinFilter (OrderDual.toDual f) l aIsMaxFilter f l a

Alias of the forward direction of isMinFilter_dual_iff.

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

Alias of the forward direction of isMaxFilter_dual_iff.

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

Alias of the reverse direction of isMaxFilter_dual_iff.

theorem IsExtrFilter.undual {α : Type u} {β : Type v} [inst : 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} [inst : 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} [inst : Preorder β] {f : αβ} {s : Set α} {a : α} :
IsMinOn (OrderDual.toDual f) s a IsMaxOn f s a
theorem isMaxOn_dual_iff {α : Type u} {β : Type v} [inst : Preorder β] {f : αβ} {s : Set α} {a : α} :
IsMaxOn (OrderDual.toDual f) s a IsMinOn f s a
theorem isExtrOn_dual_iff {α : Type u} {β : Type v} [inst : Preorder β] {f : αβ} {s : Set α} {a : α} :
IsExtrOn (OrderDual.toDual f) s a IsExtrOn f s a
theorem IsMinOn.undual {α : Type u} {β : Type v} [inst : 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.dual {α : Type u} {β : Type v} [inst : Preorder β] {f : αβ} {s : Set α} {a : α} :
IsMaxOn f s aIsMinOn (OrderDual.toDual f) s a

Alias of the reverse direction of isMinOn_dual_iff.

theorem IsMaxOn.undual {α : Type u} {β : Type v} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Preorder β] {f : αβ} {l : Filter α} {a : α} {l' : Filter α} (h : IsMinFilter f l a) (hl : l' l) :
theorem IsMaxFilter.filter_mono {α : Type u} {β : Type v} [inst : Preorder β] {f : αβ} {l : Filter α} {a : α} {l' : Filter α} (h : IsMaxFilter f l a) (hl : l' l) :
theorem IsExtrFilter.filter_mono {α : Type u} {β : Type v} [inst : Preorder β] {f : αβ} {l : Filter α} {a : α} {l' : Filter α} (h : IsExtrFilter f l a) (hl : l' l) :
theorem IsMinFilter.filter_inf {α : Type u} {β : Type v} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsMinOn f s a) (t : Set α) :
IsMinOn f (s t) a
theorem IsMaxOn.inter {α : Type u} {β : Type v} [inst : Preorder β] {f : αβ} {s : Set α} {a : α} (hf : IsMaxOn f s a) (t : Set α) :
IsMaxOn f (s t) a
theorem IsExtrOn.inter {α : Type u} {β : Type v} [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : 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} [inst : Preorder β] [inst : Preorder γ] {f : αβ} {l : Filter α} {a : α} [inst : Preorder δ] {op : βγδ} (hop : ((fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1) op op) (hf : 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} [inst : Preorder β] [inst : Preorder γ] {f : αβ} {l : Filter α} {a : α} [inst : Preorder δ] {op : βγδ} (hop : ((fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1) op op) (hf : 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} [inst : Preorder β] [inst : Preorder γ] {f : αβ} {s : Set α} {a : α} [inst : Preorder δ] {op : βγδ} (hop : ((fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1) op op) (hf : 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} [inst : Preorder β] [inst : Preorder γ] {f : αβ} {s : Set α} {a : α} [inst : Preorder δ] {op : βγδ} (hop : ((fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1) op op) (hf : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : OrderedAddCommGroup β] {f : αβ} {a : α} {l : Filter α} (hf : IsMinFilter f l a) :
IsMaxFilter (fun x => -f x) l a
theorem IsMaxFilter.neg {α : Type u} {β : Type v} [inst : OrderedAddCommGroup β] {f : αβ} {a : α} {l : Filter α} (hf : IsMaxFilter f l a) :
IsMinFilter (fun x => -f x) l a
theorem IsExtrFilter.neg {α : Type u} {β : Type v} [inst : OrderedAddCommGroup β] {f : αβ} {a : α} {l : Filter α} (hf : IsExtrFilter f l a) :
IsExtrFilter (fun x => -f x) l a
theorem IsMinOn.neg {α : Type u} {β : Type v} [inst : OrderedAddCommGroup β] {f : αβ} {a : α} {s : Set α} (hf : IsMinOn f s a) :
IsMaxOn (fun x => -f x) s a
theorem IsMaxOn.neg {α : Type u} {β : Type v} [inst : OrderedAddCommGroup β] {f : αβ} {a : α} {s : Set α} (hf : IsMaxOn f s a) :
IsMinOn (fun x => -f x) s a
theorem IsExtrOn.neg {α : Type u} {β : Type v} [inst : OrderedAddCommGroup β] {f : αβ} {a : α} {s : Set α} (hf : IsExtrOn f s a) :
IsExtrOn (fun x => -f x) s a
theorem IsMinFilter.sub {α : Type u} {β : Type v} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Preorder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
theorem IsExtrFilter.congr {α : Type u_1} {β : Type u_2} [inst : 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} [inst : Preorder β] {f : αβ} {g : αβ} {a : α} {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :

isMaxOn/isMinOn imply csupᵢ/cinfᵢ #

theorem IsMaxOn.supᵢ_eq {α : Type u} {β : Type v} [inst : ConditionallyCompleteLinearOrder α] {f : βα} {s : Set β} {x₀ : β} (hx₀ : x₀ s) (h : IsMaxOn f s x₀) :
(x, f x) = f x₀
theorem IsMinOn.infᵢ_eq {α : Type u} {β : Type v} [inst : ConditionallyCompleteLinearOrder α] {f : βα} {s : Set β} {x₀ : β} (hx₀ : x₀ s) (h : IsMinOn f s x₀) :
(x, f x) = f x₀