# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1535642454 -7200
# Node ID f443ec10447da75b617294f84223cc6d3023ccfd
# Parent  9207ada0ca3164bb0a8257d7a7b4719598a837db
Some basic materials on filters and topology

diff -r 9207ada0ca31 -r f443ec10447d src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Thu Aug 30 19:59:36 2018 +0200
+++ b/src/HOL/Complete_Lattices.thy	Thu Aug 30 17:20:54 2018 +0200
@@ -236,6 +236,9 @@
 lemma INF_mono: "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<le> (\<Sqinter>n\<in>B. g n)"
   using Inf_mono [of "g ` B" "f ` A"] by auto
 
+lemma INF_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (INF x:A. f x) \<le> (INF x:A. g x)"
+  by (rule INF_mono) auto
+
 lemma Sup_mono:
   assumes "\<And>a. a \<in> A \<Longrightarrow> \<exists>b\<in>B. a \<le> b"
   shows "\<Squnion>A \<le> \<Squnion>B"
@@ -249,6 +252,9 @@
 lemma SUP_mono: "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<le> (\<Squnion>n\<in>B. g n)"
   using Sup_mono [of "f ` A" "g ` B"] by auto
 
+lemma SUP_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (SUP x:A. f x) \<le> (SUP x:A. g x)"
+  by (rule SUP_mono) auto
+
 lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>B. g x)"
   \<comment> \<open>The last inclusion is POSITIVE!\<close>
   by (blast intro: INF_mono dest: subsetD)
diff -r 9207ada0ca31 -r f443ec10447d src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Thu Aug 30 19:59:36 2018 +0200
+++ b/src/HOL/Filter.thy	Thu Aug 30 17:20:54 2018 +0200
@@ -522,6 +522,33 @@
 lemma eventually_INF1: "i \<in> I \<Longrightarrow> eventually P (F i) \<Longrightarrow> eventually P (\<Sqinter>i\<in>I. F i)"
   using filter_leD[OF INF_lower] .
 
+lemma eventually_INF_finite:
+  assumes "finite A"
+  shows   "eventually P (INF x:A. F x) \<longleftrightarrow>
+             (\<exists>Q. (\<forall>x\<in>A. eventually (Q x) (F x)) \<and> (\<forall>y. (\<forall>x\<in>A. Q x y) \<longrightarrow> P y))" 
+  using assms
+proof (induction arbitrary: P rule: finite_induct)
+  case (insert a A P)
+  from insert.hyps have [simp]: "x \<noteq> a" if "x \<in> A" for x
+    using that by auto
+  have "eventually P (INF x:insert a A. F x) \<longleftrightarrow>
+          (\<exists>Q R S. eventually Q (F a) \<and> (( (\<forall>x\<in>A. eventually (S x) (F x)) \<and>
+            (\<forall>y. (\<forall>x\<in>A. S x y) \<longrightarrow> R y)) \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x)))"
+    unfolding ex_simps by (simp add: eventually_inf insert.IH)
+  also have "\<dots> \<longleftrightarrow> (\<exists>Q. (\<forall>x\<in>insert a A. eventually (Q x) (F x)) \<and>
+                           (\<forall>y. (\<forall>x\<in>insert a A. Q x y) \<longrightarrow> P y))"
+  proof (safe, goal_cases)
+    case (1 Q R S)
+    thus ?case using 1 by (intro exI[of _ "S(a := Q)"]) auto
+  next
+    case (2 Q)
+    show ?case
+      by (rule exI[of _ "Q a"], rule exI[of _ "\<lambda>y. \<forall>x\<in>A. Q x y"],
+          rule exI[of _ "Q(a := (\<lambda>_. True))"]) (use 2 in auto)
+  qed
+  finally show ?case .
+qed auto
+
 subsubsection \<open>Map function for filters\<close>
 
 definition filtermap :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a filter \<Rightarrow> 'b filter"
@@ -653,6 +680,33 @@
   "filtercomap f (\<Squnion>b\<in>B. F b) \<ge> (\<Squnion>b\<in>B. filtercomap f (F b))"
   by (intro SUP_least filtercomap_mono SUP_upper)
 
