Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: rename Filter.EventuallyLe #2464

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - chore: rename Filter.EventuallyLe #2464

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2302a1c
chore: rename Filter.EventuallyLe
Ruben-VandeVelde Feb 23, 2023
446e428
Merge branch 'master' into eventuallyle
Ruben-VandeVelde Feb 28, 2023
4fdab91
More
Ruben-VandeVelde Feb 28, 2023
10c0168
Merge remote-tracking branch 'origin/master' into eventuallyle
Ruben-VandeVelde Mar 2, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
102 changes: 51 additions & 51 deletions Mathlib/Order/Filter/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1620,22 +1620,22 @@ section LE
variable [LE β] {l : Filter α}

/-- A function `f` is eventually less than or equal to a function `g` at a filter `l`. -/
def EventuallyLe (l : Filter α) (f g : α → β) : Prop :=
def EventuallyLE (l : Filter α) (f g : α → β) : Prop :=
∀ᶠ x in l, f x ≤ g x
#align filter.eventually_le Filter.EventuallyLe
#align filter.eventually_le Filter.EventuallyLE

@[inherit_doc]
notation:50 f " ≤ᶠ[" l:50 "] " g:50 => EventuallyLe l f g
notation:50 f " ≤ᶠ[" l:50 "] " g:50 => EventuallyLE l f g

