--- 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)
--- 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>
--- 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}"
--- 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"
--- 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:
--- 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
--- 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"