--- a/src/HOL/Analysis/Uniform_Limit.thy Wed Mar 26 21:11:04 2025 +0000
+++ b/src/HOL/Analysis/Uniform_Limit.thy Fri Mar 28 00:26:10 2025 +0000
@@ -41,9 +41,22 @@
"(\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e) \<Longrightarrow> uniform_limit S f l F"
by (simp add: uniform_limit_iff)
+lemma uniform_limit_on_subset:
+ "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
+ by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
+
+lemma uniformly_convergent_on_subset:
+ assumes "uniformly_convergent_on A f" "B \<subseteq> A"
+ shows "uniformly_convergent_on B f"
+ using assms by (meson uniform_limit_on_subset uniformly_convergent_on_def)
+
lemma uniform_limit_singleton [simp]: "uniform_limit {x} f g F \<longleftrightarrow> ((\<lambda>n. f n x) \<longlongrightarrow> g x) F"
by (simp add: uniform_limit_iff tendsto_iff)
+lemma uniformly_convergent_on_singleton:
+ "uniformly_convergent_on {x} f \<longleftrightarrow> convergent (\<lambda>n. f n x)"
+ by (auto simp: uniformly_convergent_on_def convergent_def)
+
lemma uniform_limit_sequentially_iff:
"uniform_limit S f l sequentially \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x \<in> S. dist (f n x) (l x) < e)"
unfolding uniform_limit_iff eventually_sequentially ..
@@ -394,7 +407,7 @@
qed (metis uniformly_convergent_on_sum_E)
lemma uniform_limit_suminf:
- fixes f:: "nat \<Rightarrow> 'a::{metric_space, comm_monoid_add} \<Rightarrow> 'a"
+ fixes f:: "nat \<Rightarrow> 'a :: topological_space \<Rightarrow> 'b::{metric_space, comm_monoid_add}"
assumes "uniformly_convergent_on X (\<lambda>n x. \<Sum>k<n. f k x)"
shows "uniform_limit X (\<lambda>n x. \<Sum>k<n. f k x) (\<lambda>x. \<Sum>k. f k x) sequentially"
proof -
@@ -929,10 +942,6 @@
shows "uniform_limit (Union I) f g F"
by (metis SUP_identity_eq assms uniform_limit_on_UNION)
-lemma uniform_limit_on_subset:
- "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
- by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_mono)
-
lemma uniform_limit_bounded:
fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::metric_space"
assumes l: "uniform_limit S f l F"