From a9f9caa86393f51286190f2d4f9cdaab4dc453ff Mon Sep 17 00:00:00 2001 From: sgouezel Date: Fri, 26 Jun 2026 16:05:37 +0200 Subject: [PATCH 1/2] cherry pick --- Mathlib/Topology/Order/LeftRightLim.lean | 37 +++++++++++------------- 1 file changed, 17 insertions(+), 20 deletions(-) diff --git a/Mathlib/Topology/Order/LeftRightLim.lean b/Mathlib/Topology/Order/LeftRightLim.lean index e423bb8009f047..349daa40030a6a 100644 --- a/Mathlib/Topology/Order/LeftRightLim.lean +++ b/Mathlib/Topology/Order/LeftRightLim.lean @@ -64,18 +64,17 @@ noncomputable def Function.rightLim (f : α → β) (a : α) : β := open Function theorem leftLim_eq_of_tendsto [hα : TopologicalSpace α] [h'α : OrderTopology α] [T2Space β] - {f : α → β} {a : α} {y : β} (h : 𝓝[<] a ≠ ⊥) (h' : Tendsto f (𝓝[<] a) (𝓝 y)) : + {f : α → β} {a : α} {y : β} [h : (𝓝[<] a).NeBot] (h' : Tendsto f (𝓝[<] a) (𝓝 y)) : leftLim f a = y := by have h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y) := ⟨y, h'⟩ rw [h'α.topology_eq_generate_intervals] at h h' h'' - simp only [leftLim, h, h'', not_true, or_self_iff, if_false] - haveI := neBot_iff.2 h + simp only [leftLim, neBot_iff.mp h, h'', not_true, or_self_iff, if_false] exact lim_eq h' theorem rightLim_eq_of_tendsto [TopologicalSpace α] [OrderTopology α] [T2Space β] - {f : α → β} {a : α} {y : β} (h : 𝓝[>] a ≠ ⊥) (h' : Tendsto f (𝓝[>] a) (𝓝 y)) : + {f : α → β} {a : α} {y : β} [h : (𝓝[>] a).NeBot] (h' : Tendsto f (𝓝[>] a) (𝓝 y)) : Function.rightLim f a = y := - leftLim_eq_of_tendsto (α := αᵒᵈ) h h' + leftLim_eq_of_tendsto (α := αᵒᵈ) (h := h) h' theorem leftLim_eq_of_eq_bot [hα : TopologicalSpace α] [h'α : OrderTopology α] (f : α → β) {a : α} (h : 𝓝[<] a = ⊥) : leftLim f a = f a := by @@ -111,9 +110,9 @@ theorem rightLim_eq_of_isTop {f : α → β} {a : α} (ha : IsTop a) : theorem ContinuousWithinAt.leftLim_eq [TopologicalSpace α] [OrderTopology α] [T2Space β] {f : α → β} {a : α} (hf : ContinuousWithinAt f (Iic a) a) : leftLim f a = f a := by - rcases eq_or_ne (𝓝[<] a) ⊥ with h' | h' + rcases eq_or_neBot (𝓝[<] a) with h' | h' · simp [leftLim_eq_of_eq_bot f h'] - apply leftLim_eq_of_tendsto h' + apply leftLim_eq_of_tendsto exact hf.tendsto.mono_left (nhdsWithin_mono _ Iio_subset_Iic_self) theorem ContinuousWithinAt.rightLim_eq [TopologicalSpace α] [OrderTopology α] [T2Space β] @@ -195,7 +194,7 @@ theorem leftLim_rightLim [TopologicalSpace α] [OrderTopology α] [T3Space β] {f : α → β} {a : α} (h : Tendsto f (𝓝[<] a) (𝓝 (f.leftLim a))) [h' : (𝓝[<] a).NeBot] : f.rightLim.leftLim a = f.leftLim a := by obtain ⟨b, hb⟩ : (Iio a).Nonempty := Filter.nonempty_of_mem (self_mem_nhdsWithin (a := a)) - apply leftLim_eq_of_tendsto (neBot_iff.mp h') + apply leftLim_eq_of_tendsto apply (closed_nhds_basis (f.leftLim a)).tendsto_right_iff.2 rintro s ⟨s_mem, s_closed⟩ obtain ⟨u, au, hu⟩ : ∃ u, u < a ∧ Ioo u a ⊆ {x | f x ∈ s} := by @@ -273,24 +272,23 @@ variable {α β : Type*} [LinearOrder α] [ConditionallyCompleteLinearOrder β] [OrderTopology β] {f : α → β} (hf : Monotone f) {x y : α} include hf -theorem leftLim_eq_sSup [TopologicalSpace α] [OrderTopology α] (h : 𝓝[<] x ≠ ⊥) : +theorem leftLim_eq_sSup [TopologicalSpace α] [OrderTopology α] [(𝓝[<] x).NeBot] : leftLim f x = sSup (f '' Iio x) := - leftLim_eq_of_tendsto h (hf.tendsto_nhdsLT x) + leftLim_eq_of_tendsto (hf.tendsto_nhdsLT x) -theorem rightLim_eq_sInf [TopologicalSpace α] [OrderTopology α] (h : 𝓝[>] x ≠ ⊥) : +theorem rightLim_eq_sInf [TopologicalSpace α] [OrderTopology α] [(𝓝[>] x).NeBot] : rightLim f x = sInf (f '' Ioi x) := - rightLim_eq_of_tendsto h (hf.tendsto_nhdsGT x) + rightLim_eq_of_tendsto (hf.tendsto_nhdsGT x) theorem leftLim_le (h : x ≤ y) : leftLim f x ≤ f y := by letI : TopologicalSpace α := Preorder.topology α haveI : OrderTopology α := ⟨rfl⟩ - rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h') + rcases eq_or_neBot (𝓝[<] x) with h' | h' · simpa [leftLim, h'] using hf h - haveI A : NeBot (𝓝[<] x) := neBot_iff.2 h' - rw [leftLim_eq_sSup hf h'] + rw [leftLim_eq_sSup hf] refine csSup_le ?_ ?_ · simp only [image_nonempty] - exact (forall_mem_nonempty_iff_neBot.2 A) _ self_mem_nhdsWithin + exact (forall_mem_nonempty_iff_neBot.2 h') _ self_mem_nhdsWithin · simp only [mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] intro z hz exact hf (hz.le.trans h) @@ -298,10 +296,10 @@ theorem leftLim_le (h : x ≤ y) : leftLim f x ≤ f y := by theorem le_leftLim (h : x < y) : f x ≤ leftLim f y := by letI : TopologicalSpace α := Preorder.topology α haveI : OrderTopology α := ⟨rfl⟩ - rcases eq_or_ne (𝓝[<] y) ⊥ with (h' | h') + rcases eq_or_neBot (𝓝[<] y) with h' | h' · rw [leftLim_eq_of_eq_bot _ h'] exact hf h.le - rw [leftLim_eq_sSup hf h'] + rw [leftLim_eq_sSup hf] refine le_csSup ⟨f y, ?_⟩ (mem_image_of_mem _ h) simp only [upperBounds, mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq] @@ -356,9 +354,8 @@ theorem tendsto_rightLim_within (x : α) : Tendsto f (𝓝[>] x) (𝓝[≥] righ coincides with the value of the function. -/ theorem continuousWithinAt_Iio_iff_leftLim_eq : ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x := by - rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h') + rcases eq_or_neBot (𝓝[<] x) with h' | h' · simp [leftLim_eq_of_eq_bot f h', ContinuousWithinAt, h'] - haveI : (𝓝[Iio x] x).NeBot := neBot_iff.2 h' refine ⟨fun h => tendsto_nhds_unique (hf.tendsto_leftLim x) h.tendsto, fun h => ?_⟩ have := hf.tendsto_leftLim x rwa [h] at this From f370e4ea872539f265d85e1f7560431286c94e43 Mon Sep 17 00:00:00 2001 From: sgouezel Date: Fri, 26 Jun 2026 20:37:03 +0200 Subject: [PATCH 2/2] fix --- Mathlib/MeasureTheory/Measure/Stieltjes.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Mathlib/MeasureTheory/Measure/Stieltjes.lean b/Mathlib/MeasureTheory/Measure/Stieltjes.lean index f61f16fa6b1d78..eaa70d12d2e15b 100644 --- a/Mathlib/MeasureTheory/Measure/Stieltjes.lean +++ b/Mathlib/MeasureTheory/Measure/Stieltjes.lean @@ -148,8 +148,6 @@ theorem iInf_Ioi_eq [OrderTopology R] [DenselyOrdered R] [NoMaxOrder R] (f : StieltjesFunction R) (x : R) : ⨅ r : Ioi x, f r = f x := by suffices Function.rightLim f x = ⨅ r : Ioi x, f r by rw [← this, f.rightLim_eq] rw [f.mono.rightLim_eq_sInf, sInf_image'] - rw [← neBot_iff] - infer_instance theorem iInf_rat_gt_eq (f : StieltjesFunction ℝ) (x : ℝ) : ⨅ r : { r' : ℚ // x < r' }, f r = f x := by