+lemma filtermap_le_iff_le_filtercomap: "filtermap f F \<le> G \<longleftrightarrow> F \<le> filtercomap f G"
+  unfolding le_filter_def eventually_filtermap eventually_filtercomap
+  using eventually_mono by auto
+
+lemma filtercomap_neq_bot:
+  assumes "\<And>P. eventually P F \<Longrightarrow> \<exists>x. P (f x)"
+  shows   "filtercomap f F \<noteq> bot"
+  using assms by (auto simp: trivial_limit_def eventually_filtercomap)
+
+lemma filtercomap_neq_bot_surj:
+  assumes "F \<noteq> bot" and "surj f"
+  shows   "filtercomap f F \<noteq> bot"
+proof (rule filtercomap_neq_bot)
+  fix P assume *: "eventually P F"
+  show "\<exists>x. P (f x)"
+  proof (rule ccontr)
+    assume **: "\<not>(\<exists>x. P (f x))"
+    from * have "eventually (\<lambda>_. False) F"
+    proof eventually_elim
+      case (elim x)
+      from \<open>surj f\<close> obtain y where "x = f y" by auto
+      with elim and ** show False by auto
+    qed
+    with assms show False by (simp add: trivial_limit_def)
+  qed
+qed
+
 lemma eventually_filtercomapI [intro]:
   assumes "eventually P F"
   shows   "eventually (\<lambda>x. P (f x)) (filtercomap f F)"
@@ -858,6 +912,74 @@
 lemma filtermap_sequentually_ne_bot: "filtermap f sequentially \<noteq> bot"
   by (simp add: filtermap_bot_iff)
 
+subsection \<open>Increasing finite subsets\<close>
+
+definition finite_subsets_at_top where
+  "finite_subsets_at_top A = (INF X:{X. finite X \<and> X \<subseteq> A}. principal {Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A})"
+
+lemma eventually_finite_subsets_at_top:
+  "eventually P (finite_subsets_at_top A) \<longleftrightarrow>
+     (\<exists>X. finite X \<and> X \<subseteq> A \<and> (\<forall>Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A \<longrightarrow> P Y))"
+  unfolding finite_subsets_at_top_def
+proof (subst eventually_INF_base, goal_cases)
+  show "{X. finite X \<and> X \<subseteq> A} \<noteq> {}" by auto
+next
+  case (2 B C)
+  thus ?case by (intro bexI[of _ "B \<union> C"]) auto
+qed (simp_all add: eventually_principal)
+
+lemma eventually_finite_subsets_at_top_weakI [intro]:
+  assumes "\<And>X. finite X \<Longrightarrow> X \<subseteq> A \<Longrightarrow> P X"
+  shows   "eventually P (finite_subsets_at_top A)"
+proof -
+  have "eventually (\<lambda>X. finite X \<and> X \<subseteq> A) (finite_subsets_at_top A)"
+    by (auto simp: eventually_finite_subsets_at_top)
+  thus ?thesis by eventually_elim (use assms in auto)
+qed
+
+lemma finite_subsets_at_top_neq_bot [simp]: "finite_subsets_at_top A \<noteq> bot"
+proof -
+  have "\<not>eventually (\<lambda>x. False) (finite_subsets_at_top A)"
+    by (auto simp: eventually_finite_subsets_at_top)
+  thus ?thesis by auto
+qed
+
+lemma filtermap_image_finite_subsets_at_top:
+  assumes "inj_on f A"
+  shows   "filtermap ((`) f) (finite_subsets_at_top A) = finite_subsets_at_top (f ` A)"
+  unfolding filter_eq_iff eventually_filtermap
+proof (safe, goal_cases)
+  case (1 P)
+  then obtain X where X: "finite X" "X \<subseteq> A" "\<And>Y. finite Y \<Longrightarrow> X \<subseteq> Y \<Longrightarrow> Y \<subseteq> A \<Longrightarrow> P (f ` Y)"
+    unfolding eventually_finite_subsets_at_top by force
+  show ?case unfolding eventually_finite_subsets_at_top eventually_filtermap
+  proof (rule exI[of _ "f ` X"], intro conjI allI impI, goal_cases)
+    case (3 Y)
+    with assms and X(1,2) have "P (f ` (f -` Y \<inter> A))" using X(1,2)
+      by (intro X(3) finite_vimage_IntI) auto
+    also have "f ` (f -` Y \<inter> A) = Y" using assms 3 by blast
+    finally show ?case .
+  qed (insert assms X(1,2), auto intro!: finite_vimage_IntI)
+next
+  case (2 P)
+  then obtain X where X: "finite X" "X \<subseteq> f ` A" "\<And>Y. finite Y \<Longrightarrow> X \<subseteq> Y \<Longrightarrow> Y \<subseteq> f ` A \<Longrightarrow> P Y"
+    unfolding eventually_finite_subsets_at_top by force
+  show ?case unfolding eventually_finite_subsets_at_top eventually_filtermap
+  proof (rule exI[of _ "f -` X \<inter> A"], intro conjI allI impI, goal_cases)
+    case (3 Y)
+    with X(1,2) and assms show ?case by (intro X(3)) force+
+  qed (insert assms X(1), auto intro!: finite_vimage_IntI)
+qed
+
+lemma eventually_finite_subsets_at_top_finite:
+  assumes "finite A"
+  shows   "eventually P (finite_subsets_at_top A) \<longleftrightarrow> P A"
+  unfolding eventually_finite_subsets_at_top using assms by force
+
+lemma finite_subsets_at_top_finite: "finite A \<Longrightarrow> finite_subsets_at_top A = principal {A}"
+  by (auto simp: filter_eq_iff eventually_finite_subsets_at_top_finite eventually_principal)
+
+
 subsection \<open>The cofinite filter\<close>
 
 definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