theorem EventuallyLe.congr {f f' g g' : α → β} (H : f ≤ᶠ[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
theorem EventuallyLE.congr {f f' g g' : α → β} (H : f ≤ᶠ[l] g) (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
f' ≤ᶠ[l] g' :=
H.mp <| hg.mp <| hf.mono fun x hf hg H => by rwa [hf, hg] at H
#align filter.eventually_le.congr Filter.EventuallyLe.congr
#align filter.eventually_le.congr Filter.EventuallyLE.congr

theorem eventuallyLe_congr {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
theorem eventuallyLE_congr {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
f ≤ᶠ[l] g ↔ f' ≤ᶠ[l] g' :=
⟨fun H => H.congr hf hg, fun H => H.congr hf.symm hg.symm⟩
#align filter.eventually_le_congr Filter.eventuallyLe_congr
#align filter.eventually_le_congr Filter.eventuallyLE_congr

end LE

Expand All @@ -1648,45 +1648,45 @@ theorem EventuallyEq.le (h : f =ᶠ[l] g) : f ≤ᶠ[l] g :=
#align filter.eventually_eq.le Filter.EventuallyEq.le

@[refl]
theorem EventuallyLe.refl (l : Filter α) (f : α → β) : f ≤ᶠ[l] f :=
theorem EventuallyLE.refl (l : Filter α) (f : α → β) : f ≤ᶠ[l] f :=
EventuallyEq.rfl.le
#align filter.eventually_le.refl Filter.EventuallyLe.refl
#align filter.eventually_le.refl Filter.EventuallyLE.refl

theorem EventuallyLe.rfl : f ≤ᶠ[l] f :=
EventuallyLe.refl l f
#align filter.eventually_le.rfl Filter.EventuallyLe.rfl
theorem EventuallyLE.rfl : f ≤ᶠ[l] f :=
EventuallyLE.refl l f
#align filter.eventually_le.rfl Filter.EventuallyLE.rfl

@[trans]
theorem EventuallyLe.trans (H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h :=
theorem EventuallyLE.trans (H₁ : f ≤ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h :=
H₂.mp <| H₁.mono fun _ => le_trans
#align filter.eventually_le.trans Filter.EventuallyLe.trans
#align filter.eventually_le.trans Filter.EventuallyLE.trans

@[trans]
theorem EventuallyEq.trans_le (H₁ : f =ᶠ[l] g) (H₂ : g ≤ᶠ[l] h) : f ≤ᶠ[l] h :=
H₁.le.trans H₂
#align filter.eventually_eq.trans_le Filter.EventuallyEq.trans_le

@[trans]
theorem EventuallyLe.trans_eq (H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) : f ≤ᶠ[l] h :=
theorem EventuallyLE.trans_eq (H₁ : f ≤ᶠ[l] g) (H₂ : g =ᶠ[l] h) : f ≤ᶠ[l] h :=
H₁.trans H₂.le
#align filter.eventually_le.trans_eq Filter.EventuallyLe.trans_eq
#align filter.eventually_le.trans_eq Filter.EventuallyLE.trans_eq

end Preorder

theorem EventuallyLe.antisymm [PartialOrder β] {l : Filter α} {f g : α → β} (h₁ : f ≤ᶠ[l] g)
theorem EventuallyLE.antisymm [PartialOrder β] {l : Filter α} {f g : α → β} (h₁ : f ≤ᶠ[l] g)
(h₂ : g ≤ᶠ[l] f) : f =ᶠ[l] g :=
h₂.mp <| h₁.mono fun _ => le_antisymm
#align filter.eventually_le.antisymm Filter.EventuallyLe.antisymm
#align filter.eventually_le.antisymm Filter.EventuallyLE.antisymm

theorem eventuallyLe_antisymm_iff [PartialOrder β] {l : Filter α} {f g : α → β} :
theorem eventuallyLE_antisymm_iff [PartialOrder β] {l : Filter α} {f g : α → β} :
f =ᶠ[l] g ↔ f ≤ᶠ[l] g ∧ g ≤ᶠ[l] f := by
simp only [EventuallyEq, EventuallyLe, le_antisymm_iff, eventually_and]
#align filter.eventually_le_antisymm_iff Filter.eventuallyLe_antisymm_iff
simp only [EventuallyEq, EventuallyLE, le_antisymm_iff, eventually_and]
#align filter.eventually_le_antisymm_iff Filter.eventuallyLE_antisymm_iff

theorem EventuallyLe.le_iff_eq [PartialOrder β] {l : Filter α} {f g : α → β} (h : f ≤ᶠ[l] g) :
theorem EventuallyLE.le_iff_eq [PartialOrder β] {l : Filter α} {f g : α → β} (h : f ≤ᶠ[l] g) :
g ≤ᶠ[l] f ↔ g =ᶠ[l] f :=
⟨fun h' => h'.antisymm h, EventuallyEq.le⟩
#align filter.eventually_le.le_iff_eq Filter.EventuallyLe.le_iff_eq
#align filter.eventually_le.le_iff_eq Filter.EventuallyLE.le_iff_eq

theorem Eventually.ne_of_lt [Preorder β] {l : Filter α} {f g : α → β} (h : ∀ᶠ x in l, f x < g x) :
∀ᶠ x in l, f x ≠ g x :=
Expand All @@ -1709,71 +1709,71 @@ theorem Eventually.lt_top_iff_ne_top [PartialOrder β] [OrderTop β] {l : Filter
#align filter.eventually.lt_top_iff_ne_top Filter.Eventually.lt_top_iff_ne_top

@[mono]
theorem EventuallyLe.inter {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
theorem EventuallyLE.inter {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
(s ∩ s' : Set α) ≤ᶠ[l] (t ∩ t' : Set α) :=
h'.mp <| h.mono fun _ => And.imp
#align filter.eventually_le.inter Filter.EventuallyLe.inter
#align filter.eventually_le.inter Filter.EventuallyLE.inter

@[mono]
theorem EventuallyLe.union {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
theorem EventuallyLE.union {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : s' ≤ᶠ[l] t') :
(s ∪ s' : Set α) ≤ᶠ[l] (t ∪ t' : Set α) :=
h'.mp <| h.mono fun _ => Or.imp
#align filter.eventually_le.union Filter.EventuallyLe.union
#align filter.eventually_le.union Filter.EventuallyLE.union

@[mono]
theorem EventuallyLe.compl {s t : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) :
theorem EventuallyLE.compl {s t : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) :
(tᶜ : Set α) ≤ᶠ[l] (sᶜ : Set α) :=
h.mono fun _ => mt
#align filter.eventually_le.compl Filter.EventuallyLe.compl
#align filter.eventually_le.compl Filter.EventuallyLE.compl

@[mono]
theorem EventuallyLe.diff {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : t' ≤ᶠ[l] s') :
theorem EventuallyLE.diff {s t s' t' : Set α} {l : Filter α} (h : s ≤ᶠ[l] t) (h' : t' ≤ᶠ[l] s') :
(s \ s' : Set α) ≤ᶠ[l] (t \ t' : Set α) :=
h.inter h'.compl
#align filter.eventually_le.diff Filter.EventuallyLe.diff
#align filter.eventually_le.diff Filter.EventuallyLE.diff

theorem EventuallyLe.mul_le_mul [MulZeroClass β] [PartialOrder β] [PosMulMono β] [MulPosMono β]
theorem EventuallyLE.mul_le_mul [MulZeroClass β] [PartialOrder β] [PosMulMono β] [MulPosMono β]
{l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) (hg₀ : 0 ≤ᶠ[l] g₁)
(hf₀ : 0 ≤ᶠ[l] f₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂ := by
filter_upwards [hf, hg, hg₀, hf₀] with x using _root_.mul_le_mul
#align filter.eventually_le.mul_le_mul Filter.EventuallyLe.mul_le_mul
#align filter.eventually_le.mul_le_mul Filter.EventuallyLE.mul_le_mul

@[to_additive EventuallyLe.add_le_add]
theorem EventuallyLe.mul_le_mul' [Mul β] [Preorder β] [CovariantClass β β (· * ·) (· ≤ ·)]
@[to_additive EventuallyLE.add_le_add]
theorem EventuallyLE.mul_le_mul' [Mul β] [Preorder β] [CovariantClass β β (· * ·) (· ≤ ·)]
[CovariantClass β β (swap (· * ·)) (· ≤ ·)] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β}
(hf : f₁ ≤ᶠ[l] f₂) (hg : g₁ ≤ᶠ[l] g₂) : f₁ * g₁ ≤ᶠ[l] f₂ * g₂ := by
filter_upwards [hf, hg] with x hfx hgx using _root_.mul_le_mul' hfx hgx
#align filter.eventually_le.mul_le_mul' Filter.EventuallyLe.mul_le_mul'
#align filter.eventually_le.add_le_add Filter.EventuallyLe.add_le_add
#align filter.eventually_le.mul_le_mul' Filter.EventuallyLE.mul_le_mul'
#align filter.eventually_le.add_le_add Filter.EventuallyLE.add_le_add

theorem EventuallyLe.mul_nonneg [OrderedSemiring β] {l : Filter α} {f g : α → β} (hf : 0 ≤ᶠ[l] f)
theorem EventuallyLE.mul_nonneg [OrderedSemiring β] {l : Filter α} {f g : α → β} (hf : 0 ≤ᶠ[l] f)
(hg : 0 ≤ᶠ[l] g) : 0 ≤ᶠ[l] f * g := by filter_upwards [hf, hg] with x using _root_.mul_nonneg
#align filter.eventually_le.mul_nonneg Filter.EventuallyLe.mul_nonneg
#align filter.eventually_le.mul_nonneg Filter.EventuallyLE.mul_nonneg

theorem eventually_sub_nonneg [OrderedRing β] {l : Filter α} {f g : α → β} :
0 ≤ᶠ[l] g - f ↔ f ≤ᶠ[l] g :=
eventually_congr <| eventually_of_forall fun _ => sub_nonneg
#align filter.eventually_sub_nonneg Filter.eventually_sub_nonneg

theorem EventuallyLe.sup [SemilatticeSup β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂)
theorem EventuallyLE.sup [SemilatticeSup β] {l : Filter α} {f₁ f₂ g₁ g₂ : α → β} (hf : f₁ ≤ᶠ[l] f₂)
(hg : g₁ ≤ᶠ[l] g₂) : f₁ ⊔ g₁ ≤ᶠ[l] f₂ ⊔ g₂ := by
filter_upwards [hf, hg] with x hfx hgx using sup_le_sup hfx hgx
#align filter.eventually_le.sup Filter.EventuallyLe.sup
#align filter.eventually_le.sup Filter.EventuallyLE.sup

theorem EventuallyLe.sup_le [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : f ≤ᶠ[l] h)
theorem EventuallyLE.sup_le [SemilatticeSup β] {l : Filter α} {f g h : α → β} (hf : f ≤ᶠ[l] h)
(hg : g ≤ᶠ[l] h) : f ⊔ g ≤ᶠ[l] h := by
filter_upwards [hf, hg] with x hfx hgx using _root_.sup_le hfx hgx
#align filter.eventually_le.sup_le Filter.EventuallyLe.sup_le
#align filter.eventually_le.sup_le Filter.EventuallyLE.sup_le

theorem EventuallyLe.le_sup_of_le_left [SemilatticeSup β] {l : Filter α} {f g h : α → β}
theorem EventuallyLE.le_sup_of_le_left [SemilatticeSup β] {l : Filter α} {f g h : α → β}
(hf : h ≤ᶠ[l] f) : h ≤ᶠ[l] f ⊔ g :=
hf.mono fun _ => _root_.le_sup_of_le_left
#align filter.eventually_le.le_sup_of_le_left Filter.EventuallyLe.le_sup_of_le_left
#align filter.eventually_le.le_sup_of_le_left Filter.EventuallyLE.le_sup_of_le_left

theorem EventuallyLe.le_sup_of_le_right [SemilatticeSup β] {l : Filter α} {f g h : α → β}
theorem EventuallyLE.le_sup_of_le_right [SemilatticeSup β] {l : Filter α} {f g h : α → β}
(hg : h ≤ᶠ[l] g) : h ≤ᶠ[l] f ⊔ g :=
hg.mono fun _ => _root_.le_sup_of_le_right
#align filter.eventually_le.le_sup_of_le_right Filter.EventuallyLe.le_sup_of_le_right
#align filter.eventually_le.le_sup_of_le_right Filter.EventuallyLE.le_sup_of_le_right

theorem join_le {f : Filter (Filter α)} {l : Filter α} (h : ∀ᶠ m in f, m ≤ l) : join f ≤ l :=
fun _ hs => h.mono fun _ hm => hm hs
Expand Down Expand Up @@ -2706,10 +2706,10 @@ theorem eventuallyEq_bind {f : Filter α} {m : α → Filter β} {g₁ g₂ : β
#align filter.eventually_eq_bind Filter.eventuallyEq_bind

@[simp]
theorem eventuallyLe_bind [LE γ] {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ} :
theorem eventuallyLE_bind [LE γ] {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ} :
g₁ ≤ᶠ[bind f m] g₂ ↔ ∀ᶠ x in f, g₁ ≤ᶠ[m x] g₂ :=
Iff.rfl
#align filter.eventually_le_bind Filter.eventuallyLe_bind
#align filter.eventually_le_bind Filter.eventuallyLE_bind

theorem mem_bind' {s : Set β} {f : Filter α} {m : α → Filter β} :
s ∈ bind f m ↔ { a | s ∈ m a } ∈ f :=
Expand Down Expand Up @@ -3103,9 +3103,9 @@ theorem Set.EqOn.eventuallyEq_of_mem {α β} {s : Set α} {l : Filter α} {f g :
h.eventuallyEq.filter_mono <| Filter.le_principal_iff.2 hl
#align set.eq_on.eventually_eq_of_mem Set.EqOn.eventuallyEq_of_mem

theorem HasSubset.Subset.eventuallyLe {α} {l : Filter α} {s t : Set α} (h : s ⊆ t) : s ≤ᶠ[l] t :=
theorem HasSubset.Subset.eventuallyLE {α} {l : Filter α} {s t : Set α} (h : s ⊆ t) : s ≤ᶠ[l] t :=
Filter.eventually_of_forall h
#align has_subset.subset.eventually_le HasSubset.Subset.eventuallyLe
#align has_subset.subset.eventually_le HasSubset.Subset.eventuallyLE

theorem Set.MapsTo.tendsto {α β} {s : Set α} {t : Set β} {f : α → β} (h : MapsTo f s t) :
Filter.Tendsto f (𝓟 s) (𝓟 t) :=
Expand Down
36 changes: 18 additions & 18 deletions Mathlib/Order/Filter/CountableInter.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -74,57 +74,57 @@ theorem eventually_countable_ball {ι : Type _} {S : Set ι} (hS : S.Countable)
@countable_bInter_mem _ l _ _ _ hS fun i hi => { x | p x i hi }
#align eventually_countable_ball eventually_countable_ball

theorem EventuallyLe.countable_unionᵢ [Countable ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) :
theorem EventuallyLE.countable_unionᵢ [Countable ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) :
(⋃ i, s i) ≤ᶠ[l] ⋃ i, t i :=
(eventually_countable_forall.2 h).mono fun _ hst hs => mem_unionᵢ.2 <| (mem_unionᵢ.1 hs).imp hst
#align eventually_le.countable_Union EventuallyLe.countable_unionᵢ
#align eventually_le.countable_Union EventuallyLE.countable_unionᵢ

theorem EventuallyEq.countable_unionᵢ [Countable ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) :
(⋃ i, s i) =ᶠ[l] ⋃ i, t i :=
(EventuallyLe.countable_unionᵢ fun i => (h i).le).antisymm
(EventuallyLe.countable_unionᵢ fun i => (h i).symm.le)
(EventuallyLE.countable_unionᵢ fun i => (h i).le).antisymm
(EventuallyLE.countable_unionᵢ fun i => (h i).symm.le)
#align eventually_eq.countable_Union EventuallyEq.countable_unionᵢ

theorem EventuallyLe.countable_bUnion {ι : Type _} {S : Set ι} (hS : S.Countable)
theorem EventuallyLE.countable_bUnion {ι : Type _} {S : Set ι} (hS : S.Countable)
{s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) :
(⋃ i ∈ S, s i ‹_›) ≤ᶠ[l] ⋃ i ∈ S, t i ‹_› := by
simp only [bunionᵢ_eq_unionᵢ]
haveI := hS.toEncodable
exact EventuallyLe.countable_unionᵢ fun i => h i i.2
#align eventually_le.countable_bUnion EventuallyLe.countable_bUnion
exact EventuallyLE.countable_unionᵢ fun i => h i i.2
#align eventually_le.countable_bUnion EventuallyLE.countable_bUnion

theorem EventuallyEq.countable_bUnion {ι : Type _} {S : Set ι} (hS : S.Countable)
{s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi =ᶠ[l] t i hi) :
(⋃ i ∈ S, s i ‹_›) =ᶠ[l] ⋃ i ∈ S, t i ‹_› :=
(EventuallyLe.countable_bUnion hS fun i hi => (h i hi).le).antisymm
(EventuallyLe.countable_bUnion hS fun i hi => (h i hi).symm.le)
(EventuallyLE.countable_bUnion hS fun i hi => (h i hi).le).antisymm
(EventuallyLE.countable_bUnion hS fun i hi => (h i hi).symm.le)
#align eventually_eq.countable_bUnion EventuallyEq.countable_bUnion

theorem EventuallyLe.countable_interᵢ [Countable ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) :
theorem EventuallyLE.countable_interᵢ [Countable ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) :
(⋂ i, s i) ≤ᶠ[l] ⋂ i, t i :=
(eventually_countable_forall.2 h).mono fun _ hst hs =>
mem_interᵢ.2 fun i => hst _ (mem_interᵢ.1 hs i)
#align eventually_le.countable_Inter EventuallyLe.countable_interᵢ
#align eventually_le.countable_Inter EventuallyLE.countable_interᵢ

theorem EventuallyEq.countable_interᵢ [Countable ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) :
(⋂ i, s i) =ᶠ[l] ⋂ i, t i :=
(EventuallyLe.countable_interᵢ fun i => (h i).le).antisymm
(EventuallyLe.countable_interᵢ fun i => (h i).symm.le)
(EventuallyLE.countable_interᵢ fun i => (h i).le).antisymm
(EventuallyLE.countable_interᵢ fun i => (h i).symm.le)
#align eventually_eq.countable_Inter EventuallyEq.countable_interᵢ

theorem EventuallyLe.countable_bInter {ι : Type _} {S : Set ι} (hS : S.Countable)
theorem EventuallyLE.countable_bInter {ι : Type _} {S : Set ι} (hS : S.Countable)
{s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) :
(⋂ i ∈ S, s i ‹_›) ≤ᶠ[l] ⋂ i ∈ S, t i ‹_› := by
simp only [binterᵢ_eq_interᵢ]
haveI := hS.toEncodable
exact EventuallyLe.countable_interᵢ fun i => h i i.2
#align eventually_le.countable_bInter EventuallyLe.countable_bInter
exact EventuallyLE.countable_interᵢ fun i => h i i.2
#align eventually_le.countable_bInter EventuallyLE.countable_bInter

theorem EventuallyEq.countable_bInter {ι : Type _} {S : Set ι} (hS : S.Countable)
{s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi =ᶠ[l] t i hi) :
(⋂ i ∈ S, s i ‹_›) =ᶠ[l] ⋂ i ∈ S, t i ‹_› :=
(EventuallyLe.countable_bInter hS fun i hi => (h i hi).le).antisymm
(EventuallyLe.countable_bInter hS fun i hi => (h i hi).symm.le)
(EventuallyLE.countable_bInter hS fun i hi => (h i hi).le).antisymm
(EventuallyLE.countable_bInter hS fun i hi => (h i hi).symm.le)
#align eventually_eq.countable_bInter EventuallyEq.countable_bInter

/-- Construct a filter with countable intersection property. This constructor deduces
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Order/Filter/ENNReal.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@ theorem limsup_eq_zero_iff [CountableInterFilter f] {u : α → ℝ≥0∞} : f.
by
constructor <;> intro h
· have hu_zero :=
EventuallyLe.trans (eventually_le_limsup u) (eventually_of_forall fun _ => le_of_eq h)
EventuallyLE.trans (eventually_le_limsup u) (eventually_of_forall fun _ => le_of_eq h)
exact hu_zero.mono fun x hx => le_antisymm hx (zero_le _)
· rw [limsup_congr h]
simp_rw [Pi.zero_apply, ← ENNReal.bot_eq_zero, limsup_const_bot]
Expand Down
10 changes: 5 additions & 5 deletions Mathlib/Order/Filter/Extr.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -634,13 +634,13 @@ section Eventually
/-! ### Relation with `eventually` comparisons of two functions -/


theorem Filter.EventuallyLe.isMaxFilter {α β : Type _} [Preorder β] {f g : α → β} {a : α}
theorem Filter.EventuallyLE.isMaxFilter {α β : Type _} [Preorder β] {f g : α → β} {a : α}
{l : Filter α} (hle : g ≤ᶠ[l] f) (hfga : f a = g a) (h : IsMaxFilter f l a) :
IsMaxFilter g l a := by
refine' hle.mp (h.mono fun x hf hgf => _)
rw [← hfga]
exact le_trans hgf hf
#align filter.eventually_le.is_max_filter Filter.EventuallyLe.isMaxFilter
#align filter.eventually_le.is_max_filter Filter.EventuallyLE.isMaxFilter

theorem IsMaxFilter.congr {α β : Type _} [Preorder β] {f g : α → β} {a : α} {l : Filter α}
(h : IsMaxFilter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) : IsMaxFilter g l a :=
Expand All @@ -652,11 +652,11 @@ theorem Filter.EventuallyEq.isMaxFilter_iff {α β : Type _} [Preorder β] {f g
⟨fun h => h.congr heq hfga, fun h => h.congr heq.symm hfga.symm⟩
#align filter.eventually_eq.is_max_filter_iff Filter.EventuallyEq.isMaxFilter_iff

theorem Filter.EventuallyLe.isMinFilter {α β : Type _} [Preorder β] {f g : α → β} {a : α}
theorem Filter.EventuallyLE.isMinFilter {α β : Type _} [Preorder β] {f g : α → β} {a : α}
{l : Filter α} (hle : f ≤ᶠ[l] g) (hfga : f a = g a) (h : IsMinFilter f l a) :
IsMinFilter g l a :=
@Filter.EventuallyLe.isMaxFilter _ βᵒᵈ _ _ _ _ _ hle hfga h
#align filter.eventually_le.is_min_filter Filter.EventuallyLe.isMinFilter
@Filter.EventuallyLE.isMaxFilter _ βᵒᵈ _ _ _ _ _ hle hfga h
#align filter.eventually_le.is_min_filter Filter.EventuallyLE.isMinFilter

theorem IsMinFilter.congr {α β : Type _} [Preorder β] {f g : α → β} {a : α} {l : Filter α}
(h : IsMinFilter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) : IsMinFilter g l a :=
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Order/Filter/FilterProduct.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ instance field [Field β] : Field β* :=
{ Germ.commRing, Germ.divisionRing with }

theorem coe_lt [Preorder β] {f g : α → β} : (f : β*) < g ↔ ∀* x, f x < g x := by
simp only [lt_iff_le_not_le, eventually_and, coe_le, eventually_not, EventuallyLe]
simp only [lt_iff_le_not_le, eventually_and, coe_le, eventually_not, EventuallyLE]
#align filter.germ.coe_lt Filter.Germ.coe_lt

theorem coe_pos [Preorder β] [Zero β] {f : α → β} : 0 < (f : β*) ↔ ∀* x, 0 < f x :=
Expand Down
Loading