new material for Analysis
authorpaulson <lp15@cam.ac.uk>
Thu Mar 07 14:08:05 2019 +0000 (6 weeks ago ago)
changeset 7005511065b70407d
parent 70054 6ebe97815275
child 70056 03bc14eab432
new material for Analysis
src/HOL/Analysis/Abstract_Limits.thy
src/HOL/Analysis/Abstract_Topology.thy
src/HOL/Analysis/Analysis.thy
src/HOL/Analysis/Function_Topology.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
src/HOL/Analysis/T1_Spaces.thy
src/HOL/Library/Equipollence.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Abstract_Limits.thy	Thu Mar 07 14:08:05 2019 +0000
     1.3 @@ -0,0 +1,296 @@
     1.4 +theory Abstract_Limits
     1.5 +  imports
     1.6 +    Abstract_Topology
     1.7 +begin
     1.8 +
     1.9 +subsection\<open>nhdsin and atin\<close>
    1.10 +
    1.11 +definition nhdsin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
    1.12 +  where "nhdsin X a =
    1.13 +           (if a \<in> topspace X then (INF S:{S. openin X S \<and> a \<in> S}. principal S) else bot)"
    1.14 +
    1.15 +definition atin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
    1.16 +  where "atin X a \<equiv> inf (nhdsin X a) (principal (topspace X - {a}))"
    1.17 +
    1.18 +
    1.19 +lemma nhdsin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> nhdsin X a = bot"
    1.20 +  and atin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> atin X a = bot"
    1.21 +  by (simp_all add: nhdsin_def atin_def)
    1.22 +
    1.23 +lemma eventually_nhdsin:
    1.24 +  "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))"
    1.25 +proof (cases "a \<in> topspace X")
    1.26 +  case True
    1.27 +  hence "nhdsin X a = (INF S:{S. openin X S \<and> a \<in> S}. principal S)"
    1.28 +    by (simp add: nhdsin_def)
    1.29 +  also have "eventually P \<dots> \<longleftrightarrow> (\<exists>S. openin X S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
    1.30 +    using True by (subst eventually_INF_base) (auto simp: eventually_principal)
    1.31 +  finally show ?thesis using True by simp
    1.32 +qed auto
    1.33 +
    1.34 +lemma eventually_atin:
    1.35 +  "eventually P (atin X a) \<longleftrightarrow> a \<notin> topspace X \<or>
    1.36 +             (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
    1.37 +proof (cases "a \<in> topspace X")
    1.38 +  case True
    1.39 +  hence "eventually P (atin X a) \<longleftrightarrow> (\<exists>S. openin X S \<and>
    1.40 +           a \<in> S \<and> (\<forall>x\<in>S. x \<in> topspace X \<and> x \<noteq> a \<longrightarrow> P x))"
    1.41 +    by (simp add: atin_def eventually_inf_principal eventually_nhdsin)
    1.42 +  also have "\<dots> \<longleftrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
    1.43 +    using openin_subset by (intro ex_cong) auto
    1.44 +  finally show ?thesis by (simp add: True)
    1.45 +qed auto
    1.46 +
    1.47 +
    1.48 +subsection\<open>Limits in a topological space\<close>
    1.49 +
    1.50 +definition limit :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
    1.51 +  "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)"
    1.52 +
    1.53 +lemma limit_euclideanreal_iff [simp]: "limit euclideanreal f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
    1.54 +  by (auto simp: limit_def tendsto_def)
    1.55 +
    1.56 +lemma limit_in_topspace: "limit X f l F \<Longrightarrow> l \<in> topspace X"
    1.57 +  by (simp add: limit_def)
    1.58 +
    1.59 +lemma limit_const: "limit X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
    1.60 +  by (simp add: limit_def)
    1.61 +
    1.62 +lemma limit_real_const: "limit euclideanreal (\<lambda>a. l) l F"
    1.63 +  by (simp add: limit_def)
    1.64 +
    1.65 +lemma limit_eventually:
    1.66 +   "\<lbrakk>l \<in> topspace X; eventually (\<lambda>x. f x = l) F\<rbrakk> \<Longrightarrow> limit X f l F"
    1.67 +  by (auto simp: limit_def eventually_mono)
    1.68 +
    1.69 +lemma limit_subsequence:
    1.70 +   "\<lbrakk>strict_mono r; limit X f l sequentially\<rbrakk> \<Longrightarrow> limit X (f \<circ> r) l sequentially"
    1.71 +  unfolding limit_def using eventually_subseq by fastforce
    1.72 +
    1.73 +lemma limit_subtopology:
    1.74 +  "limit (subtopology X S) f l F
    1.75 +   \<longleftrightarrow> l \<in> S \<and> eventually (\<lambda>a. f a \<in> S) F \<and> limit X f l F"  (is "?lhs = ?rhs")
    1.76 +proof (cases "l \<in> S \<inter> topspace X")
    1.77 +  case True
    1.78 +  show ?thesis
    1.79 +  proof
    1.80 +    assume L: ?lhs
    1.81 +    with True
    1.82 +    have "\<forall>\<^sub>F b in F. f b \<in> topspace X \<inter> S"
    1.83 +      by (metis (no_types) limit_def openin_topspace topspace_subtopology)
    1.84 +    with L show ?rhs
    1.85 +      apply (clarsimp simp add: limit_def eventually_mono topspace_subtopology openin_subtopology_alt)
    1.86 +      apply (drule_tac x="S \<inter> U" in spec, force simp: elim: eventually_mono)
    1.87 +      done
    1.88 +  next
    1.89 +    assume ?rhs
    1.90 +    then show ?lhs
    1.91 +      using eventually_elim2
    1.92 +      by (fastforce simp add: limit_def topspace_subtopology openin_subtopology_alt)
    1.93 +  qed
    1.94 +qed (auto simp: limit_def topspace_subtopology)
    1.95 +
    1.96 +
    1.97 +lemma limit_sequentially:
    1.98 +   "limit X S l sequentially \<longleftrightarrow>
    1.99 +     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))"
   1.100 +  by (simp add: limit_def eventually_sequentially)
   1.101 +
   1.102 +lemma limit_sequentially_offset:
   1.103 +   "limit X f l sequentially \<Longrightarrow> limit X (\<lambda>i. f (i + k)) l sequentially"
   1.104 +  unfolding limit_sequentially
   1.105 +  by (metis add.commute le_add2 order_trans)
   1.106 +
   1.107 +lemma limit_sequentially_offset_rev:
   1.108 +  assumes "limit X (\<lambda>i. f (i + k)) l sequentially"
   1.109 +  shows "limit X f l sequentially"
   1.110 +proof -
   1.111 +  have "\<exists>N. \<forall>n\<ge>N. f n \<in> U" if U: "openin X U" "l \<in> U" for U
   1.112 +  proof -
   1.113 +    obtain N where "\<And>n. n\<ge>N \<Longrightarrow> f (n + k) \<in> U"
   1.114 +      using assms U unfolding limit_sequentially by blast
   1.115 +    then have "\<forall>n\<ge>N+k. f n \<in> U"
   1.116 +      by (metis add_leD2 le_add_diff_inverse ordered_cancel_comm_monoid_diff_class.le_diff_conv2 add.commute)
   1.117 +    then show ?thesis ..
   1.118 +  qed
   1.119 +  with assms show ?thesis
   1.120 +    unfolding limit_sequentially
   1.121 +    by simp
   1.122 +qed
   1.123 +
   1.124 +lemma limit_atin:
   1.125 +   "limit Y f y (atin X x) \<longleftrightarrow>
   1.126 +        y \<in> topspace Y \<and>
   1.127 +        (x \<in> topspace X
   1.128 +        \<longrightarrow> (\<forall>V. openin Y V \<and> y \<in> V
   1.129 +                 \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> f ` (U - {x}) \<subseteq> V)))"
   1.130 +  by (auto simp: limit_def eventually_atin image_subset_iff)
   1.131 +
   1.132 +lemma limit_atin_self:
   1.133 +   "limit Y f (f a) (atin X a) \<longleftrightarrow>
   1.134 +        f a \<in> topspace Y \<and>
   1.135 +        (a \<in> topspace X
   1.136 +         \<longrightarrow> (\<forall>V. openin Y V \<and> f a \<in> V
   1.137 +                  \<longrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> f ` U \<subseteq> V)))"
   1.138 +  unfolding limit_atin by fastforce
   1.139 +
   1.140 +lemma limit_trivial:
   1.141 +   "\<lbrakk>trivial_limit F; y \<in> topspace X\<rbrakk> \<Longrightarrow> limit X f y F"
   1.142 +  by (simp add: limit_def)
   1.143 +
   1.144 +lemma limit_transform_eventually:
   1.145 +   "\<lbrakk>eventually (\<lambda>x. f x = g x) F; limit X f l F\<rbrakk> \<Longrightarrow> limit X g l F"
   1.146 +  unfolding limit_def using eventually_elim2 by fastforce
   1.147 +
   1.148 +lemma continuous_map_limit:
   1.149 +  assumes "continuous_map X Y g" and f: "limit X f l F"
   1.150 +  shows "limit Y (g \<circ> f) (g l) F"
   1.151 +proof -
   1.152 +  have "g l \<in> topspace Y"
   1.153 +    by (meson assms continuous_map_def limit_in_topspace)
   1.154 +  moreover
   1.155 +  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>
   1.156 +            \<Longrightarrow> \<forall>\<^sub>F x in F. g (f x) \<in> U"
   1.157 +    using assms eventually_mono
   1.158 +    by (fastforce simp: limit_def dest!: openin_continuous_map_preimage)
   1.159 +  ultimately show ?thesis
   1.160 +    using f by (fastforce simp add: limit_def)
   1.161 +qed
   1.162 +
   1.163 +
   1.164 +subsection\<open>Pointwise continuity in topological spaces\<close>
   1.165 +
   1.166 +definition topcontinuous_at where
   1.167 +  "topcontinuous_at X Y f x \<longleftrightarrow>
   1.168 +     x \<in> topspace X \<and>
   1.169 +     (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
   1.170 +     (\<forall>V. openin Y V \<and> f x \<in> V
   1.171 +          \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y \<in> U. f y \<in> V)))"
   1.172 +
   1.173 +lemma topcontinuous_at_atin:
   1.174 +   "topcontinuous_at X Y f x \<longleftrightarrow>
   1.175 +        x \<in> topspace X \<and>
   1.176 +        (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
   1.177 +        limit Y f (f x) (atin X x)"
   1.178 +  unfolding topcontinuous_at_def
   1.179 +  by (fastforce simp add: limit_atin)+
   1.180 +
   1.181 +lemma continuous_map_eq_topcontinuous_at:
   1.182 +   "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. topcontinuous_at X Y f x)"
   1.183 +    (is "?lhs = ?rhs")
   1.184 +proof
   1.185 +  assume ?lhs
   1.186 +  then show ?rhs
   1.187 +    by (auto simp: continuous_map_def topcontinuous_at_def)
   1.188 +next
   1.189 +  assume R: ?rhs
   1.190 +  then show ?lhs
   1.191 +    apply (auto simp: continuous_map_def topcontinuous_at_def)
   1.192 +    apply (subst openin_subopen, safe)
   1.193 +    apply (drule bspec, assumption)
   1.194 +    using openin_subset[of X] apply (auto simp: subset_iff dest!: spec)
   1.195 +    done
   1.196 +qed
   1.197 +
   1.198 +lemma continuous_map_atin:
   1.199 +   "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. limit Y f (f x) (atin X x))"
   1.200 +  by (auto simp: limit_def topcontinuous_at_atin continuous_map_eq_topcontinuous_at)
   1.201 +
   1.202 +lemma limit_continuous_map:
   1.203 +   "\<lbrakk>continuous_map X Y f; a \<in> topspace X; f a = b\<rbrakk> \<Longrightarrow> limit Y f b (atin X a)"
   1.204 +  by (auto simp: continuous_map_atin)
   1.205 +
   1.206 +
   1.207 +subsection\<open>Combining theorems for continuous functions into the reals\<close>
   1.208 +
   1.209 +lemma continuous_map_real_const [simp,continuous_intros]:
   1.210 +   "continuous_map X euclideanreal (\<lambda>x. c)"
   1.211 +  by simp
   1.212 +
   1.213 +lemma continuous_map_real_mult [continuous_intros]:
   1.214 +   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
   1.215 +   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x * g x)"
   1.216 +  by (simp add: continuous_map_atin tendsto_mult)
   1.217 +
   1.218 +lemma continuous_map_real_pow [continuous_intros]:
   1.219 +   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x ^ n)"
   1.220 +  by (induction n) (auto simp: continuous_map_real_mult)
   1.221 +
   1.222 +lemma continuous_map_real_mult_left:
   1.223 +   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. c * f x)"
   1.224 +  by (simp add: continuous_map_atin tendsto_mult)
   1.225 +
   1.226 +lemma continuous_map_real_mult_left_eq:
   1.227 +   "continuous_map X euclideanreal (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> continuous_map X euclideanreal f"
   1.228 +proof (cases "c = 0")
   1.229 +  case False
   1.230 +  have "continuous_map X euclideanreal (\<lambda>x. c * f x) \<Longrightarrow> continuous_map X euclideanreal f"
   1.231 +    apply (frule continuous_map_real_mult_left [where c="inverse c"])
   1.232 +    apply (simp add: field_simps False)
   1.233 +    done
   1.234 +  with False show ?thesis
   1.235 +    using continuous_map_real_mult_left by blast
   1.236 +qed simp
   1.237 +
   1.238 +lemma continuous_map_real_mult_right:
   1.239 +   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x * c)"
   1.240 +  by (simp add: continuous_map_atin tendsto_mult)
   1.241 +
   1.242 +lemma continuous_map_real_mult_right_eq:
   1.243 +   "continuous_map X euclideanreal (\<lambda>x. f x * c) \<longleftrightarrow> c = 0 \<or> continuous_map X euclideanreal f"
   1.244 +  by (simp add: mult.commute flip: continuous_map_real_mult_left_eq)
   1.245 +
   1.246 +lemma continuous_map_real_minus [continuous_intros]:
   1.247 +   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. - f x)"
   1.248 +  by (simp add: continuous_map_atin tendsto_minus)
   1.249 +
   1.250 +lemma continuous_map_real_minus_eq:
   1.251 +   "continuous_map X euclideanreal (\<lambda>x. - f x) \<longleftrightarrow> continuous_map X euclideanreal f"
   1.252 +  using continuous_map_real_mult_left_eq [where c = "-1"] by auto
   1.253 +
   1.254 +lemma continuous_map_real_add [continuous_intros]:
   1.255 +   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
   1.256 +   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x + g x)"
   1.257 +  by (simp add: continuous_map_atin tendsto_add)
   1.258 +
   1.259 +lemma continuous_map_real_diff [continuous_intros]:
   1.260 +   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
   1.261 +   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x - g x)"
   1.262 +  by (simp add: continuous_map_atin tendsto_diff)
   1.263 +
   1.264 +lemma continuous_map_real_abs [continuous_intros]:
   1.265 +   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. abs(f x))"
   1.266 +  by (simp add: continuous_map_atin tendsto_rabs)
   1.267 +
   1.268 +lemma continuous_map_real_max [continuous_intros]:
   1.269 +   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
   1.270 +   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. max (f x) (g x))"
   1.271 +  by (simp add: continuous_map_atin tendsto_max)
   1.272 +
   1.273 +lemma continuous_map_real_min [continuous_intros]:
   1.274 +   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
   1.275 +   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. min (f x) (g x))"
   1.276 +  by (simp add: continuous_map_atin tendsto_min)
   1.277 +
   1.278 +lemma continuous_map_sum [continuous_intros]:
   1.279 +   "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)\<rbrakk>
   1.280 +        \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sum (f x) I)"
   1.281 +  by (simp add: continuous_map_atin tendsto_sum)
   1.282 +
   1.283 +lemma continuous_map_prod [continuous_intros]:
   1.284 +   "\<lbrakk>finite I;
   1.285 +         \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)\<rbrakk>
   1.286 +        \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. prod (f x) I)"
   1.287 +  by (simp add: continuous_map_atin tendsto_prod)
   1.288 +
   1.289 +lemma continuous_map_real_inverse [continuous_intros]:
   1.290 +   "\<lbrakk>continuous_map X euclideanreal f; \<And>x. x \<in> topspace X \<Longrightarrow> f x \<noteq> 0\<rbrakk>
   1.291 +        \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. inverse(f x))"
   1.292 +  by (simp add: continuous_map_atin tendsto_inverse)
   1.293 +
   1.294 +lemma continuous_map_real_divide [continuous_intros]:
   1.295 +   "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g; \<And>x. x \<in> topspace X \<Longrightarrow> g x \<noteq> 0\<rbrakk>
   1.296 +   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x / g x)"
   1.297 +  by (simp add: continuous_map_atin tendsto_divide)
   1.298 +
   1.299 +end
     2.1 --- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Mar 06 21:44:30 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Mar 07 14:08:05 2019 +0000
     2.3 @@ -290,7 +290,7 @@
     2.4  lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)"
     2.5    by (force simp: relative_to_def openin_subtopology)
     2.6  
     2.7 -lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
     2.8 +lemma topspace_subtopology [simp]: "topspace (subtopology U V) = topspace U \<inter> V"
     2.9    by (auto simp: topspace_def openin_subtopology)
    2.10  
    2.11  lemma topspace_subtopology_subset:
    2.12 @@ -597,7 +597,7 @@
    2.13           {x \<in> topspace X.
    2.14                  (\<forall>T. x \<in> T \<and> openin X T \<longrightarrow> (\<exists>y\<noteq>x. y \<in> S \<and> y \<in> T))}"
    2.15  
    2.16 -lemma derived_set_of_restrict:
    2.17 +lemma derived_set_of_restrict [simp]:
    2.18     "X derived_set_of (topspace X \<inter> S) = X derived_set_of S"
    2.19    by (simp add: derived_set_of_def) (metis openin_subset subset_iff)
    2.20  
    2.21 @@ -624,7 +624,7 @@
    2.22     "S \<subseteq> T \<Longrightarrow> X derived_set_of S \<subseteq> X derived_set_of T"
    2.23    unfolding derived_set_of_def by blast
    2.24  
    2.25 -lemma derived_set_of_union:
    2.26 +lemma derived_set_of_Un:
    2.27     "X derived_set_of (S \<union> T) = X derived_set_of S \<union> X derived_set_of T" (is "?lhs = ?rhs")
    2.28  proof
    2.29    show "?lhs \<subseteq> ?rhs"
    2.30 @@ -634,12 +634,12 @@
    2.31      by (simp add: derived_set_of_mono)
    2.32  qed
    2.33  
    2.34 -lemma derived_set_of_unions:
    2.35 +lemma derived_set_of_Union:
    2.36     "finite \<F> \<Longrightarrow> X derived_set_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X derived_set_of S)"
    2.37  proof (induction \<F> rule: finite_induct)
    2.38    case (insert S \<F>)
    2.39    then show ?case
    2.40 -    by (simp add: derived_set_of_union)
    2.41 +    by (simp add: derived_set_of_Un)
    2.42  qed auto
    2.43  
    2.44  lemma derived_set_of_topspace:
    2.45 @@ -745,7 +745,7 @@
    2.46    by auto (meson closure_of_mono inf_mono subset_iff)
    2.47  
    2.48  lemma closure_of_Un [simp]: "X closure_of (S \<union> T) = X closure_of S \<union> X closure_of T"
    2.49 -  by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_union inf_sup_distrib1)
    2.50 +  by (simp add: Un_assoc Un_left_commute closure_of_alt derived_set_of_Un inf_sup_distrib1)
    2.51  
    2.52  lemma closure_of_Union:
    2.53     "finite \<F> \<Longrightarrow> X closure_of (\<Union>\<F>) = (\<Union>S \<in> \<F>. X closure_of S)"
    2.54 @@ -1545,6 +1545,26 @@
    2.55  lemma continuous_map_iff_continuous_real [simp]: "continuous_map (subtopology euclideanreal S) euclideanreal g = continuous_on S g"
    2.56    by (force simp: continuous_map openin_subtopology continuous_on_open_invariant)
    2.57  
    2.58 +lemma continuous_map_iff_continuous_real2 [simp]: "continuous_map euclideanreal euclideanreal g = continuous_on UNIV g"
    2.59 +  by (metis continuous_map_iff_continuous_real subtopology_UNIV)
    2.60 +
    2.61 +lemma continuous_map_openin_preimage_eq:
    2.62 +   "continuous_map X Y f \<longleftrightarrow>
    2.63 +        f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. openin Y U \<longrightarrow> openin X (topspace X \<inter> f -` U))"
    2.64 +  by (auto simp: continuous_map_def vimage_def Int_def)
    2.65 +
    2.66 +lemma continuous_map_closedin_preimage_eq:
    2.67 +   "continuous_map X Y f \<longleftrightarrow>
    2.68 +        f ` (topspace X) \<subseteq> topspace Y \<and> (\<forall>U. closedin Y U \<longrightarrow> closedin X (topspace X \<inter> f -` U))"
    2.69 +  by (auto simp: continuous_map_closedin vimage_def Int_def)
    2.70 +
    2.71 +lemma continuous_map_square_root: "continuous_map euclideanreal euclideanreal sqrt"
    2.72 +  by (simp add: continuous_at_imp_continuous_on isCont_real_sqrt)
    2.73 +
    2.74 +lemma continuous_map_sqrt [continuous_intros]:
    2.75 +   "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sqrt(f x))"
    2.76 +  by (meson continuous_map_compose continuous_map_eq continuous_map_square_root o_apply)
    2.77 +
    2.78  lemma continuous_map_id [simp]: "continuous_map X X id"
    2.79    unfolding continuous_map_def  using openin_subopen topspace_def by fastforce
    2.80  
     3.1 --- a/src/HOL/Analysis/Analysis.thy	Wed Mar 06 21:44:30 2019 +0100
     3.2 +++ b/src/HOL/Analysis/Analysis.thy	Thu Mar 07 14:08:05 2019 +0000
     3.3 @@ -5,6 +5,7 @@
     3.4    Determinants
     3.5    (* Topology *)
     3.6    Connected
     3.7 +  Abstract_Limits
     3.8    (* Functional Analysis *)
     3.9    Elementary_Normed_Spaces
    3.10    Norm_Arith
    3.11 @@ -27,6 +28,7 @@
    3.12    Bounded_Continuous_Function
    3.13    Abstract_Topology
    3.14    Function_Topology
    3.15 +  T1_Spaces
    3.16    Infinite_Products
    3.17    Infinite_Set_Sum
    3.18    Weierstrass_Theorems
     4.1 --- a/src/HOL/Analysis/Function_Topology.thy	Wed Mar 06 21:44:30 2019 +0100
     4.2 +++ b/src/HOL/Analysis/Function_Topology.thy	Thu Mar 07 14:08:05 2019 +0000
     4.3 @@ -546,7 +546,7 @@
     4.4      done
     4.5  qed
     4.6  
     4.7 -lemma topspace_product_topology:
     4.8 +lemma topspace_product_topology [simp]:
     4.9    "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
    4.10  proof
    4.11    show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
    4.12 @@ -700,21 +700,101 @@
    4.13      by meson
    4.14  qed
    4.15  
    4.16 -
    4.17 -lemma topspace_product_topology_alt:
    4.18 -   "topspace (product_topology Y I) = {f \<in> extensional I. \<forall>k \<in> I. f k \<in> topspace(Y k)}"
    4.19 -  by (force simp: product_topology PiE_def)
    4.20 +lemma closure_of_product_topology:
    4.21 +  "(product_topology X I) closure_of (PiE I S) = PiE I (\<lambda>i. (X i) closure_of (S i))"
    4.22 +proof -
    4.23 +  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))
    4.24 +       \<longleftrightarrow> (\<forall>i \<in> I. \<forall>T. f i \<in> T \<and> openin (X i) T \<longrightarrow> S i \<inter> T \<noteq> {})"
    4.25 +    (is "?lhs = ?rhs")
    4.26 +    if top: "\<And>i. i \<in> I \<Longrightarrow> f i \<in> topspace (X i)" and ext:  "f \<in> extensional I" for f
    4.27 +  proof
    4.28 +    assume L[rule_format]: ?lhs
    4.29 +    show ?rhs
    4.30 +    proof clarify
    4.31 +      fix i T
    4.32 +      assume "i \<in> I" "f i \<in> T" "openin (X i) T" "S i \<inter> T = {}"
    4.33 +      then have "openin (product_topology X I) ((\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> {x. x i \<in> T})"
    4.34 +        by (force simp: openin_product_topology intro: arbitrary_union_of_inc relative_to_inc finite_intersection_of_inc)
    4.35 +      then show "False"
    4.36 +        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>
    4.37 +        by (auto simp: top ext PiE_iff)
    4.38 +    qed
    4.39 +  next
    4.40 +    assume R [rule_format]: ?rhs
    4.41 +    show ?lhs
    4.42 +    proof (clarsimp simp: openin_product_topology union_of_def arbitrary_def)
    4.43 +      fix \<U> U
    4.44 +      assume
    4.45 +        \<U>: "\<U> \<subseteq> Collect
    4.46 +           (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
    4.47 +            (\<Pi>\<^sub>E i\<in>I. topspace (X i)))" and
    4.48 +        "f \<in> U" "U \<in> \<U>"
    4.49 +      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)
    4.50 +                 relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))) U"
    4.51 +        by blast
    4.52 +      with \<open>f \<in> U\<close> \<open>U \<in> \<U>\<close>
    4.53 +      obtain \<T> where "finite \<T>"
    4.54 +        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}"
    4.55 +        and "topspace (product_topology X I) \<inter> \<Inter> \<T> \<subseteq> U" "f \<in> topspace (product_topology X I) \<inter> \<Inter> \<T>"
    4.56 +        apply (clarsimp simp add: relative_to_def intersection_of_def)
    4.57 +        apply (rule that, auto dest!: subsetD)
    4.58 +        done
    4.59 +      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"
    4.60 +        by (auto simp: PiE_iff)
    4.61 +      have *: "f i \<in> topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}
    4.62 +             \<and> openin (X i) (topspace (X i) \<inter> \<Inter>{U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>})"
    4.63 +        if "i \<in> I" for i
    4.64 +      proof -
    4.65 +        have "finite ((\<lambda>U. {x. x i \<in> U}) -` \<T>)"
    4.66 +        proof (rule finite_vimageI [OF \<open>finite \<T>\<close>])
    4.67 +          show "inj (\<lambda>U. {x. x i \<in> U})"
    4.68 +            by (auto simp: inj_on_def)
    4.69 +        qed
    4.70 +        then have fin: "finite {U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}"
    4.71 +          by (rule rev_finite_subset) auto
    4.72 +        have "openin (X i) (\<Inter> (insert (topspace (X i)) {U. openin (X i) U \<and> {x. x i \<in> U} \<in> \<T>}))"
    4.73 +          by (rule openin_Inter) (auto simp: fin)
    4.74 +        then show ?thesis
    4.75 +          using \<open>f \<in> \<Inter> \<T>\<close> by (fastforce simp: that top)
    4.76 +      qed
    4.77 +      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>}"
    4.78 +      have "\<forall>i \<in> I. \<exists>x. x \<in> S i \<inter> \<Phi> i"
    4.79 +        using R [OF _ *] unfolding \<Phi>_def by blast
    4.80 +      then obtain \<theta> where \<theta> [rule_format]: "\<forall>i \<in> I. \<theta> i \<in> S i \<inter> \<Phi> i"
    4.81 +        by metis
    4.82 +      show "\<exists>y\<in>Pi\<^sub>E I S. \<exists>x\<in>\<U>. y \<in> x"
    4.83 +      proof
    4.84 +        show "\<exists>U \<in> \<U>. (\<lambda>i \<in> I. \<theta> i) \<in> U"
    4.85 +        proof
    4.86 +          have "restrict \<theta> I \<in> PiE I (topspace \<circ> X) \<inter> \<Inter>\<T>"
    4.87 +            using \<T> by (fastforce simp: \<Phi>_def PiE_def dest: \<theta>)
    4.88 +          then show "restrict \<theta> I \<in> U"
    4.89 +            using subU by blast
    4.90 +        qed (rule \<open>U \<in> \<U>\<close>)
    4.91 +      next
    4.92 +        show "(\<lambda>i \<in> I. \<theta> i) \<in> Pi\<^sub>E I S"
    4.93 +          using \<theta> by simp
    4.94 +      qed
    4.95 +    qed
    4.96 +  qed
    4.97 +  show ?thesis
    4.98 +    apply (simp add: * closure_of_def PiE_iff set_eq_iff cong: conj_cong)
    4.99 +    by metis
   4.100 +qed
   4.101  
   4.102 -lemma openin_product_topology_alt:
   4.103 -  "openin (product_topology X I) S \<longleftrightarrow>
   4.104 -    (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
   4.105 -                 (\<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)"
   4.106 -  apply (simp add: openin_product_topology arbitrary_union_of_alt product_topology_base_alt, auto)
   4.107 -  apply (drule bspec; blast)
   4.108 +corollary closedin_product_topology:
   4.109 +   "closedin (product_topology X I) (PiE I S) \<longleftrightarrow> PiE I S = {} \<or> (\<forall>i \<in> I. closedin (X i) (S i))"
   4.110 +  apply (simp add: PiE_eq PiE_eq_empty_iff closure_of_product_topology flip: closure_of_eq)
   4.111 +  apply (metis closure_of_empty)
   4.112    done
   4.113  
   4.114 +corollary closedin_product_topology_singleton:
   4.115 +   "f \<in> extensional I \<Longrightarrow> closedin (product_topology X I) {f} \<longleftrightarrow> (\<forall>i \<in> I. closedin (X i) {f i})"
   4.116 +  using PiE_singleton closedin_product_topology [of X I]
   4.117 +  by (metis (no_types, lifting) all_not_in_conv insertI1)
   4.118  
   4.119 -text \<open>The basic property of the product topology is the continuity of projections:\<close>
   4.120 +
   4.121 +subsubsection \<open>The basic property of the product topology is the continuity of projections:\<close>
   4.122  
   4.123  lemma continuous_on_topo_product_coordinates [simp]:
   4.124    assumes "i \<in> I"
     5.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Wed Mar 06 21:44:30 2019 +0100
     5.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Mar 07 14:08:05 2019 +0000
     5.3 @@ -242,6 +242,27 @@
     5.4    shows "path_connected {a..b}"
     5.5    using is_interval_cc is_interval_path_connected by blast
     5.6  
     5.7 +lemma path_connected_Ioi[simp]: "path_connected {a<..}" for a :: real
     5.8 +  by (simp add: convex_imp_path_connected)
     5.9 +
    5.10 +lemma path_connected_Ici[simp]: "path_connected {a..}" for a :: real
    5.11 +  by (simp add: convex_imp_path_connected)
    5.12 +
    5.13 +lemma path_connected_Iio[simp]: "path_connected {..<a}" for a :: real
    5.14 +  by (simp add: convex_imp_path_connected)
    5.15 +
    5.16 +lemma path_connected_Iic[simp]: "path_connected {..a}" for a :: real
    5.17 +  by (simp add: convex_imp_path_connected)
    5.18 +
    5.19 +lemma path_connected_Ioo[simp]: "path_connected {a<..<b}" for a b :: real
    5.20 +  by (simp add: convex_imp_path_connected)
    5.21 +
    5.22 +lemma path_connected_Ioc[simp]: "path_connected {a<..b}" for a b :: real
    5.23 +  by (simp add: convex_imp_path_connected)
    5.24 +
    5.25 +lemma path_connected_Ico[simp]: "path_connected {a..<b}" for a b :: real
    5.26 +  by (simp add: convex_imp_path_connected)
    5.27 +
    5.28  lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
    5.29    by (auto simp: real_atLeastGreaterThan_eq)
    5.30  
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Analysis/T1_Spaces.thy	Thu Mar 07 14:08:05 2019 +0000
     6.3 @@ -0,0 +1,201 @@
     6.4 +section\<open>T1 spaces with equivalences to many naturally "nice" properties. \<close>
     6.5 +
     6.6 +theory T1_Spaces
     6.7 +imports Function_Topology 
     6.8 +begin
     6.9 +
    6.10 +definition t1_space where
    6.11 + "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)"
    6.12 +
    6.13 +lemma t1_space_expansive:
    6.14 +   "\<lbrakk>topspace Y = topspace X; \<And>U. openin X U \<Longrightarrow> openin Y U\<rbrakk> \<Longrightarrow> t1_space X \<Longrightarrow> t1_space Y"
    6.15 +  by (metis t1_space_def)
    6.16 +
    6.17 +lemma t1_space_alt:
    6.18 +   "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))"
    6.19 + by (metis DiffE DiffI closedin_def openin_closedin_eq t1_space_def)
    6.20 +
    6.21 +lemma t1_space_empty: "topspace X = {} \<Longrightarrow> t1_space X"
    6.22 +  by (simp add: t1_space_def)
    6.23 +
    6.24 +lemma t1_space_derived_set_of_singleton:
    6.25 +  "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. X derived_set_of {x} = {})"
    6.26 +  apply (simp add: t1_space_def derived_set_of_def, safe)
    6.27 +   apply (metis openin_topspace)
    6.28 +  by force
    6.29 +
    6.30 +lemma t1_space_derived_set_of_finite:
    6.31 +   "t1_space X \<longleftrightarrow> (\<forall>S. finite S \<longrightarrow> X derived_set_of S = {})"
    6.32 +proof (intro iffI allI impI)
    6.33 +  fix S :: "'a set"
    6.34 +  assume "finite S"
    6.35 +  then have fin: "finite ((\<lambda>x. {x}) ` (topspace X \<inter> S))"
    6.36 +    by blast
    6.37 +  assume "t1_space X"
    6.38 +  then have "X derived_set_of (\<Union>x \<in> topspace X \<inter> S. {x}) = {}"
    6.39 +    unfolding derived_set_of_Union [OF fin]
    6.40 +    by (auto simp: t1_space_derived_set_of_singleton)
    6.41 +  then have "X derived_set_of (topspace X \<inter> S) = {}"
    6.42 +    by simp
    6.43 +  then show "X derived_set_of S = {}"
    6.44 +    by simp
    6.45 +qed (auto simp: t1_space_derived_set_of_singleton)
    6.46 +
    6.47 +lemma t1_space_closedin_singleton:
    6.48 +   "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. closedin X {x})"
    6.49 +  apply (rule iffI)
    6.50 +  apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_singleton)
    6.51 +  using t1_space_alt by auto
    6.52 +
    6.53 +lemma closedin_t1_singleton:
    6.54 +   "\<lbrakk>t1_space X; a \<in> topspace X\<rbrakk> \<Longrightarrow> closedin X {a}"
    6.55 +  by (simp add: t1_space_closedin_singleton)
    6.56 +
    6.57 +lemma t1_space_closedin_finite:
    6.58 +   "t1_space X \<longleftrightarrow> (\<forall>S. finite S \<and> S \<subseteq> topspace X \<longrightarrow> closedin X S)"
    6.59 +  apply (rule iffI)
    6.60 +  apply (simp add: closedin_contains_derived_set t1_space_derived_set_of_finite)
    6.61 +  by (simp add: t1_space_closedin_singleton)
    6.62 +
    6.63 +lemma closure_of_singleton:
    6.64 +   "t1_space X \<Longrightarrow> X closure_of {a} = (if a \<in> topspace X then {a} else {})"
    6.65 +  by (simp add: closure_of_eq t1_space_closedin_singleton closure_of_eq_empty_gen)
    6.66 +
    6.67 +lemma separated_in_singleton:
    6.68 +  assumes "t1_space X"
    6.69 +  shows "separatedin X {a} S \<longleftrightarrow> a \<in> topspace X \<and> S \<subseteq> topspace X \<and> (a \<notin> X closure_of S)"
    6.70 +        "separatedin X S {a} \<longleftrightarrow> a \<in> topspace X \<and> S \<subseteq> topspace X \<and> (a \<notin> X closure_of S)"
    6.71 +  unfolding separatedin_def
    6.72 +  using assms closure_of closure_of_singleton by fastforce+
    6.73 +
    6.74 +lemma t1_space_openin_delete:
    6.75 +   "t1_space X \<longleftrightarrow> (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> openin X (U - {x}))"
    6.76 +  apply (rule iffI)
    6.77 +  apply (meson closedin_t1_singleton in_mono openin_diff openin_subset)
    6.78 +  by (simp add: closedin_def t1_space_closedin_singleton)
    6.79 +
    6.80 +lemma t1_space_openin_delete_alt:
    6.81 +   "t1_space X \<longleftrightarrow> (\<forall>U x. openin X U \<longrightarrow> openin X (U - {x}))"
    6.82 +  by (metis Diff_empty Diff_insert0 t1_space_openin_delete)
    6.83 +
    6.84 +
    6.85 +lemma t1_space_singleton_Inter_open:
    6.86 +      "t1_space X \<longleftrightarrow> (\<forall>x \<in> topspace X. \<Inter>{U. openin X U \<and> x \<in> U} = {x})"  (is "?P=?Q")
    6.87 +  and t1_space_Inter_open_supersets:
    6.88 +     "t1_space X \<longleftrightarrow> (\<forall>S. S \<subseteq> topspace X \<longrightarrow> \<Inter>{U. openin X U \<and> S \<subseteq> U} = S)" (is "?P=?R")
    6.89 +proof -
    6.90 +  have "?R \<Longrightarrow> ?Q"
    6.91 +    apply clarify
    6.92 +    apply (drule_tac x="{x}" in spec, simp)
    6.93 +    done
    6.94 +  moreover have "?Q \<Longrightarrow> ?P"
    6.95 +    apply (clarsimp simp add: t1_space_def)
    6.96 +    apply (drule_tac x=x in bspec)
    6.97 +     apply (simp_all add: set_eq_iff)
    6.98 +    by (metis (no_types, lifting))
    6.99 +  moreover have "?P \<Longrightarrow> ?R"
   6.100 +  proof (clarsimp simp add: t1_space_closedin_singleton, rule subset_antisym)
   6.101 +    fix S
   6.102 +    assume S: "\<forall>x\<in>topspace X. closedin X {x}" "S \<subseteq> topspace X"
   6.103 +    then show "\<Inter> {U. openin X U \<and> S \<subseteq> U} \<subseteq> S"
   6.104 +      apply clarsimp
   6.105 +      by (metis Diff_insert_absorb Set.set_insert closedin_def openin_topspace subset_insert)
   6.106 +  qed force
   6.107 +  ultimately show "?P=?Q" "?P=?R"
   6.108 +    by auto
   6.109 +qed
   6.110 +
   6.111 +lemma t1_space_derived_set_of_infinite_openin:
   6.112 +   "t1_space X \<longleftrightarrow>
   6.113 +        (\<forall>S. X derived_set_of S =
   6.114 +             {x \<in> topspace X. \<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite(S \<inter> U)})"
   6.115 +         (is "_ = ?rhs")
   6.116 +proof
   6.117 +  assume "t1_space X"
   6.118 +  show ?rhs
   6.119 +  proof safe
   6.120 +    fix S x U
   6.121 +    assume "x \<in> X derived_set_of S" "x \<in> U" "openin X U" "finite (S \<inter> U)"
   6.122 +    with \<open>t1_space X\<close> show "False"
   6.123 +      apply (simp add: t1_space_derived_set_of_finite)
   6.124 +      by (metis IntI empty_iff empty_subsetI inf_commute openin_Int_derived_set_of_subset subset_antisym)
   6.125 +  next
   6.126 +    fix S x
   6.127 +    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
   6.128 +      by blast
   6.129 +    assume "x \<in> topspace X" "\<forall>U. x \<in> U \<and> openin X U \<longrightarrow> infinite (S \<inter> U)"
   6.130 +    then show "x \<in> X derived_set_of S"
   6.131 +      apply (clarsimp simp add: derived_set_of_def eq)
   6.132 +      by (meson finite.emptyI finite.insertI finite_subset)
   6.133 +  qed (auto simp: in_derived_set_of)
   6.134 +qed (auto simp: t1_space_derived_set_of_singleton)
   6.135 +
   6.136 +lemma finite_t1_space_imp_discrete_topology:
   6.137 +   "\<lbrakk>topspace X = U; finite U; t1_space X\<rbrakk> \<Longrightarrow> X = discrete_topology U"
   6.138 +  by (metis discrete_topology_unique_derived_set t1_space_derived_set_of_finite)
   6.139 +
   6.140 +lemma t1_space_subtopology: "t1_space X \<Longrightarrow> t1_space(subtopology X U)"
   6.141 +  by (simp add: derived_set_of_subtopology t1_space_derived_set_of_finite)
   6.142 +
   6.143 +lemma closedin_derived_set_of_gen:
   6.144 +   "t1_space X \<Longrightarrow> closedin X (X derived_set_of S)"
   6.145 +  apply (clarsimp simp add: in_derived_set_of closedin_contains_derived_set derived_set_of_subset_topspace)
   6.146 +  by (metis DiffD2 insert_Diff insert_iff t1_space_openin_delete)
   6.147 +
   6.148 +lemma derived_set_of_derived_set_subset_gen:
   6.149 +   "t1_space X \<Longrightarrow> X derived_set_of (X derived_set_of S) \<subseteq> X derived_set_of S"
   6.150 +  by (meson closedin_contains_derived_set closedin_derived_set_of_gen)
   6.151 +
   6.152 +lemma subtopology_eq_discrete_topology_gen_finite:
   6.153 +   "\<lbrakk>t1_space X; finite S\<rbrakk> \<Longrightarrow> subtopology X S = discrete_topology(topspace X \<inter> S)"
   6.154 +  by (simp add: subtopology_eq_discrete_topology_gen t1_space_derived_set_of_finite)
   6.155 +
   6.156 +lemma subtopology_eq_discrete_topology_finite:
   6.157 +   "\<lbrakk>t1_space X; S \<subseteq> topspace X; finite S\<rbrakk>
   6.158 +        \<Longrightarrow> subtopology X S = discrete_topology S"
   6.159 +  by (simp add: subtopology_eq_discrete_topology_eq t1_space_derived_set_of_finite)
   6.160 +
   6.161 +lemma t1_space_closed_map_image:
   6.162 +   "\<lbrakk>closed_map X Y f; f ` (topspace X) = topspace Y; t1_space X\<rbrakk> \<Longrightarrow> t1_space Y"
   6.163 +  by (metis closed_map_def finite_subset_image t1_space_closedin_finite)
   6.164 +
   6.165 +lemma homeomorphic_t1_space: "X homeomorphic_space Y \<Longrightarrow> (t1_space X \<longleftrightarrow> t1_space Y)"
   6.166 +  apply (clarsimp simp add: homeomorphic_space_def)
   6.167 +  by (meson homeomorphic_eq_everything_map homeomorphic_maps_map t1_space_closed_map_image)
   6.168 +
   6.169 +proposition t1_space_product_topology:
   6.170 +   "t1_space (product_topology X I)
   6.171 +\<longleftrightarrow> topspace(product_topology X I) = {} \<or> (\<forall>i \<in> I. t1_space (X i))"
   6.172 +proof (cases "topspace(product_topology X I) = {}")
   6.173 +  case True
   6.174 +  then show ?thesis
   6.175 +    using True t1_space_empty by blast
   6.176 +next
   6.177 +  case False
   6.178 +  then obtain f where f: "f \<in> (\<Pi>\<^sub>E i\<in>I. topspace(X i))"
   6.179 +    by fastforce
   6.180 +  have "t1_space (product_topology X I) \<longleftrightarrow> (\<forall>i\<in>I. t1_space (X i))"
   6.181 +  proof (intro iffI ballI)
   6.182 +    show "t1_space (X i)" if "t1_space (product_topology X I)" and "i \<in> I" for i
   6.183 +    proof -
   6.184 +      have clo: "\<And>h. h \<in> (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<Longrightarrow> closedin (product_topology X I) {h}"
   6.185 +        using that by (simp add: t1_space_closedin_singleton)
   6.186 +      show ?thesis
   6.187 +        unfolding t1_space_closedin_singleton
   6.188 +      proof clarify
   6.189 +        show "closedin (X i) {xi}" if "xi \<in> topspace (X i)" for xi
   6.190 +          using clo [of "\<lambda>j \<in> I. if i=j then xi else f j"] f that \<open>i \<in> I\<close>
   6.191 +          by (fastforce simp add: closedin_product_topology_singleton)
   6.192 +      qed
   6.193 +    qed
   6.194 +  next
   6.195 +  next
   6.196 +    show "t1_space (product_topology X I)" if "\<forall>i\<in>I. t1_space (X i)"
   6.197 +      using that
   6.198 +      by (simp add: t1_space_closedin_singleton Ball_def PiE_iff closedin_product_topology_singleton)
   6.199 +  qed
   6.200 +  then show ?thesis
   6.201 +    using False by blast
   6.202 +qed
   6.203 +
   6.204 +end
     7.1 --- a/src/HOL/Library/Equipollence.thy	Wed Mar 06 21:44:30 2019 +0100
     7.2 +++ b/src/HOL/Library/Equipollence.thy	Thu Mar 07 14:08:05 2019 +0000
     7.3 @@ -82,7 +82,6 @@
     7.4    apply (simp add: infinite_countable_subset)
     7.5    using infinite_iff_countable_subset by blast
     7.6  
     7.7 -
     7.8  lemma bij_betw_iff_bijections:
     7.9    "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))"
    7.10    (is "?lhs = ?rhs")
    7.11 @@ -114,9 +113,23 @@
    7.12      using * by (auto simp: image_def)
    7.13  qed
    7.14  
    7.15 +lemma singleton_lepoll: "{x} \<lesssim> insert y A"
    7.16 +  by (force simp: lepoll_def)
    7.17 +
    7.18 +lemma singleton_eqpoll: "{x} \<approx> {y}"
    7.19 +  by (blast intro: lepoll_antisym singleton_lepoll)
    7.20 +
    7.21 +lemma subset_singleton_iff_lepoll: "(\<exists>x. S \<subseteq> {x}) \<longleftrightarrow> S \<lesssim> {()}"
    7.22 +proof safe
    7.23 +  show "S \<lesssim> {()}" if "S \<subseteq> {x}" for x
    7.24 +    using subset_imp_lepoll [OF that] by (simp add: singleton_eqpoll lepoll_trans2)
    7.25 +  show "\<exists>x. S \<subseteq> {x}" if "S \<lesssim> {()}"
    7.26 +  by (metis (no_types, hide_lams) image_empty image_insert lepoll_iff that)
    7.27 +qed
    7.28 +
    7.29 +
    7.30  subsection\<open>The strict relation\<close>
    7.31  
    7.32 -
    7.33  lemma lesspoll_not_refl [iff]: "~ (i \<prec> i)"
    7.34    by (simp add: lepoll_antisym lesspoll_def)
    7.35