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

We list here the statements for Extr; analogous statements exist for the min and max predicates. For statements without an Extr variant we list the min variant.

Change of the filter (set) argument

• IsExtrFilter.filter_mono: replace the filter with a smaller one;
• IsExtrFilter.filter_inf: replace a filter l with l ⊓ l';
• IsExtrOn.of_subset: restrict to a smaller set;
• IsExtrOn.inter: replace a set s with s ∩ t.

Composition

• IsExtrFilter.comp_mono, IsExtrOn.comp_mono: if x is an extremum for f and g is a monotone function, then x is an extremum for g ∘ f.
• IsExtrFilter.comp_antitone, IsExtrOn.comp_antitone: similarly for the case of antitone g.
• IsMinFilter.bicomp_mono, IsMinOn.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).
• IsExtrFilter.comp_of_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.
• IsExtrOn.preimage: if g x is an extremum for f on s, then x is an extremum for f ∘ g on g ⁻¹' s.

Algebraic operations

• IsMinFilter.add, IsMinOn.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.
• IsExtrFilter.neg, IsExtrOn.neg: if x is an extremum for f, then it is an extremum of the opposite type for -f.
• IsMinFilter.sub, IsMinOn.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.
• IsMinOn.max, IsMinOn.min, IsMinOn.sup, IsMinOn.inf: similarly for IsMinOn.add for pointwise max, min, sup, inf, respectively. These also have Filter variants.

Miscellaneous definitions

• isExtrFilter_const, isExtrOn_const: any point is an extremum for a constant function.
• IsMinFilter.isExtrFilter, IsMinOn.isExtrOn: any minimum/maximum point is an extremum.
• IsExtrFilter.undual, IsExtrFilter.dual, IsExtrOn.undual, IsExtrOn.dual: convert between codomains α and αᵒᵈ.

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_mono/comp_antitone/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

IsMaxFilter 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 IsMinOn.bddBelow {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} (h : IsMinOn f s a) : BddBelow (f '' s)

theorem IsMinOn.isGLB {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} (ha : a ∈ s) (hfsa : IsMinOn f s a) : IsGLB {x : β | ∃ x_1 ∈ s, f x_1 = x} (f a)

theorem IsMaxOn.isLUB {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} (ha : a ∈ s) (hfsa : IsMaxOn f s a) : IsLUB {x : β | ∃ x_1 ∈ s, f x_1 = x} (f a)

theorem IsMaxOn.bddAbove {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} (h : IsMaxOn f s a) : BddAbove (f '' s)

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.isExtrFilter {α : Type u} {β : Type v} [Preorder β] {f : α → β} {l : Filter α} {a : α} (h : IsMinFilter f l a) : IsExtrFilter f l a

@[deprecated IsMinFilter.isExtrFilter (since := "2026-07-17")]

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

Alias of IsMinFilter.isExtrFilter.

theorem IsMaxFilter.isExtrFilter {α : Type u} {β : Type v} [Preorder β] {f : α → β} {l : Filter α} {a : α} (h : IsMaxFilter f l a) : IsExtrFilter f l a

@[deprecated IsMaxFilter.isExtrFilter (since := "2026-07-17")]

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

Alias of IsMaxFilter.isExtrFilter.

theorem IsMinOn.isExtrOn {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} (h : IsMinOn f s a) : IsExtrOn f s a

@[deprecated IsMinOn.isExtrOn (since := "2026-07-17")]

theorem IsMinOn.isExtr {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} (h : IsMinOn f s a) : IsExtrOn f s a

Alias of IsMinOn.isExtrOn.

theorem IsMaxOn.isExtrOn {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} (h : IsMaxOn f s a) : IsExtrOn f s a

@[deprecated IsMaxOn.isExtrOn (since := "2026-07-17")]

theorem IsMaxOn.isExtr {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} (h : IsMaxOn f s a) : IsExtrOn f s a

Alias of IsMaxOn.isExtrOn.

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

theorem eventuallyEq_of_isMinFilter_of_isMaxFilter {α : Type u} {l : Filter α} {a : α} {β : Type u_1} [PartialOrder β] {f : α → β} (h₁ : IsMinFilter f l a) (h₂ : IsMaxFilter f l a) : f =ᶠ[l] fun (x : α) => f a