@@ -1208,6 +1330,9 @@
   "(LIM x F. f x :> principal S) \<longleftrightarrow> (eventually (\<lambda>x. f x \<in> S) F)"
   unfolding filterlim_def eventually_filtermap le_principal ..
 
+lemma filterlim_filtercomap [intro]: "filterlim f F (filtercomap f F)"
+  unfolding filterlim_def by (rule filtermap_filtercomap)
+
 lemma filterlim_inf:
   "(LIM x F1. f x :> inf F2 F3) \<longleftrightarrow> ((LIM x F1. f x :> F2) \<and> (LIM x F1. f x :> F3))"
   unfolding filterlim_def by simp
@@ -1220,6 +1345,15 @@
   "(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (\<Sqinter>i\<in>I. F i). f x :> (\<Sqinter>j\<in>J. G j)"
   unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
 
+lemma filterlim_INF': "x \<in> A \<Longrightarrow> filterlim f F (G x) \<Longrightarrow> filterlim f F (INF x:A. G x)"
+  unfolding filterlim_def by (rule order.trans[OF filtermap_mono[OF INF_lower]])
+
+lemma filterlim_filtercomap_iff: "filterlim f (filtercomap g G) F \<longleftrightarrow> filterlim (g \<circ> f) G F"
+  by (simp add: filterlim_def filtermap_le_iff_le_filtercomap filtercomap_filtercomap o_def)
+
+lemma filterlim_iff_le_filtercomap: "filterlim f F G \<longleftrightarrow> G \<le> filtercomap f F"
+  by (simp add: filterlim_def filtermap_le_iff_le_filtercomap)
+
 lemma filterlim_base:
   "(\<And>m x. m \<in> J \<Longrightarrow> i m \<in> I) \<Longrightarrow> (\<And>m x. m \<in> J \<Longrightarrow> x \<in> F (i m) \<Longrightarrow> f x \<in> G m) \<Longrightarrow>
     LIM x (\<Sqinter>i\<in>I. principal (F i)). f x :> (\<Sqinter>j\<in>J. principal (G j))"
@@ -1347,9 +1481,51 @@
   shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
   by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
     
-lemma filterlim_filtercomap [intro]: "filterlim f F (filtercomap f F)"
-  unfolding filterlim_def by (rule filtermap_filtercomap)
+lemma filterlim_finite_subsets_at_top:
+  "filterlim f (finite_subsets_at_top A) F \<longleftrightarrow>
+     (\<forall>X. finite X \<and> X \<subseteq> A \<longrightarrow> eventually (\<lambda>y. finite (f y) \<and> X \<subseteq> f y \<and> f y \<subseteq> A) F)"
+  (is "?lhs = ?rhs")
+proof 
+  assume ?lhs
+  thus ?rhs
+  proof (safe, goal_cases)
+    case (1 X)
+    hence *: "(\<forall>\<^sub>F x in F. P (f x))" if "eventually P (finite_subsets_at_top A)" for P
+      using that by (auto simp: filterlim_def le_filter_def eventually_filtermap)
+    have "\<forall>\<^sub>F Y in finite_subsets_at_top A. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A"
+      using 1 unfolding eventually_finite_subsets_at_top by force
+    thus ?case by (intro *) auto
+  qed
+next
+  assume rhs: ?rhs
+  show ?lhs unfolding filterlim_def le_filter_def eventually_finite_subsets_at_top
+  proof (safe, goal_cases)
+    case (1 P X)
+    with rhs have "\<forall>\<^sub>F y in F. finite (f y) \<and> X \<subseteq> f y \<and> f y \<subseteq> A" by auto
+    thus "eventually P (filtermap f F)" unfolding eventually_filtermap
+      by eventually_elim (insert 1, auto)
+  qed
+qed
 
