# HG changeset patch
# User nipkow
# Date 1746591706 -7200
# Node ID 2f225d5044b54034025ee094ee554da2019343cd
# Parent  a61f82ddede4225ab0da331b298d97869db55306# Parent  a7d6d17abb28802eb03dc7132420762d5044a75c
merged

diff -r a7d6d17abb28 -r 2f225d5044b5 src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Wed May 07 06:20:42 2025 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Wed May 07 06:21:46 2025 +0200
@@ -1303,6 +1303,41 @@
   qed
 qed
 
+lemma Lim_left_bound:
+  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_bot} \<Rightarrow>
+    'b :: {linorder_topology, conditionally_complete_linorder}"
+  assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> b < x \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
+    and bnd: "\<And>b. b \<in> I \<Longrightarrow> b < x \<Longrightarrow> f b \<le> K"
+  shows "(f \<longlongrightarrow> Sup (f ` ({..<x} \<inter> I))) (at x within ({..<x} \<inter> I))"
+proof (cases "{..<x} \<inter> I = {}")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  show ?thesis
+  proof (rule order_tendstoI)
+    fix b
+    assume b: "Sup (f ` ({..<x} \<inter> I)) < b"
+    {
+      fix y
+      assume "y \<in> {..<x} \<inter> I"
+      with False bnd have "f y \<le> Sup (f ` ({..<x} \<inter> I))" by (auto intro!: cSup_upper bdd_aboveI2)
+      with b have "f y < b" by order
+    }
+    then show "eventually (\<lambda>x. f x < b) (at x within ({..<x} \<inter> I))"
+      by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
+  next
+    fix b
+    assume "b < Sup (f ` ({..<x} \<inter> I))"
+    from less_cSupD[OF _ this] False obtain y where y: "y < x" "y \<in> I" "b < f y" by auto
+    then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> b < f x) (at_left x)"
+      unfolding eventually_at_left[OF \<open>y < x\<close>] by (metis mono order_less_le order_less_le_trans)
+    then show "eventually (\<lambda>x. b < f x) (at x within ({..<x} \<inter> I))"
+      unfolding eventually_at_filter by eventually_elim simp
+  qed
+qed
+
+
 text\<open>These are special for limits out of the same topological space.\<close>
 
 lemma Lim_within_id: "(id \<longlongrightarrow> a) (at a within s)"
diff -r a7d6d17abb28 -r 2f225d5044b5 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed May 07 06:20:42 2025 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed May 07 06:21:46 2025 +0200
@@ -230,7 +230,7 @@
   by (metis (no_types) open_UNIV not_open_singleton)
 
 
-subsection \<open>Generators for toplogies\<close>
+subsection \<open>Generators for topologies\<close>
 
 inductive generate_topology :: "'a set set \<Rightarrow> 'a set \<Rightarrow> bool" for S :: "'a set set"
   where