--- a/src/HOL/Topological_Spaces.thy Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Topological_Spaces.thy Sat Sep 23 18:45:19 2023 +0100
@@ -1076,38 +1076,12 @@
unfolding Lim_def using tendsto_unique [of net f] by auto
lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
- by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
+ by (simp add: tendsto_Lim)
lemma Lim_cong:
- assumes "eventually (\<lambda>x. f x = g x) F" "F = G"
- shows "Lim F f = Lim G g"
-proof (cases "(\<exists>c. (f \<longlongrightarrow> c) F) \<and> F \<noteq> bot")
- case True
- then obtain c where c: "(f \<longlongrightarrow> c) F"
- by blast
- hence "Lim F f = c"
- using True by (intro tendsto_Lim) auto
- moreover have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G"
- using assms by (intro filterlim_cong) auto
- with True c assms have "Lim G g = c"
- by (intro tendsto_Lim) auto
- ultimately show ?thesis
- by simp
-next
- case False
- show ?thesis
- proof (cases "F = bot")
- case True
- thus ?thesis using assms
- by (auto simp: Topological_Spaces.Lim_def)
- next
- case False
- have "(f \<longlongrightarrow> c) F \<longleftrightarrow> (g \<longlongrightarrow> c) G" for c
- using assms by (intro filterlim_cong) auto
- thus ?thesis
- by (auto simp: Topological_Spaces.Lim_def)
- qed
-qed
+ assumes "\<forall>\<^sub>F x in F. f x = g x" "F = G"
+ shows "Lim F f = Lim F g"
+ unfolding t2_space_class.Lim_def using tendsto_cong assms by fastforce
lemma eventually_Lim_ident_at:
"(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>