+lemma filterlim_atMost_at_top:
+  "filterlim (\<lambda>n. {..n}) (finite_subsets_at_top (UNIV :: nat set)) at_top"
+  unfolding filterlim_finite_subsets_at_top
+proof (safe, goal_cases)
+  case (1 X)
+  then obtain n where n: "X \<subseteq> {..n}" by (auto simp: finite_nat_set_iff_bounded_le)
+  show ?case using eventually_ge_at_top[of n]
+    by eventually_elim (insert n, auto)
+qed
+
+lemma filterlim_lessThan_at_top:
+  "filterlim (\<lambda>n. {..<n}) (finite_subsets_at_top (UNIV :: nat set)) at_top"
+  unfolding filterlim_finite_subsets_at_top
+proof (safe, goal_cases)
+  case (1 X)
+  then obtain n where n: "X \<subseteq> {..<n}" by (auto simp: finite_nat_set_iff_bounded)
+  show ?case using eventually_ge_at_top[of n]
+    by eventually_elim (insert n, auto)
+qed
 
 subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
 
diff -r 9207ada0ca31 -r f443ec10447d src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Thu Aug 30 19:59:36 2018 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Thu Aug 30 17:20:54 2018 +0200
@@ -69,6 +69,11 @@
   then show thesis ..
 qed
 
+lemma countable_infiniteE':
+  assumes "countable A" "infinite A"
+  obtains g where "bij_betw g (UNIV :: nat set) A"
+  using bij_betw_inv[OF countableE_infinite[OF assms]] that by blast
+
 lemma countable_enum_cases:
   assumes "countable S"
   obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"
diff -r 9207ada0ca31 -r f443ec10447d src/HOL/Library/Liminf_Limsup.thy
--- a/src/HOL/Library/Liminf_Limsup.thy	Thu Aug 30 19:59:36 2018 +0200
+++ b/src/HOL/Library/Liminf_Limsup.thy	Thu Aug 30 17:20:54 2018 +0200
@@ -71,6 +71,11 @@
   shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
   by (rule antisym) (auto intro!: INF_greatest INF_lower2)
 
+lemma INF_Sigma:
+  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
+  shows "(INF i : A. INF j : B i. f i j) = (INF p : Sigma A B. f (fst p) (snd p))"
+  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
+
 subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
 
 definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
@@ -202,7 +207,7 @@
 lemma le_Limsup:
   assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. l \<le> f x"
   shows "l \<le> Limsup F f"
-  using F Liminf_bounded Liminf_le_Limsup order.trans x by blast
+  using F Liminf_bounded[of l f F] Liminf_le_Limsup[of F f] order.trans x by blast
 
 lemma Liminf_le:
   assumes F: "F \<noteq> bot" and x: "\<forall>\<^sub>F x in F. f x \<le> l"
diff -r 9207ada0ca31 -r f443ec10447d src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Aug 30 19:59:36 2018 +0200
+++ b/src/HOL/Limits.thy	Thu Aug 30 17:20:54 2018 +0200
@@ -876,6 +876,91 @@
     and tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto
 
 
