--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Abstract_Limits.thy Thu Mar 07 14:08:05 2019 +0000
@@ -0,0 +1,296 @@
+theory Abstract_Limits
+ imports
+ Abstract_Topology
+begin
+
+subsection\<open>nhdsin and atin\<close>
+
+definition nhdsin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
+ where "nhdsin X a =
+ (if a \<in> topspace X then (INF S:{S. openin X S \<and> a \<in> S}. principal S) else bot)"
+
+definition atin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
+ where "atin X a \<equiv> inf (nhdsin X a) (principal (topspace X - {a}))"
+
+
+lemma nhdsin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> nhdsin X a = bot"
+ and atin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> atin X a = bot"
+ by (simp_all add: nhdsin_def atin_def)
+
+lemma eventually_nhdsin:
+ "eventually P (nhdsin X a) \<longleftrightarrow> a \<notin> topspace X \<or> (\<exists>S. openin X S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
+proof (cases "a \<in> topspace X")
+ case True
+ hence "nhdsin X a = (INF S:{S. openin X S \<and> a \<in> S}. principal S)"
+ by (simp add: nhdsin_def)
+ also have "eventually P \<dots> \<longleftrightarrow> (\<exists>S. openin X S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
+ using True by (subst eventually_INF_base) (auto simp: eventually_principal)
+ finally show ?thesis using True by simp
+qed auto
+
+lemma eventually_atin:
+ "eventually P (atin X a) \<longleftrightarrow> a \<notin> topspace X \<or>
+ (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
+proof (cases "a \<in> topspace X")
+ case True
+ hence "eventually P (atin X a) \<longleftrightarrow> (\<exists>S. openin X S \<and>
+ a \<in> S \<and> (\<forall>x\<in>S. x \<in> topspace X \<and> x \<noteq> a \<longrightarrow> P x))"
+ by (simp add: atin_def eventually_inf_principal eventually_nhdsin)
+ also have "\<dots> \<longleftrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
+ using openin_subset by (intro ex_cong) auto
+ finally show ?thesis by (simp add: True)
+qed auto
+
+
+subsection\<open>Limits in a topological space\<close>
+
+definition limit :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
+ "limit X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
+
+lemma limit_euclideanreal_iff [simp]: "limit euclideanreal f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
+ by (auto simp: limit_def tendsto_def)
+
+lemma limit_in_topspace: "limit X f l F \<Longrightarrow> l \<in> topspace X"
+ by (simp add: limit_def)
+
+lemma limit_const: "limit X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
+ by (simp add: limit_def)
+
+lemma limit_real_const: "limit euclideanreal (\<lambda>a. l) l F"
+ by (simp add: limit_def)
+
+lemma limit_eventually:
+ "\<lbrakk>l \<in> topspace X; eventually (\<lambda>x. f x = l) F\<rbrakk> \<Longrightarrow> limit X f l F"
+ by (auto simp: limit_def eventually_mono)
+
+lemma limit_subsequence:
+ "\<lbrakk>strict_mono r; limit X f l sequentially\<rbrakk> \<Longrightarrow> limit X (f \<circ> r) l sequentially"
+ unfolding limit_def using eventually_subseq by fastforce
+
+lemma limit_subtopology:
+ "limit (subtopology X S) f l F
+ \<longleftrightarrow> l \<in> S \<and> eventually (\<lambda>a. f a \<in> S) F \<and> limit X f l F" (is "?lhs = ?rhs")
+proof (cases "l \<in> S \<inter> topspace X")
+ case True
+ show ?thesis
+ proof
+ assume L: ?lhs
+ with True
+ have "\<forall>\<^sub>F b in F. f b \<in> topspace X \<inter> S"
+ by (metis (no_types) limit_def openin_topspace topspace_subtopology)
+ with L show ?rhs
+ apply (clarsimp simp add: limit_def eventually_mono topspace_subtopology openin_subtopology_alt)
+ apply (drule_tac x="S \<inter> U" in spec, force simp: elim: eventually_mono)
+ done
+ next
+ assume ?rhs
+ then show ?lhs
+ using eventually_elim2
+ by (fastforce simp add: limit_def topspace_subtopology openin_subtopology_alt)
+ qed
+qed (auto simp: limit_def topspace_subtopology)
+
+
+lemma limit_sequentially:
+ "limit X S l sequentially \<longleftrightarrow>
+ l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> (\<exists>N. \<forall>n. N \<le> n \<longrightarrow> S n \<in> U))"
+ by (simp add: limit_def eventually_sequentially)
+
+lemma limit_sequentially_offset:
+ "limit X f l sequentially \<Longrightarrow> limit X (\<lambda>i. f (i + k)) l sequentially"
+ unfolding limit_sequentially
+ by (metis add.commute le_add2 order_trans)
+
+lemma limit_sequentially_offset_rev:
+ assumes "limit X (\<lambda>i. f (i + k)) l sequentially"
+ shows "limit X f l sequentially"
+proof -
+ have "\<exists>N. \<forall>n\<ge>N. f n \<in> U" if U: "openin X U" "l \<in> U" for U
+ proof -
+ obtain N where "\<And>n. n\<ge>N \<Longrightarrow> f (n + k) \<in> U"
+ using assms U unfolding limit_sequentially by blast
+ then have "\<forall>n\<ge>N+k. f n \<in> U"
+ by (metis add_leD2 le_add_diff_inverse ordered_cancel_comm_monoid_diff_class.le_diff_conv2 add.commute)
+ then show ?thesis ..
+ qed
+ with assms show ?thesis
+ unfolding limit_sequentially
+ by simp
+qed
+
+lemma limit_atin:
+ "limit Y f y (atin X x) \<longleftrightarrow>
+ y \<in> topspace Y \<and>
+ (x \<in> topspace X
+ \<longrightarrow> (\<forall>V. openin Y V \<and> y \<in> V
+ \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> f ` (U - {x}) \<subseteq> V)))"
+ by (auto simp: limit_def eventually_atin image_subset_iff)
+
+lemma limit_atin_self:
+ "limit Y f (f a) (atin X a) \<longleftrightarrow>
+ f a \<in> topspace Y \<and>
+ (a \<in> topspace X
+ \<longrightarrow> (\<forall>V. openin Y V \<and> f a \<in> V
+ \<longrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> f ` U \<subseteq> V)))"
+ unfolding limit_atin by fastforce
+
+lemma limit_trivial:
+ "\<lbrakk>trivial_limit F; y \<in> topspace X\<rbrakk> \<Longrightarrow> limit X f y F"
+ by (simp add: limit_def)
+
+lemma limit_transform_eventually:
+ "\<lbrakk>eventually (\<lambda>x. f x = g x) F; limit X f l F\<rbrakk> \<Longrightarrow> limit X g l F"
+ unfolding limit_def using eventually_elim2 by fastforce
+
+lemma continuous_map_limit:
+ assumes "continuous_map X Y g" and f: "limit X f l F"
+ shows "limit Y (g \<circ> f) (g l) F"
+proof -
+ have "g l \<in> topspace Y"
+ by (meson assms continuous_map_def limit_in_topspace)
+ moreover
+ have "\<And>U. \<lbrakk>\<forall>V. openin X V \<and> l \<in> V \<longrightarrow> (\<forall>\<^sub>F x in F. f x \<in> V); openin Y U; g l \<in> U\<rbrakk>
+ \<Longrightarrow> \<forall>\<^sub>F x in F. g (f x) \<in> U"
+ using assms eventually_mono
+ by (fastforce simp: limit_def dest!: openin_continuous_map_preimage)
+ ultimately show ?thesis
+ using f by (fastforce simp add: limit_def)
+qed
+
+
+subsection\<open>Pointwise continuity in topological spaces\<close>
+
+definition topcontinuous_at where
+ "topcontinuous_at X Y f x \<longleftrightarrow>
+ x \<in> topspace X \<and>
+ (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+ (\<forall>V. openin Y V \<and> f x \<in> V
+ \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y \<in> U. f y \<in> V)))"
+
+lemma topcontinuous_at_atin:
+ "topcontinuous_at X Y f x \<longleftrightarrow>
+ x \<in> topspace X \<and>
+ (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
+ limit Y f (f x) (atin X x)"
+ unfolding topcontinuous_at_def
+ by (fastforce simp add: limit_atin)+
+
+lemma continuous_map_eq_topcontinuous_at:
+ "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. topcontinuous_at X Y f x)"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then show ?rhs
+ by (auto simp: continuous_map_def topcontinuous_at_def)
+next
+ assume R: ?rhs
+ then show ?lhs
+ apply (auto simp: continuous_map_def topcontinuous_at_def)
+ apply (subst openin_subopen, safe)
+ apply (drule bspec, assumption)
+ using openin_subset[of X] apply (auto simp: subset_iff dest!: spec)
+ done
+qed
+
+lemma continuous_map_atin:
+ "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. limit Y f (f x) (atin X x))"
+ by (auto simp: limit_def topcontinuous_at_atin continuous_map_eq_topcontinuous_at)
+
+lemma limit_continuous_map:
+ "\<lbrakk>continuous_map X Y f; a \<in> topspace X; f a = b\<rbrakk> \<Longrightarrow> limit Y f b (atin X a)"
+ by (auto simp: continuous_map_atin)
+
+
+subsection\<open>Combining theorems for continuous functions into the reals\<close>
+
+lemma continuous_map_real_const [simp,continuous_intros]:
+ "continuous_map X euclideanreal (\<lambda>x. c)"
+ by simp
+
+lemma continuous_map_real_mult [continuous_intros]:
+ "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
+ \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x * g x)"
+ by (simp add: continuous_map_atin tendsto_mult)
+
+lemma continuous_map_real_pow [continuous_intros]:
+ "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x ^ n)"
+ by (induction n) (auto simp: continuous_map_real_mult)
+
+lemma continuous_map_real_mult_left:
+ "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. c * f x)"
+ by (simp add: continuous_map_atin tendsto_mult)
+
+lemma continuous_map_real_mult_left_eq:
+ "continuous_map X euclideanreal (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> continuous_map X euclideanreal f"
+proof (cases "c = 0")
+ case False
+ have "continuous_map X euclideanreal (\<lambda>x. c * f x) \<Longrightarrow> continuous_map X euclideanreal f"
+ apply (frule continuous_map_real_mult_left [where c="inverse c"])
+ apply (simp add: field_simps False)
+ done
+ with False show ?thesis
+ using continuous_map_real_mult_left by blast
+qed simp
+
+lemma continuous_map_real_mult_right:
+ "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x * c)"
+ by (simp add: continuous_map_atin tendsto_mult)
+
+lemma continuous_map_real_mult_right_eq:
+ "continuous_map X euclideanreal (\<lambda>x. f x * c) \<longleftrightarrow> c = 0 \<or> continuous_map X euclideanreal f"
+ by (simp add: mult.commute flip: continuous_map_real_mult_left_eq)
+
+lemma continuous_map_real_minus [continuous_intros]:
+ "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. - f x)"
+ by (simp add: continuous_map_atin tendsto_minus)
+
+lemma continuous_map_real_minus_eq:
+ "continuous_map X euclideanreal (\<lambda>x. - f x) \<longleftrightarrow> continuous_map X euclideanreal f"
+ using continuous_map_real_mult_left_eq [where c = "-1"] by auto
+
+lemma continuous_map_real_add [continuous_intros]:
+ "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
+ \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x + g x)"
+ by (simp add: continuous_map_atin tendsto_add)
+
+lemma continuous_map_real_diff [continuous_intros]:
+ "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
+ \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x - g x)"
+ by (simp add: continuous_map_atin tendsto_diff)
+
+lemma continuous_map_real_abs [continuous_intros]:
+ "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. abs(f x))"
+ by (simp add: continuous_map_atin tendsto_rabs)
+
+lemma continuous_map_real_max [continuous_intros]:
+ "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
+ \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. max (f x) (g x))"
+ by (simp add: continuous_map_atin tendsto_max)
+
+lemma continuous_map_real_min [continuous_intros]:
+ "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
+ \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. min (f x) (g x))"
+ by (simp add: continuous_map_atin tendsto_min)
+
+lemma continuous_map_sum [continuous_intros]:
+ "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)\<rbrakk>
+ \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sum (f x) I)"
+ by (simp add: continuous_map_atin tendsto_sum)
+
+lemma continuous_map_prod [continuous_intros]:
+ "\<lbrakk>finite I;
+ \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)\<rbrakk>
+ \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. prod (f x) I)"
+ by (simp add: continuous_map_atin tendsto_prod)
+
+lemma continuous_map_real_inverse [continuous_intros]:
+ "\<lbrakk>continuous_map X euclideanreal f; \<And>x. x \<in> topspace X \<Longrightarrow> f x \<noteq> 0\<rbrakk>
+ \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. inverse(f x))"
+ by (simp add: continuous_map_atin tendsto_inverse)
+
+lemma continuous_map_real_divide [continuous_intros]:
+ "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g; \<And>x. x \<in> topspace X \<Longrightarrow> g x \<noteq> 0\<rbrakk>
+ \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x / g x)"
+ by (simp add: continuous_map_atin tendsto_divide)
+
+end
--- a/src/HOL/Analysis/Abstract_Topology.thy Wed Mar 06 21:44:30 2019 +0100
+++ b/src/HOL/Analysis/Abstract_Topology.thy Thu Mar 07 14:08:05 2019 +0000
@@ -290,7 +290,7 @@
lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)"
by (force simp: relative_to_def openin_subtopology)
-lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
+lemma topspace_subtopology [simp]: "topspace (subtopology U V) = topspace U \<inter> V"
by (auto simp: topspace_def openin_subtopology)
lemma topspace_subtopology_subset:
@@ -597,7 +597,7 @@
{x \<in> topspace X.
(\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))}"
-lemma derived_set_of_restrict:
+lemma derived_set_of_restrict [simp]:
"X derived_set_of (topspace X \<inter> S) = X derived_set_of S"
by (simp add: derived_set_of_def) (metis openin_subset subset_iff)
@@ -624,7 +624,7 @@
"S \<subseteq> T \<Longrightarrow> X derived_set_of S \<subseteq> X derived_set_of T"
unfolding derived_set_of_def by blast
-lemma derived_set_of_union:
+lemma derived_set_of_Un:
"X derived_set_of (S \<union> T) = X derived_set_of S \<union> X derived_set_of T" (is "?lhs = ?rhs")
proof
show "?lhs \<subseteq> ?rhs"
@@ -634,12 +634,12 @@
by (simp add: derived_set_of_mono)
qed
-lemma derived_set_of_unions:
+lemma derived_set_of_Union:
"finite \<F> \<Longrightarrow> X derived_set_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X derived_set_of S)"
proof (induction \<F> rule: finite_induct)
case (insert S \<F>)
then show ?case
- by (simp add: derived_set_of_union)
+ by (simp add: derived_set_of_Un)
qed auto
lemma derived_set_of_topspace:
@@ -745,7 +745,7 @@
by auto (meson closure_of_mono inf_mono subset_iff)
lemma closure_of_Un [simp]: "X closure_of (S \<union> T) = X closure_of S \<union> X closure_of T"
- by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_union inf_sup_distrib1)
+ by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_Un inf_sup_distrib1)
lemma closure_of_Union:
"finite \<F> \<Longrightarrow> X closure_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X closure_of S)"
@@ -1545,6 +1545,26 @@
lemma continuous_map_iff_continuous_real [simp]: "continuous_map (subtopology euclideanreal S) euclideanreal g = continuous_on S g"
by (force simp: continuous_map openin_subtopology continuous_on_open_invariant)
+lemma continuous_map_iff_continuous_real2 [simp]: "continuous_map euclideanreal euclideanreal g = continuous_on UNIV g"
+ by (metis continuous_map_iff_continuous_real subtopology_UNIV)
+
+lemma continuous_map_openin_preimage_eq:
+ "continuous_map X Y f \<longleftrightarrow>
+ f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X (topspace X \<inter> f -` U))"
+ by (auto simp: continuous_map_def vimage_def Int_def)
+
+lemma continuous_map_closedin_preimage_eq:
+ "continuous_map X Y f \<longleftrightarrow>
+ f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. closedin Y U \<longrightarrow> closedin X (topspace X \<inter> f -` U))"
+ by (auto simp: continuous_map_closedin vimage_def Int_def)
+
+lemma continuous_map_square_root: "continuous_map euclideanreal euclideanreal sqrt"
+ by (simp add: continuous_at_imp_continuous_on isCont_real_sqrt)
+
+lemma continuous_map_sqrt [continuous_intros]:
+ "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sqrt(f x))"
+ by (meson continuous_map_compose continuous_map_eq continuous_map_square_root o_apply)
+
lemma continuous_map_id [simp]: "continuous_map X X id"
unfolding continuous_map_def using openin_subopen topspace_def by fastforce
--- a/src/HOL/Analysis/Analysis.thy Wed Mar 06 21:44:30 2019 +0100
+++ b/src/HOL/Analysis/Analysis.thy Thu Mar 07 14:08:05 2019 +0000
@@ -5,6 +5,7 @@
Determinants
(* Topology *)
Connected
+ Abstract_Limits
(* Functional Analysis *)
Elementary_Normed_Spaces
Norm_Arith
@@ -27,6 +28,7 @@
Bounded_Continuous_Function
Abstract_Topology
Function_Topology
+ T1_Spaces
Infinite_Products
Infinite_Set_Sum
Weierstrass_Theorems
--- a/src/HOL/Analysis/Function_Topology.thy Wed Mar 06 21:44:30 2019 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Thu Mar 07 14:08:05 2019 +0000
@@ -546,7 +546,7 @@
done
qed
-lemma topspace_product_topology:
+lemma topspace_product_topology [simp]:
"topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
proof
show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
@@ -700,21 +700,101 @@
by meson
qed
-
-lemma topspace_product_topology_alt:
- "topspace (product_topology Y I) = {f \<in> extensional I. \<forall>k \<in> I. f k \<in> topspace(Y k)}"
- by (force simp: product_topology PiE_def)
+lemma closure_of_product_topology:
+ "(product_topology X I) closure_of (PiE I S) = PiE I (\<lambda>i. (X i) closure_of (S i))"
+proof -
+ have *: "(\<forall>T. f \<in> T \<and> openin (product_topology X I) T \<longrightarrow> (\<exists>y\<in>Pi\<^sub>E I S. y \<in> T))
+ \<longleftrightarrow> (\<forall>i \<in> I. \<forall>T. f i \<in> T \<and> openin (X i) T \<longrightarrow> S i \<inter> T \<noteq> {})"
+ (is "?lhs = ?rhs")
+ if top: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> topspace (X i)" and ext: "f \<in> extensional I" for f
+ proof
+ assume L[rule_format]: ?lhs
+ show ?rhs
+ proof clarify
+ fix i T
+ assume "i \<in> I" "f i \<in> T" "openin (X i) T" "S i \<inter> T = {}"
+ then have "openin (product_topology X I) ((\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> {x. x i \<in> T})"
+ by (force simp: openin_product_topology intro: arbitrary_union_of_inc relative_to_inc finite_intersection_of_inc)
+ then show "False"
+ using L [of "topspace (product_topology X I) \<inter> {f. f i \<in> T}"] \<open>S i \<inter> T = {}\<close> \<open>f i \<in> T\<close> \<open>i \<in> I\<close>
+ by (auto simp: top ext PiE_iff)
+ qed
+ next
+ assume R [rule_format]: ?rhs
+ show ?lhs
+ proof (clarsimp simp: openin_product_topology union_of_def arbitrary_def)
+ fix \<U> U
+ assume
+ \<U>: "\<U> \<subseteq> Collect
+ (finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U) relative_to
+ (\<Pi>\<^sub>E i\<in>I. topspace (X i)))" and
+ "f \<in> U" "U \<in> \<U>"
+ then have "(finite intersection_of (\<lambda>F. \<exists>i U. F = {x. x i \<in> U} \<and> i \<in> I \<and> openin (X i) U)
+ relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))) U"
+ by blast
+ with \<open>f \<in> U\<close> \<open>U \<in> \<U>\<close>
+ obtain \<T> where "finite \<T>"
+ and \<T>: "\<And>C. C \<in> \<T> \<Longrightarrow> \<exists>i \<in> I. \<exists>V. openin (X i) V \<and> C = {x. x i \<in> V}"
+ and "topspace (product_topology X I) \<inter> \<Inter> \<T> \<subseteq> U" "f \<in> topspace (product_topology X I) \<inter> \<Inter> \<T>"
+ apply (clarsimp simp add: relative_to_def intersection_of_def)
+ apply (rule that, auto dest!: subsetD)
+ done
+ then have "f \<in> PiE I (topspace \<circ> X)" "f \<in> \<Inter>\<T>" and subU: "PiE I (topspace \<circ> X) \<inter> \<Inter>\<T> \<subseteq> U"
+ by (auto simp: PiE_iff)
+ have *: "f i \<in> topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}
+ \<and> openin (X i) (topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>})"
+ if "i \<in> I" for i
+ proof -
+ have "finite ((\<lambda>U. {x. x i \<in> U}) -` \<T>)"
+ proof (rule finite_vimageI [OF \<open>finite \<T>\<close>])
+ show "inj (\<lambda>U. {x. x i \<in> U})"
+ by (auto simp: inj_on_def)
+ qed
+ then have fin: "finite {U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}"
+ by (rule rev_finite_subset) auto
+ have "openin (X i) (\<Inter> (insert (topspace (X i)) {U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}))"
+ by (rule openin_Inter) (auto simp: fin)
+ then show ?thesis
+ using \<open>f \<in> \<Inter> \<T>\<close> by (fastforce simp: that top)
+ qed
+ define \<Phi> where "\<Phi> \<equiv> \<lambda>i. topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {f. f i \<in> U} \<in> \<T>}"
+ have "\<forall>i \<in> I. \<exists>x. x \<in> S i \<inter> \<Phi> i"
+ using R [OF _ *] unfolding \<Phi>_def by blast
+ then obtain \<theta> where \<theta> [rule_format]: "\<forall>i \<in> I. \<theta> i \<in> S i \<inter> \<Phi> i"
+ by metis
+ show "\<exists>y\<in>Pi\<^sub>E I S. \<exists>x\<in>\<U>. y \<in> x"
+ proof
+ show "\<exists>U \<in> \<U>. (\<lambda>i \<in> I. \<theta> i) \<in> U"
+ proof
+ have "restrict \<theta> I \<in> PiE I (topspace \<circ> X) \<inter> \<Inter>\<T>"
+ using \<T> by (fastforce simp: \<Phi>_def PiE_def dest: \<theta>)
+ then show "restrict \<theta> I \<in> U"
+ using subU by blast
+ qed (rule \<open>U \<in> \<U>\<close>)
+ next
+ show "(\<lambda>i \<in> I. \<theta> i) \<in> Pi\<^sub>E I S"
+ using \<theta> by simp
+ qed
+ qed
+ qed
+ show ?thesis
+ apply (simp add: * closure_of_def PiE_iff set_eq_iff cong: conj_cong)
+ by metis
+qed
-lemma openin_product_topology_alt:
- "openin (product_topology X I) S \<longleftrightarrow>
- (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
- (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
- apply (simp add: openin_product_topology arbitrary_union_of_alt product_topology_base_alt, auto)
- apply (drule bspec; blast)
+corollary closedin_product_topology:
+ "closedin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. closedin (X i) (S i))"
+ apply (simp add: PiE_eq PiE_eq_empty_iff closure_of_product_topology flip: closure_of_eq)
+ apply (metis closure_of_empty)
done
+corollary closedin_product_topology_singleton:
+ "f \<in> extensional I \<Longrightarrow> closedin (product_topology X I) {f} \<longleftrightarrow> (\<forall>i \<in> I. closedin (X i) {f i})"
+ using PiE_singleton closedin_product_topology [of X I]
+ by (metis (no_types, lifting) all_not_in_conv insertI1)
-text \<open>The basic property of the product topology is the continuity of projections:\<close>
+
+subsubsection \<open>The basic property of the product topology is the continuity of projections:\<close>
lemma continuous_on_topo_product_coordinates [simp]:
assumes "i \<in> I"
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Wed Mar 06 21:44:30 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Thu Mar 07 14:08:05 2019 +0000
@@ -242,6 +242,27 @@
shows "path_connected {a..b}"
using is_interval_cc is_interval_path_connected by blast
+lemma path_connected_Ioi[simp]: "path_connected {a<..}" for a :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ici[simp]: "path_connected {a..}" for a :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Iio[simp]: "path_connected {..<a}" for a :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Iic[simp]: "path_connected {..a}" for a :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ioo[simp]: "path_connected {a<..<b}" for a b :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ioc[simp]: "path_connected {a<..b}" for a b :: real
+ by (simp add: convex_imp_path_connected)
+
+lemma path_connected_Ico[simp]: "path_connected {a..<b}" for a b :: real
+ by (simp add: convex_imp_path_connected)
+
lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
by (auto simp: real_atLeastGreaterThan_eq)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/T1_Spaces.thy Thu Mar 07 14:08:05 2019 +0000
@@ -0,0 +1,201 @@
+section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
+
+theory T1_Spaces
+imports Function_Topology
+begin
+
+definition t1_space where
+ "t1_space X \<equiv> \<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x\<noteq>y \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> y \<notin> U)"
+
+lemma t1_space_expansive:
+ "\<lbrakk>topspace Y = topspace X; \<And>U. openin X U \<Longrightarrow> openin Y U\<rbrakk> \<Longrightarrow> t1_space X \<Longrightarrow> t1_space Y"
+ by (metis t1_space_def)
+
+lemma t1_space_alt:
+ "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<forall>y \<in> topspace X. x\<noteq>y \<longrightarrow> (\<exists>U. closedin X U \<and> x \<in> U \<and> y \<notin> U))"
+ by (metis DiffE DiffI closedin_def openin_closedin_eq t1_space_def)
+
+lemma t1_space_empty: "topspace X = {} \<Longrightarrow> t1_space X"
+ by (simp add: t1_space_def)
+
+lemma t1_space_derived_set_of_singleton:
+ "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. X derived_set_of {x} = {})"
+ apply (simp add: t1_space_def derived_set_of_def, safe)
+ apply (metis openin_topspace)
+ by force
+
+lemma t1_space_derived_set_of_finite:
+ "t1_space X \<longleftrightarrow> (\<forall>S. finite S \<longrightarrow> X derived_set_of S = {})"
+proof (intro iffI allI impI)
+ fix S :: "'a set"
+ assume "finite S"
+ then have fin: "finite ((\<lambda>x. {x}) ` (topspace X \<inter> S))"
+ by blast
+ assume "t1_space X"
+ then have "X derived_set_of (\<Union>x \<in> topspace X \<inter> S. {x}) = {}"
+ unfolding derived_set_of_Union [OF fin]
+ by (auto simp: t1_space_derived_set_of_singleton)
+ then have "X derived_set_of (topspace X \<inter> S) = {}"
+ by simp
+ then show "X derived_set_of S = {}"
+ by simp
+qed (auto simp: t1_space_derived_set_of_singleton)
+
+lemma t1_space_closedin_singleton:
+ "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. closedin X {x})"
+ apply (rule iffI)
+ apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_singleton)
+ using t1_space_alt by auto
+
+lemma closedin_t1_singleton:
+ "\<lbrakk>t1_space X; a \<in> topspace X\<rbrakk> \<Longrightarrow> closedin X {a}"
+ by (simp add: t1_space_closedin_singleton)
+
+lemma t1_space_closedin_finite:
+ "t1_space X \<longleftrightarrow> (\<forall>S. finite S \<and> S \<subseteq> topspace X \<longrightarrow> closedin X S)"
+ apply (rule iffI)
+ apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_finite)
+ by (simp add: t1_space_closedin_singleton)
+
+lemma closure_of_singleton:
+ "t1_space X \<Longrightarrow> X closure_of {a} = (if a \<in> topspace X then {a} else {})"
+ by (simp add: closure_of_eq t1_space_closedin_singleton closure_of_eq_empty_gen)
+
+lemma separated_in_singleton:
+ assumes "t1_space X"
+ shows "separatedin X {a} S \<longleftrightarrow> a \<in> topspace X \<and> S \<subseteq> topspace X \<and> (a \<notin> X closure_of S)"
+ "separatedin X S {a} \<longleftrightarrow> a \<in> topspace X \<and> S \<subseteq> topspace X \<and> (a \<notin> X closure_of S)"
+ unfolding separatedin_def
+ using assms closure_of closure_of_singleton by fastforce+
+
+lemma t1_space_openin_delete:
+ "t1_space X \<longleftrightarrow> (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (U - {x}))"
+ apply (rule iffI)
+ apply (meson closedin_t1_singleton in_mono openin_diff openin_subset)
+ by (simp add: closedin_def t1_space_closedin_singleton)
+
+lemma t1_space_openin_delete_alt:
+ "t1_space X \<longleftrightarrow> (\<forall>U x. openin X U \<longrightarrow> openin X (U - {x}))"
+ by (metis Diff_empty Diff_insert0 t1_space_openin_delete)
+
+
+lemma t1_space_singleton_Inter_open:
+ "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<Inter>{U. openin X U \<and> x \<in> U} = {x})" (is "?P=?Q")
+ and t1_space_Inter_open_supersets:
+ "t1_space X \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> \<Inter>{U. openin X U \<and> S \<subseteq> U} = S)" (is "?P=?R")
+proof -
+ have "?R \<Longrightarrow> ?Q"
+ apply clarify
+ apply (drule_tac x="{x}" in spec, simp)
+ done
+ moreover have "?Q \<Longrightarrow> ?P"
+ apply (clarsimp simp add: t1_space_def)
+ apply (drule_tac x=x in bspec)
+ apply (simp_all add: set_eq_iff)
+ by (metis (no_types, lifting))
+ moreover have "?P \<Longrightarrow> ?R"
+ proof (clarsimp simp add: t1_space_closedin_singleton, rule subset_antisym)
+ fix S
+ assume S: "\<forall>x\<in>topspace X. closedin X {x}" "S \<subseteq> topspace X"
+ then show "\<Inter> {U. openin X U \<and> S \<subseteq> U} \<subseteq> S"
+ apply clarsimp
+ by (metis Diff_insert_absorb Set.set_insert closedin_def openin_topspace subset_insert)
+ qed force
+ ultimately show "?P=?Q" "?P=?R"
+ by auto
+qed
+
+lemma t1_space_derived_set_of_infinite_openin:
+ "t1_space X \<longleftrightarrow>
+ (\<forall>S. X derived_set_of S =
+ {x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)})"
+ (is "_ = ?rhs")
+proof
+ assume "t1_space X"
+ show ?rhs
+ proof safe
+ fix S x U
+ assume "x \<in> X derived_set_of S" "x \<in> U" "openin X U" "finite (S \<inter> U)"
+ with \<open>t1_space X\<close> show "False"
+ apply (simp add: t1_space_derived_set_of_finite)
+ by (metis IntI empty_iff empty_subsetI inf_commute openin_Int_derived_set_of_subset subset_antisym)
+ next
+ fix S x
+ have eq: "(\<exists>y. (y \<noteq> x) \<and> y \<in> S \<and> y \<in> T) \<longleftrightarrow> ~((S \<inter> T) \<subseteq> {x})" for x S T
+ by blast
+ assume "x \<in> topspace X" "\<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite (S \<inter> U)"
+ then show "x \<in> X derived_set_of S"
+ apply (clarsimp simp add: derived_set_of_def eq)
+ by (meson finite.emptyI finite.insertI finite_subset)
+ qed (auto simp: in_derived_set_of)
+qed (auto simp: t1_space_derived_set_of_singleton)
+
+lemma finite_t1_space_imp_discrete_topology:
+ "\<lbrakk>topspace X = U; finite U; t1_space X\<rbrakk> \<Longrightarrow> X = discrete_topology U"
+ by (metis discrete_topology_unique_derived_set t1_space_derived_set_of_finite)
+
+lemma t1_space_subtopology: "t1_space X \<Longrightarrow> t1_space(subtopology X U)"
+ by (simp add: derived_set_of_subtopology t1_space_derived_set_of_finite)
+
+lemma closedin_derived_set_of_gen:
+ "t1_space X \<Longrightarrow> closedin X (X derived_set_of S)"
+ apply (clarsimp simp add: in_derived_set_of closedin_contains_derived_set derived_set_of_subset_topspace)
+ by (metis DiffD2 insert_Diff insert_iff t1_space_openin_delete)
+
+lemma derived_set_of_derived_set_subset_gen:
+ "t1_space X \<Longrightarrow> X derived_set_of (X derived_set_of S) \<subseteq> X derived_set_of S"
+ by (meson closedin_contains_derived_set closedin_derived_set_of_gen)
+
+lemma subtopology_eq_discrete_topology_gen_finite:
+ "\<lbrakk>t1_space X; finite S\<rbrakk> \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
+ by (simp add: subtopology_eq_discrete_topology_gen t1_space_derived_set_of_finite)
+
+lemma subtopology_eq_discrete_topology_finite:
+ "\<lbrakk>t1_space X; S \<subseteq> topspace X; finite S\<rbrakk>
+ \<Longrightarrow> subtopology X S = discrete_topology S"
+ by (simp add: subtopology_eq_discrete_topology_eq t1_space_derived_set_of_finite)
+
+lemma t1_space_closed_map_image:
+ "\<lbrakk>closed_map X Y f; f ` (topspace X) = topspace Y; t1_space X\<rbrakk> \<Longrightarrow> t1_space Y"
+ by (metis closed_map_def finite_subset_image t1_space_closedin_finite)
+
+lemma homeomorphic_t1_space: "X homeomorphic_space Y \<Longrightarrow> (t1_space X \<longleftrightarrow> t1_space Y)"
+ apply (clarsimp simp add: homeomorphic_space_def)
+ by (meson homeomorphic_eq_everything_map homeomorphic_maps_map t1_space_closed_map_image)
+
+proposition t1_space_product_topology:
+ "t1_space (product_topology X I)
+\<longleftrightarrow> topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. t1_space (X i))"
+proof (cases "topspace(product_topology X I) = {}")
+ case True
+ then show ?thesis
+ using True t1_space_empty by blast
+next
+ case False
+ then obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
+ by fastforce
+ have "t1_space (product_topology X I) \<longleftrightarrow> (\<forall>i\<in>I. t1_space (X i))"
+ proof (intro iffI ballI)
+ show "t1_space (X i)" if "t1_space (product_topology X I)" and "i \<in> I" for i
+ proof -
+ have clo: "\<And>h. h \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<Longrightarrow> closedin (product_topology X I) {h}"
+ using that by (simp add: t1_space_closedin_singleton)
+ show ?thesis
+ unfolding t1_space_closedin_singleton
+ proof clarify
+ show "closedin (X i) {xi}" if "xi \<in> topspace (X i)" for xi
+ using clo [of "\<lambda>j \<in> I. if i=j then xi else f j"] f that \<open>i \<in> I\<close>
+ by (fastforce simp add: closedin_product_topology_singleton)
+ qed
+ qed
+ next
+ next
+ show "t1_space (product_topology X I)" if "\<forall>i\<in>I. t1_space (X i)"
+ using that
+ by (simp add: t1_space_closedin_singleton Ball_def PiE_iff closedin_product_topology_singleton)
+ qed
+ then show ?thesis
+ using False by blast
+qed
+
+end
--- a/src/HOL/Library/Equipollence.thy Wed Mar 06 21:44:30 2019 +0100
+++ b/src/HOL/Library/Equipollence.thy Thu Mar 07 14:08:05 2019 +0000
@@ -82,7 +82,6 @@
apply (simp add: infinite_countable_subset)
using infinite_iff_countable_subset by blast
-
lemma bij_betw_iff_bijections:
"bij_betw f A B \<longleftrightarrow> (\<exists>g. (\<forall>x \<in> A. f x \<in> B \<and> g(f x) = x) \<and> (\<forall>y \<in> B. g y \<in> A \<and> f(g y) = y))"
(is "?lhs = ?rhs")
@@ -114,9 +113,23 @@
using * by (auto simp: image_def)
qed
+lemma singleton_lepoll: "{x} \<lesssim> insert y A"
+ by (force simp: lepoll_def)
+
+lemma singleton_eqpoll: "{x} \<approx> {y}"
+ by (blast intro: lepoll_antisym singleton_lepoll)
+
+lemma subset_singleton_iff_lepoll: "(\<exists>x. S \<subseteq> {x}) \<longleftrightarrow> S \<lesssim> {()}"
+proof safe
+ show "S \<lesssim> {()}" if "S \<subseteq> {x}" for x
+ using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2)
+ show "\<exists>x. S \<subseteq> {x}" if "S \<lesssim> {()}"
+ by (metis (no_types, hide_lams) image_empty image_insert lepoll_iff that)
+qed
+
+
subsection\<open>The strict relation\<close>
-
lemma lesspoll_not_refl [iff]: "~ (i \<prec> i)"
by (simp add: lepoll_antisym lesspoll_def)