mathlib documentation

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 is_A_B, 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 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
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
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
theorem is_extr_on.elim {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} {p : Prop} :
is_extr_on f s a(is_min_on f s a → p)(is_max_on f s a → p) → p
theorem is_min_on_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
is_min_on f s a ∀ (x : α), x sf a f x
theorem is_max_on_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
is_max_on f s a ∀ (x : α), x sf x f a
theorem is_min_on_univ_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {a : α} :
is_min_on f set.univ a ∀ (x : α), f a f x
theorem is_max_on_univ_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {a : α} :
is_max_on f set.univ a ∀ (x : α), f x f a
theorem is_min_filter.tendsto_principal_Ici {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} (h : is_min_filter f l a) :
theorem is_max_filter.tendsto_principal_Iic {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} (h : is_max_filter f l a) :

Conversion to is_extr_* #

theorem is_min_filter.is_extr {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} :
theorem is_max_filter.is_extr {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} :
theorem is_min_on.is_extr {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} (h : is_min_on f s a) :
theorem is_max_on.is_extr {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} (h : is_max_on f 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 : α} :
theorem is_max_filter_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} :
theorem is_extr_filter_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} :
theorem is_min_filter.undual {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {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 : α} :

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 : α} :

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 : α} :

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 : α} :

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 : α} :

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 : α} :
theorem is_max_on_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
theorem is_extr_on_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
theorem is_min_on.undual {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {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 : α} :

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 : α} :

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 : α} :

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 : α} :

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 : α} :

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 : is_min_filter f l a) (hl : l' l) :
theorem is_max_filter.filter_mono {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} {l' : filter α} (h : is_max_filter f l a) (hl : l' l) :
theorem is_extr_filter.filter_mono {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} {l' : filter α} (h : is_extr_filter f l a) (hl : l' l) :
theorem is_min_filter.filter_inf {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} (h : is_min_filter f l a) (l' : filter α) :
is_min_filter f (l l') a
theorem is_max_filter.filter_inf {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} (h : is_max_filter f l a) (l' : filter α) :
is_max_filter f (l l') a
theorem is_extr_filter.filter_inf {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} (h : is_extr_filter f l a) (l' : filter α) :
is_extr_filter f (l l') a
theorem is_min_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} {t : set α} (hf : is_min_on f t a) (h : s t) :
is_min_on f s a
theorem is_max_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} {t : set α} (hf : is_max_on f t a) (h : s t) :
is_max_on f s a
theorem is_extr_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} {t : set α} (hf : is_extr_on f t a) (h : s t) :
theorem is_min_on.inter {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} (hf : is_min_on f s a) (t : set α) :
is_min_on f (s t) a
theorem is_max_on.inter {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} (hf : is_max_on f s a) (t : set α) :
is_max_on f (s t) a
theorem is_extr_on.inter {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} (hf : is_extr_on f s a) (t : set α) :
is_extr_on f (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 : is_min_filter f l 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 : is_max_filter f l 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 : is_extr_filter f l a) {g : β → γ} (hg : monotone g) :
theorem is_min_filter.comp_antitone {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {l : filter α} {a : α} (hf : is_min_filter f l 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 : is_max_filter f l 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 : is_extr_filter f l a) {g : β → γ} (hg : antitone g) :
theorem is_min_on.comp_mono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : is_min_on f 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 : is_max_on f 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 : is_extr_on f 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 : is_min_on f 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 : is_max_on f 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 : is_extr_on f 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 : (has_le.le has_le.le has_le.le) op op) (hf : is_min_filter f l a) {g : α → γ} (hg : is_min_filter g l 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 : (has_le.le has_le.le has_le.le) op op) (hf : is_max_filter f l a) {g : α → γ} (hg : is_max_filter g l 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 : (has_le.le has_le.le has_le.le) op op) (hf : is_min_on f s a) {g : α → γ} (hg : is_min_on g 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 : (has_le.le has_le.le has_le.le) op op) (hf : is_max_on f s a) {g : α → γ} (hg : is_max_on g 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 : is_min_filter f l (g b)) (hg : filter.tendsto g 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 : is_max_filter f l (g b)) (hg : filter.tendsto g 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 : is_extr_filter f l (g b)) (hg : filter.tendsto g 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 : is_min_on f 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 : is_max_on f 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 : is_extr_on f 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 : is_min_on f s a) (hg : set.maps_to g 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 : is_max_on f s a) (hg : set.maps_to g 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 : is_extr_on f s a) (hg : set.maps_to g t s) (ha : g b = a) :
is_extr_on (f g) t b

Pointwise addition #

theorem is_min_filter.add {α : Type u} {β : Type v} [ordered_add_comm_monoid β] {f g : α → β} {a : α} {l : filter α} (hf : is_min_filter f l a) (hg : is_min_filter g l a) :
is_min_filter (λ (x : α), f x + g x) l a
theorem is_max_filter.add {α : Type u} {β : Type v} [ordered_add_comm_monoid β] {f g : α → β} {a : α} {l : filter α} (hf : is_max_filter f l a) (hg : is_max_filter g l a) :
is_max_filter (λ (x : α), f x + g x) l a
theorem is_min_on.add {α : Type u} {β : Type v} [ordered_add_comm_monoid β] {f g : α → β} {a : α} {s : set α} (hf : is_min_on f s a) (hg : is_min_on g s a) :
is_min_on (λ (x : α), f x + g x) s a
theorem is_max_on.add {α : Type u} {β : Type v} [ordered_add_comm_monoid β] {f g : α → β} {a : α} {s : set α} (hf : is_max_on f s a) (hg : is_max_on g 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} [ordered_add_comm_group β] {f : α → β} {a : α} {l : filter α} (hf : is_min_filter f l a) :
is_max_filter (λ (x : α), -f x) l a
theorem is_max_filter.neg {α : Type u} {β : Type v} [ordered_add_comm_group β] {f : α → β} {a : α} {l : filter α} (hf : is_max_filter f l a) :
is_min_filter (λ (x : α), -f x) l a
theorem is_extr_filter.neg {α : Type u} {β : Type v} [ordered_add_comm_group β] {f : α → β} {a : α} {l : filter α} (hf : is_extr_filter f l a) :
is_extr_filter (λ (x : α), -f x) l a
theorem is_min_on.neg {α : Type u} {β : Type v} [ordered_add_comm_group β] {f : α → β} {a : α} {s : set α} (hf : is_min_on f s a) :
is_max_on (λ (x : α), -f x) s a
theorem is_max_on.neg {α : Type u} {β : Type v} [ordered_add_comm_group β] {f : α → β} {a : α} {s : set α} (hf : is_max_on f s a) :
is_min_on (λ (x : α), -f x) s a
theorem is_extr_on.neg {α : Type u} {β : Type v} [ordered_add_comm_group β] {f : α → β} {a : α} {s : set α} (hf : is_extr_on f s a) :
is_extr_on (λ (x : α), -f x) s a
theorem is_min_filter.sub {α : Type u} {β : Type v} [ordered_add_comm_group β] {f g : α → β} {a : α} {l : filter α} (hf : is_min_filter f l a) (hg : is_max_filter g l a) :
is_min_filter (λ (x : α), f x - g x) l a
theorem is_max_filter.sub {α : Type u} {β : Type v} [ordered_add_comm_group β] {f g : α → β} {a : α} {l : filter α} (hf : is_max_filter f l a) (hg : is_min_filter g l a) :
is_max_filter (λ (x : α), f x - g x) l a
theorem is_min_on.sub {α : Type u} {β : Type v} [ordered_add_comm_group β] {f g : α → β} {a : α} {s : set α} (hf : is_min_on f s a) (hg : is_max_on g s a) :
is_min_on (λ (x : α), f x - g x) s a
theorem is_max_on.sub {α : Type u} {β : Type v} [ordered_add_comm_group β] {f g : α → β} {a : α} {s : set α} (hf : is_max_on f s a) (hg : is_min_on g s a) :
is_max_on (λ (x : α), f x - g x) s a

Pointwise sup/inf #

theorem is_min_filter.sup {α : Type u} {β : Type v} [semilattice_sup β] {f g : α → β} {a : α} {l : filter α} (hf : is_min_filter f l a) (hg : is_min_filter g l a) :
is_min_filter (λ (x : α), f x g x) l a
theorem is_max_filter.sup {α : Type u} {β : Type v} [semilattice_sup β] {f g : α → β} {a : α} {l : filter α} (hf : is_max_filter f l a) (hg : is_max_filter g l a) :
is_max_filter (λ (x : α), f x g x) l a
theorem is_min_on.sup {α : Type u} {β : Type v} [semilattice_sup β] {f g : α → β} {a : α} {s : set α} (hf : is_min_on f s a) (hg : is_min_on g s a) :
is_min_on (λ (x : α), f x g x) s a
theorem is_max_on.sup {α : Type u} {β : Type v} [semilattice_sup β] {f g : α → β} {a : α} {s : set α} (hf : is_max_on f s a) (hg : is_max_on g s a) :
is_max_on (λ (x : α), f x g x) s a
theorem is_min_filter.inf {α : Type u} {β : Type v} [semilattice_inf β] {f g : α → β} {a : α} {l : filter α} (hf : is_min_filter f l a) (hg : is_min_filter g l a) :
is_min_filter (λ (x : α), f x g x) l a
theorem is_max_filter.inf {α : Type u} {β : Type v} [semilattice_inf β] {f g : α → β} {a : α} {l : filter α} (hf : is_max_filter f l a) (hg : is_max_filter g l a) :
is_max_filter (λ (x : α), f x g x) l a
theorem is_min_on.inf {α : Type u} {β : Type v} [semilattice_inf β] {f g : α → β} {a : α} {s : set α} (hf : is_min_on f s a) (hg : is_min_on g s a) :
is_min_on (λ (x : α), f x g x) s a
theorem is_max_on.inf {α : Type u} {β : Type v} [semilattice_inf β] {f g : α → β} {a : α} {s : set α} (hf : is_max_on f s a) (hg : is_max_on g 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 : is_min_filter f l a) (hg : is_min_filter g l 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 : is_max_filter f l a) (hg : is_max_filter g l 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 : is_min_on f s a) (hg : is_min_on g 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 : is_max_on f s a) (hg : is_max_on g 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 : is_min_filter f l a) (hg : is_min_filter g l 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 : is_max_filter f l a) (hg : is_max_filter g l 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 : is_min_on f s a) (hg : is_min_on g 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 : is_max_on f s a) (hg : is_max_on g 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 : is_max_filter f l a) :
theorem is_max_filter.congr {α : Type u_1} {β : Type u_2} [preorder β] {f g : α → β} {a : α} {l : filter α} (h : is_max_filter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g 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) :
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 : is_min_filter f l a) :
theorem is_min_filter.congr {α : Type u_1} {β : Type u_2} [preorder β] {f g : α → β} {a : α} {l : filter α} (h : is_min_filter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g 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) :
theorem is_extr_filter.congr {α : Type u_1} {β : Type u_2} [preorder β] {f g : α → β} {a : α} {l : filter α} (h : is_extr_filter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g 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) :

is_max_on/is_min_on imply csupr/cinfi #

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