+class topological_monoid_mult = topological_semigroup_mult + monoid_mult
+class topological_comm_monoid_mult = topological_monoid_mult + comm_monoid_mult
+
+lemma tendsto_power_strong [tendsto_intros]:
+  fixes f :: "_ \<Rightarrow> 'b :: topological_monoid_mult"
+  assumes "(f \<longlongrightarrow> a) F" "(g \<longlongrightarrow> b) F"
+  shows   "((\<lambda>x. f x ^ g x) \<longlongrightarrow> a ^ b) F"
+proof -
+  have "((\<lambda>x. f x ^ b) \<longlongrightarrow> a ^ b) F"
+    by (induction b) (auto intro: tendsto_intros assms)
+  also from assms(2) have "eventually (\<lambda>x. g x = b) F"
+    by (simp add: nhds_discrete filterlim_principal)
+  hence "eventually (\<lambda>x. f x ^ b = f x ^ g x) F"
+    by eventually_elim simp
+  hence "((\<lambda>x. f x ^ b) \<longlongrightarrow> a ^ b) F \<longleftrightarrow> ((\<lambda>x. f x ^ g x) \<longlongrightarrow> a ^ b) F"
+    by (intro filterlim_cong refl)
+  finally show ?thesis .
+qed
+
+lemma continuous_mult' [continuous_intros]:
+  fixes f g :: "_ \<Rightarrow> 'b::topological_semigroup_mult"
+  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x * g x)"
+  unfolding continuous_def by (rule tendsto_mult)
+
+lemma continuous_power' [continuous_intros]:
+  fixes f :: "_ \<Rightarrow> 'b::topological_monoid_mult"
+  shows "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. f x ^ g x)"
+  unfolding continuous_def by (rule tendsto_power_strong) auto
+
+lemma continuous_on_mult' [continuous_intros]:
+  fixes f g :: "_ \<Rightarrow> 'b::topological_semigroup_mult"
+  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x * g x)"
+  unfolding continuous_on_def by (auto intro: tendsto_mult)
+
+lemma continuous_on_power' [continuous_intros]:
+  fixes f :: "_ \<Rightarrow> 'b::topological_monoid_mult"
+  shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. f x ^ g x)"
+  unfolding continuous_on_def by (auto intro: tendsto_power_strong)
+
+lemma tendsto_mult_one:
+  fixes f g :: "_ \<Rightarrow> 'b::topological_monoid_mult"
+  shows "(f \<longlongrightarrow> 1) F \<Longrightarrow> (g \<longlongrightarrow> 1) F \<Longrightarrow> ((\<lambda>x. f x * g x) \<longlongrightarrow> 1) F"
+  by (drule (1) tendsto_mult) simp
+
+lemma tendsto_prod' [tendsto_intros]:
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_mult"
+  shows "(\<And>i. i \<in> I \<Longrightarrow> (f i \<longlongrightarrow> a i) F) \<Longrightarrow> ((\<lambda>x. \<Prod>i\<in>I. f i x) \<longlongrightarrow> (\<Prod>i\<in>I. a i)) F"
+  by (induct I rule: infinite_finite_induct) (simp_all add: tendsto_mult)
+
+lemma tendsto_one_prod':
+  fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::topological_comm_monoid_mult"
+  assumes "\<And>i. i \<in> I \<Longrightarrow> ((\<lambda>x. f x i) \<longlongrightarrow> 1) F"
+  shows "((\<lambda>i. prod (f i) I) \<longlongrightarrow> 1) F"
+  using tendsto_prod' [of I "\<lambda>x y. f y x" "\<lambda>x. 1"] assms by simp
+
+lemma continuous_prod' [continuous_intros]:
+  fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::topological_comm_monoid_mult"
+  shows "(\<And>i. i \<in> I \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>I. f i x)"
+  unfolding continuous_def by (rule tendsto_prod')
+
+lemma continuous_on_prod' [continuous_intros]:
+  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::topological_comm_monoid_mult"
+  shows "(\<And>i. i \<in> I \<Longrightarrow> continuous_on S (f i)) \<Longrightarrow> continuous_on S (\<lambda>x. \<Prod>i\<in>I. f i x)"
+  unfolding continuous_on_def by (auto intro: tendsto_prod')
+
+instance nat :: topological_comm_monoid_mult
+  by standard
+    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)
+
+instance int :: topological_comm_monoid_mult
+  by standard
+    (simp add: nhds_discrete principal_prod_principal filterlim_principal eventually_principal)
+
+class comm_real_normed_algebra_1 = real_normed_algebra_1 + comm_monoid_mult
+
+context real_normed_field
+begin
+
+subclass comm_real_normed_algebra_1
+proof
+  from norm_mult[of "1 :: 'a" 1] show "norm 1 = 1" by simp 
+qed (simp_all add: norm_mult)
+
+end
+
 subsubsection \<open>Inverse and division\<close>
 
 lemma (in bounded_bilinear) Zfun_prod_Bfun:
diff -r 9207ada0ca31 -r f443ec10447d src/HOL/Series.thy
--- a/src/HOL/Series.thy	Thu Aug 30 19:59:36 2018 +0200
+++ b/src/HOL/Series.thy	Thu Aug 30 17:20:54 2018 +0200
@@ -335,6 +335,18 @@
 
 end
 
+lemma sums_If_finite_set':
+  fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_ab_group_add}"
+  assumes "g sums S" and "finite A" and "S' = S + (\<Sum>n\<in>A. f n - g n)"
+  shows   "(\<lambda>n. if n \<in> A then f n else g n) sums S'"
+proof -
+  have "(\<lambda>n. g n + (if n \<in> A then f n - g n else 0)) sums (S + (\<Sum>n\<in>A. f n - g n))"
+    by (intro sums_add assms sums_If_finite_set)
+  also have "(\<lambda>n. g n + (if n \<in> A then f n - g n else 0)) = (\<lambda>n. if n \<in> A then f n else g n)"
+    by (simp add: fun_eq_iff)
+  finally show ?thesis using assms by simp
+qed
+
 subsection \<open>Infinite summability on real normed vector spaces\<close>
 
 context
