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

[Ruben-VandeVelde]

---

[Vierkantor]

I still see the following usages of eventuallyLe:

mathlib4$ rg 'eventuallyLe'
Mathlib/Order/Filter/IndicatorFunction.lean
57:theorem indicator_eventuallyLe_indicator (h : f ≤ᶠ[l ⊓ 𝓟 s] g) :
60:#align indicator_eventually_le_indicator indicator_eventuallyLe_indicator

Mathlib/Order/Filter/Basic.lean
1635:theorem eventuallyLe_congr {f f' g g' : α → β} (hf : f =ᶠ[l] f') (hg : g =ᶠ[l] g') :
1638:#align filter.eventually_le_congr Filter.eventuallyLe_congr
1681:theorem eventuallyLe_antisymm_iff [PartialOrder β] {l : Filter α} {f g : α → β} :
1684:#align filter.eventually_le_antisymm_iff Filter.eventuallyLe_antisymm_iff
2709:theorem eventuallyLe_bind [LE γ] {f : Filter α} {m : α → Filter β} {g₁ g₂ : β → γ} :
2712:#align filter.eventually_le_bind Filter.eventuallyLe_bind
3096:theorem HasSubset.Subset.eventuallyLe {α} {l : Filter α} {s t : Set α} (h : s ⊆ t) : s ≤ᶠ[l] t :=
3098:#align has_subset.subset.eventually_le HasSubset.Subset.eventuallyLe

Mathlib/Topology/Order/Basic.lean
177:alias le_of_tendsto_of_tendsto ← tendsto_le_of_eventuallyLe
178:#align tendsto_le_of_eventually_le tendsto_le_of_eventuallyLe

Mathlib/Topology/Basic.lean
1009:theorem eventually_eventuallyLe_nhds [LE β] {f g : α → β} {a : α} :
1012:#align eventually_eventually_le_nhds eventually_eventuallyLe_nhds
1023:theorem Filter.EventuallyLE.eventuallyLe_nhds [LE β] {f g : α → β} {a : α} (h : f ≤ᶠ[𝓝 a] g) :
1026:#align filter.eventually_le.eventually_le_nhds Filter.EventuallyLE.eventuallyLe_nhds

[Vierkantor]

Thanks!

bors d+

[bors]

✌️ Ruben-VandeVelde can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[Ruben-VandeVelde]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style