If f has a minimum and a maximum both given by f a along the filter l, then it is eventually equal to f a along the filter.

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

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.

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.of_subset {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α} (hf : IsMinOn f t a) (h : s ⊆ t) : IsMinOn f s a

@[deprecated IsMinOn.of_subset (since := "2026-07-17")]

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

Alias of IsMinOn.of_subset.

theorem IsMaxOn.of_subset {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α} (hf : IsMaxOn f t a) (h : s ⊆ t) : IsMaxOn f s a

@[deprecated IsMaxOn.of_subset (since := "2026-07-17")]

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

Alias of IsMaxOn.of_subset.

theorem IsExtrOn.of_subset {α : Type u} {β : Type v} [Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set α} (hf : IsExtrOn f t a) (h : s ⊆ t) : IsExtrOn f s a

@[deprecated IsExtrOn.of_subset (since := "2026-07-17")]

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

Alias of IsExtrOn.of_subset.

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_of_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

@[deprecated IsMinFilter.comp_of_tendsto (since := "2026-07-17")]

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

Alias of IsMinFilter.comp_of_tendsto.

theorem IsMaxFilter.comp_of_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

@[deprecated IsMaxFilter.comp_of_tendsto (since := "2026-07-17")]

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

Alias of IsMaxFilter.comp_of_tendsto.

theorem IsExtrFilter.comp_of_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

@[deprecated IsExtrFilter.comp_of_tendsto (since := "2026-07-17")]

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

Alias of IsExtrFilter.comp_of_tendsto.

theorem IsMinOn.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

@[deprecated IsMinOn.preimage (since := "2026-07-17")]

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

Alias of IsMinOn.preimage.

theorem IsMaxOn.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

@[deprecated IsMaxOn.preimage (since := "2026-07-17")]

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

Alias of IsMaxOn.preimage.

theorem IsExtrOn.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

@[deprecated IsExtrOn.preimage (since := "2026-07-17")]

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

Alias of IsExtrOn.preimage.

theorem IsMinOn.comp_of_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

@[deprecated IsMinOn.comp_of_mapsTo (since := "2026-07-17")]

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

Alias of IsMinOn.comp_of_mapsTo.

theorem IsMaxOn.comp_of_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

@[deprecated IsMaxOn.comp_of_mapsTo (since := "2026-07-17")]

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

Alias of IsMaxOn.comp_of_mapsTo.

theorem IsExtrOn.comp_of_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

@[deprecated IsExtrOn.comp_of_mapsTo (since := "2026-07-17")]

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

Alias of IsExtrOn.comp_of_mapsTo.

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

Extrema from monotonicity and antitonicity

theorem isMaxOn_Ioo_of_mono_anti {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : MonotoneOn f (Set.Ioc a b)) (h₁ : AntitoneOn f (Set.Ico b c)) : IsMaxOn f (Set.Ioo a c) b

If f is monotone on Ioc a b and antitone on Ico b c, then the maximum of f on Ioo a c is attained at b.

theorem isMinOn_Ioo_of_anti_mono {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : AntitoneOn f (Set.Ioc a b)) (h₁ : MonotoneOn f (Set.Ico b c)) : IsMinOn f (Set.Ioo a c) b

If f is antitone on Ioc a b and monotone on Ico b c, then the minimum of f on Ioo a c is attained at b.

theorem isMaxOn_Ico_of_mono_anti {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : MonotoneOn f (Set.Icc a b)) (h₁ : AntitoneOn f (Set.Ico b c)) : IsMaxOn f (Set.Ico a c) b

If f is monotone on Icc a b and antitone on Ico b c, then the maximum of f on Ico a c is attained at b.

theorem isMinOn_Ico_of_anti_mono {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : AntitoneOn f (Set.Icc a b)) (h₁ : MonotoneOn f (Set.Ico b c)) : IsMinOn f (Set.Ico a c) b

If f is antitone on Icc a b and monotone on Ico b c, then the minimum of f on Ico a c is attained at b.

theorem isMaxOn_Ioc_of_mono_anti {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : MonotoneOn f (Set.Ioc a b)) (h₁ : AntitoneOn f (Set.Icc b c)) : IsMaxOn f (Set.Ioc a c) b

If f is monotone on Ioc a b and antitone on Icc b c, then the maximum of f on Ioc a c is attained at b.