diff -r 9207ada0ca31 -r f443ec10447d src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Aug 30 19:59:36 2018 +0200
+++ b/src/HOL/Topological_Spaces.thy	Thu Aug 30 17:20:54 2018 +0200
@@ -512,6 +512,10 @@
 lemma (in discrete_topology) at_discrete: "at x within S = bot"
   unfolding at_within_def nhds_discrete by simp
 
+lemma (in discrete_topology) tendsto_discrete:
+  "filterlim (f :: 'b \<Rightarrow> 'a) (nhds y) F \<longleftrightarrow> eventually (\<lambda>x. f x = y) F"
+  by (auto simp: nhds_discrete filterlim_principal)
+
 lemma (in topological_space) at_within_eq:
   "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
   unfolding nhds_def at_within_def
@@ -881,6 +885,36 @@
   shows "((\<lambda>x. a) \<longlongrightarrow> b) F \<longleftrightarrow> a = b"
   by (auto intro!: tendsto_unique [OF assms tendsto_const])
 
+lemma Lim_in_closed_set:
+  assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) F" "F \<noteq> bot" "(f \<longlongrightarrow> l) F"
+  shows "l \<in> S"
+proof (rule ccontr)
+  assume "l \<notin> S"
+  with \<open>closed S\<close> have "open (- S)" "l \<in> - S"
+    by (simp_all add: open_Compl)
+  with assms(4) have "eventually (\<lambda>x. f x \<in> - S) F"
+    by (rule topological_tendstoD)
+  with assms(2) have "eventually (\<lambda>x. False) F"
+    by (rule eventually_elim2) simp
+  with assms(3) show "False"
+    by (simp add: eventually_False)
+qed
+
+lemma (in t3_space) nhds_closed:
+  assumes "x \<in> A" and "open A"
+  shows   "\<exists>A'. x \<in> A' \<and> closed A' \<and> A' \<subseteq> A \<and> eventually (\<lambda>y. y \<in> A') (nhds x)"
+proof -
+  from assms have "\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> - A \<subseteq> V \<and> U \<inter> V = {}"
+    by (intro t3_space) auto
+  then obtain U V where UV: "open U" "open V" "x \<in> U" "-A \<subseteq> V" "U \<inter> V = {}"
+    by auto
+  have "eventually (\<lambda>y. y \<in> U) (nhds x)"
+    using \<open>open U\<close> and \<open>x \<in> U\<close> by (intro eventually_nhds_in_open)
+  hence "eventually (\<lambda>y. y \<in> -V) (nhds x)"
+    by eventually_elim (use UV in auto)
+  with UV show ?thesis by (intro exI[of _ "-V"]) auto
+qed
+
 lemma (in order_topology) increasing_tendsto:
   assumes bdd: "eventually (\<lambda>n. f n \<le> l) F"
     and en: "\<And>x. x < l \<Longrightarrow> eventually (\<lambda>n. x < f n) F"
@@ -2082,6 +2116,9 @@
   by (auto simp: at_within_Icc_at_right at_within_Icc_at_left continuous_on_def
       dest: bspec[where x=a] bspec[where x=b])
 
+lemma continuous_on_discrete [simp, continuous_intros]:
+  "continuous_on A (f :: 'a :: discrete_topology \<Rightarrow> _)"
+  by (auto simp: continuous_on_def at_discrete)
 
 subsubsection \<open>Continuity at a point\<close>
 
@@ -2125,6 +2162,10 @@
   "continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. continuous (at x within s) f)"
   unfolding continuous_on_def continuous_within ..
 
+lemma continuous_discrete [simp, continuous_intros]:
+  "continuous (at x within A) (f :: 'a :: discrete_topology \<Rightarrow> _)"
+  by (auto simp: continuous_def at_discrete)
+
 abbreviation isCont :: "('a::t2_space \<Rightarrow> 'b::topological_space) \<Rightarrow> 'a \<Rightarrow> bool"
   where "isCont f a \<equiv> continuous (at a) f"