Minimum and maximum w.r.t. a filter and on a aet #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
is_min_filter f l ameans thatf a ≤ f xin somel-neighborhood ofa;is_max_filter f l ameans thatf x ≤ f ain somel-neighborhood ofa;is_extr_filter f l ameansis_min_filter f l aoris_max_filter f l a.
Similar predicates with _on suffix are particular cases for l = 𝓟 s.
Main statements #
Change of the filter (set) argument #
is_*_filter.filter_mono: replace the filter with a smaller one;is_*_filter.filter_inf: replace a filterlwithl ⊓ l';is_*_on.on_subset: restrict to a smaller set;is_*_on.inter: replace a setswtihs ∩ t.
Composition #
is_*_*.comp_mono: ifxis an extremum forfandgis a monotone function, thenxis an extremum forg ∘ f;is_*_*.comp_antitone: similarly for the case of antitoneg;is_*_*.bicomp_mono: ifxis an extremum of the same type forfandgand a binary operationopis monotone in both arguments, thenxis an extremum of the same type forλ x, op (f x) (g x).is_*_filter.comp_tendsto: ifg xis an extremum forfw.r.t.l'andtendsto g l l', thenxis an extremum forf ∘ gw.r.t.l.is_*_on.on_preimage: ifg xis an extremum forfons, thenxis an extremum forf ∘ gong ⁻¹' s.
Algebraic operations #
is_*_*.add: ifxis an extremum of the same type for two functions, then it is an extremum of the same type for their sum;is_*_*.neg: ifxis an extremum forf, then it is an extremum of the opposite type for-f;is_*_*.sub: ifxis an a minimum forfand a maximum forg, then it is a minimum forf - gand a maximum forg - f;is_*_*.max,is_*_*.min,is_*_*.sup,is_*_*.inf: similarly foris_*_*.addfor pointwisemax,min,sup,inf, respectively.
Miscellaneous definitions #
is_*_*_const: any point is both a minimum and maximum for a constant function;is_min/max_*.is_ext: any minimum/maximum point is an extremum;is_*_*.dual,is_*_*.undual: conversion between codomainsαanddual α;
Missing features (TODO) #
- Multiplication and division;
is_*_*.bicompl: ifxis a minimum forf,yis a minimum forg, andopis a monotone binary operation, then(x, y)is a minimum foruncurry (bicompl op f g). From this point of view,is_*_*.bicompis a composition- It would be nice to have a tactic that specializes
comp_(anti)monoorbicomp_monobased on a proof of monotonicity of a given (binary) function. The tactic should maintain ametalist 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 #
is_min_filter f l a means that f a ≤ f x in some l-neighborhood of a
is_max_filter f l a means that f x ≤ f a in some l-neighborhood of a
is_extr_filter f l a means is_min_filter f l a or is_max_filter f l a
Equations
- is_extr_filter f l a = (is_min_filter f l a ∨ is_max_filter f l a)
is_extr_on f s a means is_min_on f s a or is_max_on f s a
Equations
- is_extr_on f s a = is_extr_filter f (filter.principal s) a
theorem
is_min_filter.tendsto_principal_Ici
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α}
(h : is_min_filter f l a) :
filter.tendsto f l (filter.principal (set.Ici (f a)))
theorem
is_max_filter.tendsto_principal_Iic
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α}
(h : is_max_filter f l a) :
filter.tendsto f l (filter.principal (set.Iic (f a)))
Conversion to is_extr_* #
theorem
is_min_filter.is_extr
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α} :
is_min_filter f l a → is_extr_filter f l a
theorem
is_max_filter.is_extr
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α} :
is_max_filter f l a → is_extr_filter f l a
theorem
is_min_on.is_extr
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(h : is_min_on f s a) :
is_extr_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) :
is_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_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 : α} :
is_min_filter (⇑order_dual.to_dual ∘ f) l a ↔ is_max_filter f l a
theorem
is_max_filter_dual_iff
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α} :
is_max_filter (⇑order_dual.to_dual ∘ f) l a ↔ is_min_filter f l a
theorem
is_extr_filter_dual_iff
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α} :
is_extr_filter (⇑order_dual.to_dual ∘ f) l a ↔ is_extr_filter f l a
theorem
is_min_filter.undual
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α} :
is_min_filter (⇑order_dual.to_dual ∘ f) l a → is_max_filter f l 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 : α} :
is_max_filter f l a → is_min_filter (⇑order_dual.to_dual ∘ f) l 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 : α} :
is_max_filter (⇑order_dual.to_dual ∘ f) l a → is_min_filter f l 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 : α} :
is_min_filter f l a → is_max_filter (⇑order_dual.to_dual ∘ f) l 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 : α} :
is_extr_filter (⇑order_dual.to_dual ∘ f) l a → is_extr_filter f l 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 : α} :
is_extr_filter f l a → is_extr_filter (⇑order_dual.to_dual ∘ f) l a
Alias of the reverse direction of is_extr_filter_dual_iff.
theorem
is_extr_on_dual_iff
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{s : set α}
{a : α} :
is_extr_on (⇑order_dual.to_dual ∘ f) s a ↔ is_extr_on f s a
Alias of the forward direction of is_min_on_dual_iff.
Alias of the reverse direction of is_min_on_dual_iff.
Alias of the forward direction of is_max_on_dual_iff.
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 : α} :
is_extr_on f s a → is_extr_on (⇑order_dual.to_dual ∘ f) s 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 : α} :
is_extr_on (⇑order_dual.to_dual ∘ f) s a → is_extr_on f s 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) :
is_min_filter f l' a
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) :
is_max_filter f l' a
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) :
is_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_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) :
is_extr_on f s 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) :
is_extr_filter (g ∘ f) l a
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) :
is_extr_filter (g ∘ f) l 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_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_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_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
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) :
theorem
is_max_on.neg
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f : α → β}
{a : α}
{s : set α}
(hf : is_max_on f 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
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_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
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) :
is_max_filter g 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) :
is_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 α}
(heq : f =ᶠ[l] g)
(hfga : f 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 α}
(hle : f ≤ᶠ[l] g)
(hfga : f a = g a)
(h : is_min_filter f l a) :
is_min_filter g 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) :
is_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 α}
(heq : f =ᶠ[l] g)
(hfga : f 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 α}
(h : is_extr_filter f l a)
(heq : f =ᶠ[l] g)
(hfga : f a = g a) :
is_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 α}
(heq : f =ᶠ[l] g)
(hfga : f a = g a) :
is_extr_filter f l a ↔ is_extr_filter g l a