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 β] :
(α → β)filter αα → 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 β] :
(α → β)filter αα → 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 β] :
(α → β)filter αα → 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 β] :
(α → β)set αα → 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 β] :
(α → β)set αα → 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 β] :
(α → β)set αα → 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

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 : α} :
is_min_on f s ais_extr_on f s a

theorem is_max_on.is_extr {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
is_max_on f s ais_extr_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_on_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
is_min_on f s a is_max_on f s a

theorem is_max_on_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :
is_max_on f s a is_min_on f s a

theorem is_extr_on_dual_iff {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} :

Operations on the filter/set

theorem is_min_filter.filter_mono {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} {l' : filter α} :
is_min_filter f l al' lis_min_filter f l' a

theorem is_max_filter.filter_mono {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} {l' : filter α} :
is_max_filter f l al' lis_max_filter f l' a

theorem is_extr_filter.filter_mono {α : Type u} {β : Type v} [preorder β] {f : α → β} {l : filter α} {a : α} {l' : filter α} :
is_extr_filter f l al' lis_extr_filter f l' a

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 α} :
is_min_on f t as tis_min_on f s a

theorem is_max_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} {t : set α} :
is_max_on f t as tis_max_on f s a

theorem is_extr_on.on_subset {α : Type u} {β : Type v} [preorder β] {f : α → β} {s : set α} {a : α} {t : set α} :
is_extr_on f t as tis_extr_on f s a

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 : β → γ} :
monotone gis_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 : β → γ} :
monotone gis_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 : β → γ} :
monotone gis_extr_filter (g f) l a

theorem is_min_filter.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {l : filter α} {a : α} (hf : is_min_filter f l a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_max_filter (g f) l a

theorem is_max_filter.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {l : filter α} {a : α} (hf : is_max_filter f l a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_min_filter (g f) l a

theorem is_extr_filter.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {l : filter α} {a : α} (hf : is_extr_filter f l a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_extr_filter (g f) l a

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 : β → γ} :
monotone gis_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 : β → γ} :
monotone gis_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 : β → γ} :
monotone gis_extr_on (g f) s a

theorem is_min_on.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : is_min_on f s a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_max_on (g f) s a

theorem is_max_on.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : is_max_on f s a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)is_min_on (g f) s a

theorem is_extr_on.comp_antimono {α : Type u} {β : Type v} {γ : Type w} [preorder β] [preorder γ] {f : α → β} {s : set α} {a : α} (hf : is_extr_on f s a) {g : β → γ} :
(∀ ⦃x y : β⦄, x yg y g x)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 : α → γ} :
is_min_filter g l ais_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 : α → γ} :
is_max_filter g l ais_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 : α → γ} :
is_min_on g s ais_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 : α → γ} :
is_max_on g s ais_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 : δ} :
is_min_filter f l (g b)filter.tendsto g l' lis_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 : δ} :
is_max_filter f l (g b)filter.tendsto g l' lis_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 : δ} :
is_extr_filter f l (g b)filter.tendsto g l' lis_extr_filter (f g) l' b

theorem is_min_on.on_preimage {α : Type u} {β : Type v} {δ : Type x} [preorder β] {f : α → β} {s : set α} (g : δ → α) {b : δ} :
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 : δ} :
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 : δ} :
is_extr_on f s (g b)is_extr_on (f g) (g ⁻¹' s) b

Pointwise addition

theorem is_min_filter.add {α : Type u} {β : Type v} [ordered_add_comm_monoid β] {f g : α → β} {a : α} {l : filter α} :
is_min_filter f l ais_min_filter g l ais_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 α} :
is_max_filter f l ais_max_filter g l ais_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 α} :
is_min_on f s ais_min_on g s ais_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 α} :
is_max_on f s ais_max_on g s ais_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 α} :
is_min_filter f l ais_max_filter (λ (x : α), -f x) l a

theorem is_max_filter.neg {α : Type u} {β : Type v} [ordered_add_comm_group β] {f : α → β} {a : α} {l : filter α} :
is_max_filter f l ais_min_filter (λ (x : α), -f x) l a

theorem is_extr_filter.neg {α : Type u} {β : Type v} [ordered_add_comm_group β] {f : α → β} {a : α} {l : filter α} :
is_extr_filter f l ais_extr_filter (λ (x : α), -f x) l a

theorem is_min_on.neg {α : Type u} {β : Type v} [ordered_add_comm_group β] {f : α → β} {a : α} {s : set α} :
is_min_on f s ais_max_on (λ (x : α), -f x) s a