theorem isMinOn_Ioc_of_anti_mono {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : AntitoneOn f (Set.Ioc a b)) (h₁ : MonotoneOn f (Set.Icc b c)) : IsMinOn f (Set.Ioc a c) b

If f is antitone on Ioc a b and monotone on Icc b c, then the minimum of f on Ioc a c is attained at b.

theorem isMaxOn_Icc_of_mono_anti {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : MonotoneOn f (Set.Icc a b)) (h₁ : AntitoneOn f (Set.Icc b c)) : IsMaxOn f (Set.Icc a c) b

If f is monotone on Icc a b and antitone on Icc b c, then the maximum of f on Icc a c is attained at b.

theorem isMinOn_Icc_of_anti_mono {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b c : α} {f : α → β} (h₀ : AntitoneOn f (Set.Icc a b)) (h₁ : MonotoneOn f (Set.Icc b c)) : IsMinOn f (Set.Icc a c) b

If f is antitone on Icc a b and monotone on Icc b c, then the minimum of f on Icc a c is attained at b.

theorem isMaxOn_Ioi_of_mono_anti {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : MonotoneOn f (Set.Ioc a b)) (h₁ : AntitoneOn f (Set.Ici b)) : IsMaxOn f (Set.Ioi a) b

If f is monotone on Ioc a b and antitone on Ici b, then the maximum of f on Ioi a is attained at b.

theorem isMinOn_Ioi_of_anti_mono {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : AntitoneOn f (Set.Ioc a b)) (h₁ : MonotoneOn f (Set.Ici b)) : IsMinOn f (Set.Ioi a) b

If f is antitone on Ioc a b and monotone on Ici b, then the minimum of f on Ioi a is attained at b.

theorem isMaxOn_Ici_of_mono_anti {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : MonotoneOn f (Set.Icc a b)) (h₁ : AntitoneOn f (Set.Ici b)) : IsMaxOn f (Set.Ici a) b

If f is monotone on Icc a b and antitone on Ici b, then the maximum of f on Ici a is attained at b.

theorem isMinOn_Ici_of_anti_mono {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : AntitoneOn f (Set.Icc a b)) (h₁ : MonotoneOn f (Set.Ici b)) : IsMinOn f (Set.Ici a) b

If f is antitone on Icc a b and monotone on Ici b, then the minimum of f on Ici a is attained at b.

theorem isMaxOn_Iio_of_mono_anti {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : MonotoneOn f (Set.Iic b)) (h₁ : AntitoneOn f (Set.Ico b a)) : IsMaxOn f (Set.Iio a) b

If f is monotone on Iic b and antitone on Ico b a, then the maximum of f on Iio a is attained at b.

theorem isMinOn_Iio_of_anti_mono {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : AntitoneOn f (Set.Iic b)) (h₁ : MonotoneOn f (Set.Ico b a)) : IsMinOn f (Set.Iio a) b

If f is antitone on Iic b and monotone on Ico b a, then the minimum of f on Iio a is attained at b.

theorem isMaxOn_Iic_of_mono_anti {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : MonotoneOn f (Set.Iic b)) (h₁ : AntitoneOn f (Set.Icc b a)) : IsMaxOn f (Set.Iic a) b

If f is monotone on Iic b and antitone on Icc b a, then the maximum of f on Iic a is attained at b.

theorem isMinOn_Iic_of_anti_mono {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {a b : α} {f : α → β} (h₀ : AntitoneOn f (Set.Iic b)) (h₁ : MonotoneOn f (Set.Icc b a)) : IsMinOn f (Set.Iic a) b

If f is antitone on Iic b and monotone on Icc b a, then the minimum of f on Iic a is attained at b.

theorem isMaxOn_univ_of_mono_anti {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {b : α} {f : α → β} (h₀ : MonotoneOn f (Set.Iic b)) (h₁ : AntitoneOn f (Set.Ici b)) : IsMaxOn f Set.univ b

If f is monotone on Iic b and antitone on Ici b, then the maximum of f is attained at b.

theorem isMinOn_univ_of_anti_mono {α : Type u} {β : Type u_1} [LinearOrder α] [Preorder β] {b : α} {f : α → β} (h₀ : AntitoneOn f (Set.Iic b)) (h₁ : MonotoneOn f (Set.Ici b)) : IsMinOn f Set.univ b

If f is antitone on Iic b and monotone on Ici b, then the minimum of f is attained at b.

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