# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1551967685 0
# Node ID 11065b70407da6cd54eb9c0fa029acf9bddc7339
# Parent  6ebe97815275995cfdd487c69e8e8a62bcff4fe4
new material for Analysis

diff -r 6ebe97815275 -r 11065b70407d src/HOL/Analysis/Abstract_Limits.thy
--- /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
diff -r 6ebe97815275 -r 11065b70407d src/HOL/Analysis/Abstract_Topology.thy
--- 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
 
diff -r 6ebe97815275 -r 11065b70407d src/HOL/Analysis/Analysis.thy
--- 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
diff -r 6ebe97815275 -r 11065b70407d src/HOL/Analysis/Function_Topology.thy
--- 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"
diff -r 6ebe97815275 -r 11065b70407d src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- 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)
 
diff -r 6ebe97815275 -r 11065b70407d src/HOL/Analysis/T1_Spaces.thy
--- /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
diff -r 6ebe97815275 -r 11065b70407d src/HOL/Library/Equipollence.thy
--- 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)