diff --git a/Mathlib/Algebra/Order/Floor/Prime.lean b/Mathlib/Algebra/Order/Floor/Prime.lean index 506029de21811..8158125cc8e49 100644 --- a/Mathlib/Algebra/Order/Floor/Prime.lean +++ b/Mathlib/Algebra/Order/Floor/Prime.lean @@ -39,7 +39,7 @@ theorem exists_prime_mul_pow_div_factorial_lt_one [LinearOrderedField K] [FloorR letI := Preorder.topology K haveI : OrderTopology K := ⟨rfl⟩ ((Filter.frequently_atTop.mpr Nat.exists_infinite_primes).and_eventually - (eventually_lt_of_tendsto_lt zero_lt_one + (Filter.Tendsto.eventually_lt_const zero_lt_one (FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop a c 1))).forall_exists_of_atTop (n + 1) diff --git a/Mathlib/Analysis/Asymptotics/TVS.lean b/Mathlib/Analysis/Asymptotics/TVS.lean index f116d2b07113c..e4d49370e6a0a 100644 --- a/Mathlib/Analysis/Asymptotics/TVS.lean +++ b/Mathlib/Analysis/Asymptotics/TVS.lean @@ -125,7 +125,7 @@ lemma isLittleOTVS_one [ContinuousSMul 𝕜 E] {f : α → E} {l : Filter α} : rcases NormedField.exists_one_lt_norm 𝕜 with ⟨c, hc⟩ obtain ⟨ε, hε₀, hε⟩ : ∃ ε : ℝ≥0, 0 < ε ∧ (ε * ‖c‖₊ / r : ℝ≥0∞) < 1 := by apply Eventually.exists_gt - refine eventually_lt_of_tendsto_lt zero_lt_one <| Continuous.tendsto' ?_ _ _ (by simp) + refine Continuous.tendsto' ?_ _ _ (by simp) |>.eventually_lt_const zero_lt_one fun_prop (disch := intros; first | apply ENNReal.coe_ne_top | positivity) filter_upwards [hr ε hε₀.ne'] with x hx refine mem_of_egauge_lt_one hUb (hx.trans_lt ?_) diff --git a/Mathlib/Analysis/BoundedVariation.lean b/Mathlib/Analysis/BoundedVariation.lean index 4f281d9bfca6d..4a2fafb5a8000 100644 --- a/Mathlib/Analysis/BoundedVariation.lean +++ b/Mathlib/Analysis/BoundedVariation.lean @@ -180,7 +180,7 @@ theorem lowerSemicontinuous_aux {ι : Type*} {F : ι → α → E} {p : Filter (𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))) := by apply tendsto_finset_sum exact fun i _ => Tendsto.edist (Ffs (u i.succ) (us i.succ)) (Ffs (u i) (us i)) - exact (eventually_gt_of_tendsto_gt hlt this).mono fun i h => h.trans_le (sum_le (F i) n um us) + exact (this.eventually_const_lt hlt).mono fun i h => h.trans_le (sum_le (F i) n um us) /-- The map `(eVariationOn · s)` is lower semicontinuous for pointwise convergence *on `s`*. Pointwise convergence on `s` is encoded here as uniform convergence on the family consisting of the diff --git a/Mathlib/Analysis/Normed/Lp/lpSpace.lean b/Mathlib/Analysis/Normed/Lp/lpSpace.lean index 4797943bc7ec5..b2a36ecac89b5 100644 --- a/Mathlib/Analysis/Normed/Lp/lpSpace.lean +++ b/Mathlib/Analysis/Normed/Lp/lpSpace.lean @@ -183,7 +183,7 @@ theorem of_exponent_ge {p q : ℝ≥0∞} {f : ∀ i, E i} (hfq : Memℓp f q) ( have hf' := hfq.summable hq refine .of_norm_bounded_eventually _ hf' (@Set.Finite.subset _ { i | 1 ≤ ‖f i‖ } ?_ _ ?_) · have H : { x : α | 1 ≤ ‖f x‖ ^ q.toReal }.Finite := by - simpa using eventually_lt_of_tendsto_lt (by norm_num) hf'.tendsto_cofinite_zero + simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by norm_num) exact H.subset fun i hi => Real.one_le_rpow hi hq.le · show ∀ i, ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖ intro i hi diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean index 71ae3fbd4d054..49c7cb8a86df9 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean +++ b/Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean @@ -592,7 +592,7 @@ theorem tendsto_one_plus_div_rpow_exp (t : ℝ) : have h₁ : (1 : ℝ) / 2 < 1 := by norm_num have h₂ : Tendsto (fun x : ℝ => 1 + t / x) atTop (𝓝 1) := by simpa using (tendsto_inv_atTop_zero.const_mul t).const_add 1 - refine (eventually_ge_of_tendsto_gt h₁ h₂).mono fun x hx => ?_ + refine (h₂.eventually_const_le h₁).mono fun x hx => ?_ have hx' : 0 < 1 + t / x := by linarith simp [mul_comm x, exp_mul, exp_log hx'] diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index 69992fdb4a113..cf5f9286f5bd2 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -601,7 +601,7 @@ theorem summable_of_ratio_test_tendsto_lt_one {α : Type*} [NormedAddCommGroup (h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)) : Summable f := by rcases exists_between hl₁ with ⟨r, hr₀, hr₁⟩ refine summable_of_ratio_norm_eventually_le hr₁ ?_ - filter_upwards [eventually_le_of_tendsto_lt hr₀ h, hf] with _ _ h₁ + filter_upwards [h.eventually_le_const hr₀, hf] with _ _ h₁ rwa [← div_le_iff₀ (norm_pos_iff.mpr h₁)] theorem not_summable_of_ratio_norm_eventually_ge {α : Type*} [SeminormedAddCommGroup α] {f : ℕ → α} @@ -629,12 +629,12 @@ theorem not_summable_of_ratio_test_tendsto_gt_one {α : Type*} [SeminormedAddCom {f : ℕ → α} {l : ℝ} (hl : 1 < l) (h : Tendsto (fun n ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)) : ¬Summable f := by have key : ∀ᶠ n in atTop, ‖f n‖ ≠ 0 := by - filter_upwards [eventually_ge_of_tendsto_gt hl h] with _ hn hc + filter_upwards [h.eventually_const_le hl] with _ hn hc rw [hc, _root_.div_zero] at hn linarith rcases exists_between hl with ⟨r, hr₀, hr₁⟩ refine not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently ?_ - filter_upwards [eventually_ge_of_tendsto_gt hr₁ h, key] with _ _ h₁ + filter_upwards [h.eventually_const_le hr₁, key] with _ _ h₁ rwa [← le_div_iff₀ (lt_of_le_of_ne (norm_nonneg _) h₁.symm)] section NormedDivisionRing diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean index 9cfbcd713b62a..7cd217fadb8cf 100644 --- a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean +++ b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean @@ -544,9 +544,9 @@ lemma tendsto_atTop_sumCoeffsExp : Tendsto (fun (p : ℝ) => ∑ i, a i * (b i) lemma one_mem_range_sumCoeffsExp : 1 ∈ Set.range (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) := by refine mem_range_of_exists_le_of_exists_ge R.continuous_sumCoeffsExp ?le_one ?ge_one case le_one => - exact Eventually.exists <| eventually_le_of_tendsto_lt zero_lt_one R.tendsto_zero_sumCoeffsExp + exact R.tendsto_zero_sumCoeffsExp.eventually_le_const zero_lt_one |>.exists case ge_one => - exact Eventually.exists <| R.tendsto_atTop_sumCoeffsExp.eventually_ge_atTop _ + exact R.tendsto_atTop_sumCoeffsExp.eventually_ge_atTop _ |>.exists /-- The function x ↦ ∑ a_i b_i^x is injective. This implies the uniqueness of `p`. -/ lemma injective_sumCoeffsExp : Function.Injective (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) := diff --git a/Mathlib/Data/Real/Pi/Irrational.lean b/Mathlib/Data/Real/Pi/Irrational.lean index e3884b774698d..afebb88a105b2 100644 --- a/Mathlib/Data/Real/Pi/Irrational.lean +++ b/Mathlib/Data/Real/Pi/Irrational.lean @@ -283,8 +283,8 @@ private lemma not_irrational_exists_rep {x : ℝ} : rwa [lt_div_iff₀ (by positivity), zero_mul] at this have k (n : ℕ) : 0 < (a : ℝ) ^ (2 * n + 1) / n ! := by positivity have j : ∀ᶠ n : ℕ in atTop, (a : ℝ) ^ (2 * n + 1) / n ! * I n (π / 2) < 1 := by - have := eventually_lt_of_tendsto_lt (show (0 : ℝ) < 1 / 2 by norm_num) - (tendsto_pow_div_factorial_at_top_aux a) + have := (tendsto_pow_div_factorial_at_top_aux a).eventually_lt_const + (show (0 : ℝ) < 1 / 2 by norm_num) filter_upwards [this] with n hn rw [lt_div_iff₀ (zero_lt_two : (0 : ℝ) < 2)] at hn exact hn.trans_le' (mul_le_mul_of_nonneg_left (I_le _) (by positivity)) diff --git a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean index ce393e78fea5c..10f195e4aacff 100644 --- a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean +++ b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean @@ -193,12 +193,12 @@ theorem ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ [SigmaFinite μ] have : Tendsto (fun n => g x + u n) atTop (𝓝 (g x + (0 : ℝ≥0))) := tendsto_const_nhds.add (ENNReal.tendsto_coe.2 u_lim) simp only [ENNReal.coe_zero, add_zero] at this - exact eventually_le_of_tendsto_lt hx this + exact this.eventually_le_const hx have L2 : ∀ᶠ n : ℕ in (atTop : Filter ℕ), g x ≤ (n : ℝ≥0) := - haveI : Tendsto (fun n : ℕ => ((n : ℝ≥0) : ℝ≥0∞)) atTop (𝓝 ∞) := by + have : Tendsto (fun n : ℕ => ((n : ℝ≥0) : ℝ≥0∞)) atTop (𝓝 ∞) := by simp only [ENNReal.coe_natCast] exact ENNReal.tendsto_nat_nhds_top - eventually_ge_of_tendsto_gt (hx.trans_le le_top) this + this.eventually_const_le (hx.trans_le le_top) apply Set.mem_iUnion.2 exact ((L1.and L2).and (eventually_mem_spanningSets μ x)).exists refine le_antisymm ?_ bot_le diff --git a/Mathlib/MeasureTheory/Function/LpSpace.lean b/Mathlib/MeasureTheory/Function/LpSpace.lean index 01ccd42815470..5b9c9290dac61 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace.lean +++ b/Mathlib/MeasureTheory/Function/LpSpace.lean @@ -673,8 +673,7 @@ theorem exists_eLpNorm_indicator_le (hp : p ≠ ∞) (c : E) {ε : ℝ≥0∞} ( convert (NNReal.continuousAt_rpow_const (Or.inr hp₀')).tendsto.const_mul _ simp [hp₀''.ne'] have hε' : 0 < ε := hε.bot_lt - obtain ⟨δ, hδ, hδε'⟩ := - NNReal.nhds_zero_basis.eventually_iff.mp (eventually_le_of_tendsto_lt hε' this) + obtain ⟨δ, hδ, hδε'⟩ := NNReal.nhds_zero_basis.eventually_iff.mp (this.eventually_le_const hε') obtain ⟨η, hη, hηδ⟩ := exists_between hδ refine ⟨η, hη, ?_⟩ rw [← ENNReal.coe_rpow_of_nonneg _ hp₀', ← ENNReal.coe_mul] diff --git a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean index e2ec1a0114d79..9678b171ff3fc 100644 --- a/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean +++ b/Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean @@ -388,9 +388,7 @@ theorem AECover.iSup_lintegral_eq_of_countably_generated [Nonempty ι] [l.NeBot] have := hφ.lintegral_tendsto_of_countably_generated hfm refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun i => lintegral_mono' Measure.restrict_le_self le_rfl) fun w hw => ?_ - rcases exists_between hw with ⟨m, hm₁, hm₂⟩ - rcases (eventually_ge_of_tendsto_gt hm₂ this).exists with ⟨i, hi⟩ - exact ⟨i, lt_of_lt_of_le hm₁ hi⟩ + exact (this.eventually_const_lt hw).exists end Lintegral diff --git a/Mathlib/MeasureTheory/Measure/Portmanteau.lean b/Mathlib/MeasureTheory/Measure/Portmanteau.lean index 4d82e897d1771..72fe3305828be 100644 --- a/Mathlib/MeasureTheory/Measure/Portmanteau.lean +++ b/Mathlib/MeasureTheory/Measure/Portmanteau.lean @@ -278,14 +278,14 @@ theorem FiniteMeasure.limsup_measure_closed_le_of_tendsto {Ω ι : Type*} {L : F HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed (μ : Measure Ω) have room₁ : (μ : Measure Ω) F < (μ : Measure Ω) F + ε / 2 := ENNReal.lt_add_right (measure_lt_top (μ : Measure Ω) F).ne ε_pos' - obtain ⟨M, hM⟩ := eventually_atTop.mp <| eventually_lt_of_tendsto_lt room₁ key₁ + obtain ⟨M, hM⟩ := eventually_atTop.mp <| key₁.eventually_lt_const room₁ have key₂ := FiniteMeasure.tendsto_iff_forall_lintegral_tendsto.mp μs_lim (fs M) have room₂ : (lintegral (μ : Measure Ω) fun a ↦ fs M a) < (lintegral (μ : Measure Ω) fun a ↦ fs M a) + ε / 2 := ENNReal.lt_add_right (ne_of_lt ((fs M).lintegral_lt_top_of_nnreal _)) ε_pos' - have ev_near := Eventually.mono (eventually_lt_of_tendsto_lt room₂ key₂) fun n ↦ le_of_lt - have ev_near' := Eventually.mono ev_near + have ev_near := key₂.eventually_le_const room₂ + have ev_near' := ev_near.mono (fun n ↦ le_trans (HasOuterApproxClosed.measure_le_lintegral F_closed (μs n) M)) apply (Filter.limsup_le_limsup ev_near').trans rw [limsup_const] diff --git a/Mathlib/MeasureTheory/Measure/WithDensity.lean b/Mathlib/MeasureTheory/Measure/WithDensity.lean index d343307b3e3fc..f8c9285e8bbbf 100644 --- a/Mathlib/MeasureTheory/Measure/WithDensity.lean +++ b/Mathlib/MeasureTheory/Measure/WithDensity.lean @@ -669,7 +669,7 @@ lemma IsLocallyFiniteMeasure.withDensity_coe {f : α → ℝ≥0} (hf : Continuo IsLocallyFiniteMeasure (μ.withDensity fun x ↦ f x) := by refine ⟨fun x ↦ ?_⟩ rcases (μ.finiteAt_nhds x).exists_mem_basis ((nhds_basis_opens' x).restrict_subset - (eventually_le_of_tendsto_lt (lt_add_one _) (hf.tendsto x))) with ⟨U, ⟨⟨hUx, hUo⟩, hUf⟩, hμU⟩ + ((hf.tendsto x).eventually_le_const (lt_add_one _))) with ⟨U, ⟨⟨hUx, hUo⟩, hUf⟩, hμU⟩ refine ⟨U, hUx, ?_⟩ rw [withDensity_apply _ hUo.measurableSet] exact setLIntegral_lt_top_of_bddAbove hμU.ne ⟨f x + 1, forall_mem_image.2 hUf⟩ diff --git a/Mathlib/Topology/Order/IntermediateValue.lean b/Mathlib/Topology/Order/IntermediateValue.lean index 81446ea8fdf08..ef73d422348e1 100644 --- a/Mathlib/Topology/Order/IntermediateValue.lean +++ b/Mathlib/Topology/Order/IntermediateValue.lean @@ -122,21 +122,20 @@ theorem IsPreconnected.intermediate_value {s : Set X} (hs : IsPreconnected s) {a theorem IsPreconnected.intermediate_value_Ico {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht : Tendsto f l (𝓝 v)) : Ico (f a) v ⊆ f '' s := fun _ h => - hs.intermediate_value₂_eventually₁ ha hl hf continuousOn_const h.1 - (eventually_ge_of_tendsto_gt h.2 ht) + hs.intermediate_value₂_eventually₁ ha hl hf continuousOn_const h.1 (ht.eventually_const_le h.2) theorem IsPreconnected.intermediate_value_Ioc {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht : Tendsto f l (𝓝 v)) : Ioc v (f a) ⊆ f '' s := fun _ h => (hs.intermediate_value₂_eventually₁ ha hl continuousOn_const hf h.2 - (eventually_le_of_tendsto_lt h.1 ht)).imp fun _ h => h.imp_right Eq.symm + (ht.eventually_le_const h.1)).imp fun _ h => h.imp_right Eq.symm theorem IsPreconnected.intermediate_value_Ioo {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) {v₁ v₂ : α} (ht₁ : Tendsto f l₁ (𝓝 v₁)) (ht₂ : Tendsto f l₂ (𝓝 v₂)) : Ioo v₁ v₂ ⊆ f '' s := fun _ h => hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const - (eventually_le_of_tendsto_lt h.1 ht₁) (eventually_ge_of_tendsto_gt h.2 ht₂) + (ht₁.eventually_le_const h.1) (ht₂.eventually_const_le h.2) theorem IsPreconnected.intermediate_value_Ici {s : Set X} (hs : IsPreconnected s) {a : X} {l : Filter X} (ha : a ∈ s) [NeBot l] (hl : l ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) @@ -153,19 +152,19 @@ theorem IsPreconnected.intermediate_value_Ioi {s : Set X} (hs : IsPreconnected s [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht₁ : Tendsto f l₁ (𝓝 v)) (ht₂ : Tendsto f l₂ atTop) : Ioi v ⊆ f '' s := fun y h => hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const - (eventually_le_of_tendsto_lt h ht₁) (tendsto_atTop.1 ht₂ y) + (ht₁.eventually_le_const h) (ht₂.eventually_ge_atTop y) theorem IsPreconnected.intermediate_value_Iio {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) {v : α} (ht₁ : Tendsto f l₁ atBot) (ht₂ : Tendsto f l₂ (𝓝 v)) : Iio v ⊆ f '' s := fun y h => - hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (tendsto_atBot.1 ht₁ y) - (eventually_ge_of_tendsto_gt h ht₂) + hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (ht₁.eventually_le_atBot y) + (ht₂.eventually_const_le h) theorem IsPreconnected.intermediate_value_Iii {s : Set X} (hs : IsPreconnected s) {l₁ l₂ : Filter X} [NeBot l₁] [NeBot l₂] (hl₁ : l₁ ≤ 𝓟 s) (hl₂ : l₂ ≤ 𝓟 s) {f : X → α} (hf : ContinuousOn f s) (ht₁ : Tendsto f l₁ atBot) (ht₂ : Tendsto f l₂ atTop) : univ ⊆ f '' s := fun y _ => - hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (tendsto_atBot.1 ht₁ y) - (tendsto_atTop.1 ht₂ y) + hs.intermediate_value₂_eventually₂ hl₁ hl₂ hf continuousOn_const (ht₁.eventually_le_atBot y) + (ht₂.eventually_ge_atTop y) /-- **Intermediate Value Theorem** for continuous functions on connected spaces. -/ theorem intermediate_value_univ [PreconnectedSpace X] (a b : X) {f : X → α} (hf : Continuous f) : diff --git a/Mathlib/Topology/Order/OrderClosed.lean b/Mathlib/Topology/Order/OrderClosed.lean index 4efa005c67f3f..7ded140f87a07 100644 --- a/Mathlib/Topology/Order/OrderClosed.lean +++ b/Mathlib/Topology/Order/OrderClosed.lean @@ -213,14 +213,20 @@ theorem Ici_mem_nhds (h : a < b) : Ici a ∈ 𝓝 b := theorem eventually_ge_nhds (hab : b < a) : ∀ᶠ x in 𝓝 a, b ≤ x := Ici_mem_nhds hab -theorem eventually_gt_of_tendsto_gt {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) +theorem Filter.Tendsto.eventually_const_lt {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Filter.Tendsto f l (𝓝 v)) : ∀ᶠ a in l, u < f a := h.eventually <| eventually_gt_nhds hv -theorem eventually_ge_of_tendsto_gt {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) +@[deprecated (since := "2024-11-17")] +alias eventually_gt_of_tendsto_gt := Filter.Tendsto.eventually_const_lt + +theorem Filter.Tendsto.eventually_const_le {l : Filter γ} {f : γ → α} {u v : α} (hv : u < v) (h : Tendsto f l (𝓝 v)) : ∀ᶠ a in l, u ≤ f a := h.eventually <| eventually_ge_nhds hv +@[deprecated (since := "2024-11-17")] +alias eventually_ge_of_tendsto_gt := Filter.Tendsto.eventually_const_le + protected theorem Dense.exists_gt [NoMaxOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, x < y := hs.exists_mem_open isOpen_Ioi (exists_gt x) @@ -451,14 +457,20 @@ theorem Iic_mem_nhds (h : a < b) : Iic b ∈ 𝓝 a := theorem eventually_le_nhds (hab : a < b) : ∀ᶠ x in 𝓝 a, x ≤ b := Iic_mem_nhds hab -theorem eventually_lt_of_tendsto_lt {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) +theorem Filter.Tendsto.eventually_lt_const {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) (h : Filter.Tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a < u := h.eventually <| eventually_lt_nhds hv -theorem eventually_le_of_tendsto_lt {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) +@[deprecated (since := "2024-11-17")] +alias eventually_lt_of_tendsto_lt := Filter.Tendsto.eventually_lt_const + +theorem Filter.Tendsto.eventually_le_const {l : Filter γ} {f : γ → α} {u v : α} (hv : v < u) (h : Tendsto f l (𝓝 v)) : ∀ᶠ a in l, f a ≤ u := h.eventually <| eventually_le_nhds hv +@[deprecated (since := "2024-11-17")] +alias eventually_le_of_tendsto_lt := Filter.Tendsto.eventually_le_const + protected theorem Dense.exists_lt [NoMinOrder α] {s : Set α} (hs : Dense s) (x : α) : ∃ y ∈ s, y < x := hs.orderDual.exists_gt x