theorem is_max_on.neg {α : Type u} {β : Type v} [ordered_add_comm_group β] {f : α → β} {a : α} {s : set α} :
is_max_on f s ais_min_on (λ (x : α), -f x) s a

theorem is_extr_on.neg {α : Type u} {β : Type v} [ordered_add_comm_group β] {f : α → β} {a : α} {s : set α} :
is_extr_on f s ais_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 α} :
is_min_filter f l ais_max_filter g l ais_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 α} :
is_max_filter f l ais_min_filter g l ais_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 α} :
is_min_on f s ais_max_on g s ais_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 α} :
is_max_on f s ais_min_on g s ais_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 α} :
is_min_filter f l ais_min_filter g l ais_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 α} :
is_max_filter f l ais_max_filter g l ais_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 α} :
is_min_on f s ais_min_on g s ais_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 α} :
is_max_on f s ais_max_on g s ais_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 α} :
is_min_filter f l ais_min_filter g l ais_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 α} :
is_max_filter f l ais_max_filter g l ais_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 α} :
is_min_on f s ais_min_on g s ais_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 α} :
is_max_on f s ais_max_on g s ais_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 α} :
is_min_filter f l ais_min_filter g l ais_min_filter (λ (x : α), min (f x) (g x)) l a

theorem is_max_filter.min {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {l : filter α} :
is_max_filter f l ais_max_filter g l ais_max_filter (λ (x : α), min (f x) (g x)) l a

theorem is_min_on.min {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {s : set α} :
is_min_on f s ais_min_on g s ais_min_on (λ (x : α), min (f x) (g x)) s a

theorem is_max_on.min {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {s : set α} :
is_max_on f s ais_max_on g s ais_max_on (λ (x : α), min (f x) (g x)) s a

theorem is_min_filter.max {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {l : filter α} :
is_min_filter f l ais_min_filter g l ais_min_filter (λ (x : α), max (f x) (g x)) l a

theorem is_max_filter.max {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {l : filter α} :
is_max_filter f l ais_max_filter g l ais_max_filter (λ (x : α), max (f x) (g x)) l a

theorem is_min_on.max {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {s : set α} :
is_min_on f s ais_min_on g s ais_min_on (λ (x : α), max (f x) (g x)) s a

theorem is_max_on.max {α : Type u} {β : Type v} [linear_order β] {f g : α → β} {a : α} {s : set α} :
is_max_on f s ais_max_on g s ais_max_on (λ (x : α), 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 α} :
g ≤ᶠ[l] ff a = g ais_max_filter f l ais_max_filter g l a

theorem is_max_filter.congr {α : Type u_1} {β : Type u_2} [preorder β] {f g : α → β} {a : α} {l : filter α} :
is_max_filter f l af =ᶠ[l] gf a = g ais_max_filter g l a

theorem filter.eventually_eq.is_max_filter_iff {α : Type u_1} {β : Type u_2} [preorder β] {f g : α → β} {a : α} {l : filter α} :
f =ᶠ[l] gf a = g a(is_max_filter f l a is_max_filter g l a)

theorem filter.eventually_le.is_min_filter {α : Type u_1} {β : Type u_2} [preorder β] {f g : α → β} {a : α} {l : filter α} :
f ≤ᶠ[l] gf a = g ais_min_filter f l ais_min_filter g l a

theorem is_min_filter.congr {α : Type u_1} {β : Type u_2} [preorder β] {f g : α → β} {a : α} {l : filter α} :
is_min_filter f l af =ᶠ[l] gf a = g ais_min_filter g l a

theorem filter.eventually_eq.is_min_filter_iff {α : Type u_1} {β : Type u_2} [preorder β] {f g : α → β} {a : α} {l : filter α} :
f =ᶠ[l] gf a = g a(is_min_filter f l a is_min_filter g l a)

theorem is_extr_filter.congr {α : Type u_1} {β : Type u_2} [preorder β] {f g : α → β} {a : α} {l : filter α} :
is_extr_filter f l af =ᶠ[l] gf a = g ais_extr_filter g l a

theorem filter.eventually_eq.is_extr_filter_iff {α : Type u_1} {β : Type u_2} [preorder β] {f g : α → β} {a : α} {l : filter α} :
f =ᶠ[l] gf a = g a(is_extr_filter f l a is_extr_filter g l a)