src/HOL/Analysis/Elementary_Topology.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 months ago) changeset 69981 3dced198b9ec parent 69768 7e4966eaf781 child 70044 da5857dbcbb9 permissions -rw-r--r--
more strict AFP properties;
```     1 (*  Author:     L C Paulson, University of Cambridge
```
```     2     Author:     Amine Chaieb, University of Cambridge
```
```     3     Author:     Robert Himmelmann, TU Muenchen
```
```     4     Author:     Brian Huffman, Portland State University
```
```     5 *)
```
```     6
```
```     7 chapter \<open>Topology\<close>
```
```     8
```
```     9 theory Elementary_Topology
```
```    10 imports
```
```    11   "HOL-Library.Set_Idioms"
```
```    12   "HOL-Library.Disjoint_Sets"
```
```    13   Product_Vector
```
```    14 begin
```
```    15
```
```    16
```
```    17 section \<open>Elementary Topology\<close>
```
```    18
```
```    19 subsection \<open>TODO: move?\<close>
```
```    20
```
```    21 lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
```
```    22   using openI by auto
```
```    23
```
```    24
```
```    25 subsubsection%unimportant \<open>Archimedean properties and useful consequences\<close>
```
```    26
```
```    27 text\<open>Bernoulli's inequality\<close>
```
```    28 proposition Bernoulli_inequality:
```
```    29   fixes x :: real
```
```    30   assumes "-1 \<le> x"
```
```    31     shows "1 + n * x \<le> (1 + x) ^ n"
```
```    32 proof (induct n)
```
```    33   case 0
```
```    34   then show ?case by simp
```
```    35 next
```
```    36   case (Suc n)
```
```    37   have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
```
```    38     by (simp add: algebra_simps)
```
```    39   also have "... = (1 + x) * (1 + n*x)"
```
```    40     by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
```
```    41   also have "... \<le> (1 + x) ^ Suc n"
```
```    42     using Suc.hyps assms mult_left_mono by fastforce
```
```    43   finally show ?case .
```
```    44 qed
```
```    45
```
```    46 corollary Bernoulli_inequality_even:
```
```    47   fixes x :: real
```
```    48   assumes "even n"
```
```    49     shows "1 + n * x \<le> (1 + x) ^ n"
```
```    50 proof (cases "-1 \<le> x \<or> n=0")
```
```    51   case True
```
```    52   then show ?thesis
```
```    53     by (auto simp: Bernoulli_inequality)
```
```    54 next
```
```    55   case False
```
```    56   then have "real n \<ge> 1"
```
```    57     by simp
```
```    58   with False have "n * x \<le> -1"
```
```    59     by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
```
```    60   then have "1 + n * x \<le> 0"
```
```    61     by auto
```
```    62   also have "... \<le> (1 + x) ^ n"
```
```    63     using assms
```
```    64     using zero_le_even_power by blast
```
```    65   finally show ?thesis .
```
```    66 qed
```
```    67
```
```    68 corollary real_arch_pow:
```
```    69   fixes x :: real
```
```    70   assumes x: "1 < x"
```
```    71   shows "\<exists>n. y < x^n"
```
```    72 proof -
```
```    73   from x have x0: "x - 1 > 0"
```
```    74     by arith
```
```    75   from reals_Archimedean3[OF x0, rule_format, of y]
```
```    76   obtain n :: nat where n: "y < real n * (x - 1)" by metis
```
```    77   from x0 have x00: "x- 1 \<ge> -1" by arith
```
```    78   from Bernoulli_inequality[OF x00, of n] n
```
```    79   have "y < x^n" by auto
```
```    80   then show ?thesis by metis
```
```    81 qed
```
```    82
```
```    83 corollary real_arch_pow_inv:
```
```    84   fixes x y :: real
```
```    85   assumes y: "y > 0"
```
```    86     and x1: "x < 1"
```
```    87   shows "\<exists>n. x^n < y"
```
```    88 proof (cases "x > 0")
```
```    89   case True
```
```    90   with x1 have ix: "1 < 1/x" by (simp add: field_simps)
```
```    91   from real_arch_pow[OF ix, of "1/y"]
```
```    92   obtain n where n: "1/y < (1/x)^n" by blast
```
```    93   then show ?thesis using y \<open>x > 0\<close>
```
```    94     by (auto simp add: field_simps)
```
```    95 next
```
```    96   case False
```
```    97   with y x1 show ?thesis
```
```    98     by (metis less_le_trans not_less power_one_right)
```
```    99 qed
```
```   100
```
```   101 lemma forall_pos_mono:
```
```   102   "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
```
```   103     (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
```
```   104   by (metis real_arch_inverse)
```
```   105
```
```   106 lemma forall_pos_mono_1:
```
```   107   "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
```
```   108     (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
```
```   109   apply (rule forall_pos_mono)
```
```   110   apply auto
```
```   111   apply (metis Suc_pred of_nat_Suc)
```
```   112   done
```
```   113
```
```   114 subsubsection%unimportant \<open>Affine transformations of intervals\<close>
```
```   115
```
```   116 lemma real_affinity_le: "0 < m \<Longrightarrow> m * x + c \<le> y \<longleftrightarrow> x \<le> inverse m * y + - (c / m)"
```
```   117   for m :: "'a::linordered_field"
```
```   118   by (simp add: field_simps)
```
```   119
```
```   120 lemma real_le_affinity: "0 < m \<Longrightarrow> y \<le> m * x + c \<longleftrightarrow> inverse m * y + - (c / m) \<le> x"
```
```   121   for m :: "'a::linordered_field"
```
```   122   by (simp add: field_simps)
```
```   123
```
```   124 lemma real_affinity_lt: "0 < m \<Longrightarrow> m * x + c < y \<longleftrightarrow> x < inverse m * y + - (c / m)"
```
```   125   for m :: "'a::linordered_field"
```
```   126   by (simp add: field_simps)
```
```   127
```
```   128 lemma real_lt_affinity: "0 < m \<Longrightarrow> y < m * x + c \<longleftrightarrow> inverse m * y + - (c / m) < x"
```
```   129   for m :: "'a::linordered_field"
```
```   130   by (simp add: field_simps)
```
```   131
```
```   132 lemma real_affinity_eq: "m \<noteq> 0 \<Longrightarrow> m * x + c = y \<longleftrightarrow> x = inverse m * y + - (c / m)"
```
```   133   for m :: "'a::linordered_field"
```
```   134   by (simp add: field_simps)
```
```   135
```
```   136 lemma real_eq_affinity: "m \<noteq> 0 \<Longrightarrow> y = m * x + c  \<longleftrightarrow> inverse m * y + - (c / m) = x"
```
```   137   for m :: "'a::linordered_field"
```
```   138   by (simp add: field_simps)
```
```   139
```
```   140
```
```   141
```
```   142 subsection \<open>Topological Basis\<close>
```
```   143
```
```   144 context topological_space
```
```   145 begin
```
```   146
```
```   147 definition%important "topological_basis B \<longleftrightarrow>
```
```   148   (\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
```
```   149
```
```   150 lemma topological_basis:
```
```   151   "topological_basis B \<longleftrightarrow> (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
```
```   152   unfolding topological_basis_def
```
```   153   apply safe
```
```   154      apply fastforce
```
```   155     apply fastforce
```
```   156    apply (erule_tac x=x in allE, simp)
```
```   157    apply (rule_tac x="{x}" in exI, auto)
```
```   158   done
```
```   159
```
```   160 lemma topological_basis_iff:
```
```   161   assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
```
```   162   shows "topological_basis B \<longleftrightarrow> (\<forall>O'. open O' \<longrightarrow> (\<forall>x\<in>O'. \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'))"
```
```   163     (is "_ \<longleftrightarrow> ?rhs")
```
```   164 proof safe
```
```   165   fix O' and x::'a
```
```   166   assume H: "topological_basis B" "open O'" "x \<in> O'"
```
```   167   then have "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def)
```
```   168   then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto
```
```   169   then show "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto
```
```   170 next
```
```   171   assume H: ?rhs
```
```   172   show "topological_basis B"
```
```   173     using assms unfolding topological_basis_def
```
```   174   proof safe
```
```   175     fix O' :: "'a set"
```
```   176     assume "open O'"
```
```   177     with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'"
```
```   178       by (force intro: bchoice simp: Bex_def)
```
```   179     then show "\<exists>B'\<subseteq>B. \<Union>B' = O'"
```
```   180       by (auto intro: exI[where x="{f x |x. x \<in> O'}"])
```
```   181   qed
```
```   182 qed
```
```   183
```
```   184 lemma topological_basisI:
```
```   185   assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
```
```   186     and "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'"
```
```   187   shows "topological_basis B"
```
```   188   using assms by (subst topological_basis_iff) auto
```
```   189
```
```   190 lemma topological_basisE:
```
```   191   fixes O'
```
```   192   assumes "topological_basis B"
```
```   193     and "open O'"
```
```   194     and "x \<in> O'"
```
```   195   obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'"
```
```   196 proof atomize_elim
```
```   197   from assms have "\<And>B'. B'\<in>B \<Longrightarrow> open B'"
```
```   198     by (simp add: topological_basis_def)
```
```   199   with topological_basis_iff assms
```
```   200   show  "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'"
```
```   201     using assms by (simp add: Bex_def)
```
```   202 qed
```
```   203
```
```   204 lemma topological_basis_open:
```
```   205   assumes "topological_basis B"
```
```   206     and "X \<in> B"
```
```   207   shows "open X"
```
```   208   using assms by (simp add: topological_basis_def)
```
```   209
```
```   210 lemma topological_basis_imp_subbasis:
```
```   211   assumes B: "topological_basis B"
```
```   212   shows "open = generate_topology B"
```
```   213 proof (intro ext iffI)
```
```   214   fix S :: "'a set"
```
```   215   assume "open S"
```
```   216   with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'"
```
```   217     unfolding topological_basis_def by blast
```
```   218   then show "generate_topology B S"
```
```   219     by (auto intro: generate_topology.intros dest: topological_basis_open)
```
```   220 next
```
```   221   fix S :: "'a set"
```
```   222   assume "generate_topology B S"
```
```   223   then show "open S"
```
```   224     by induct (auto dest: topological_basis_open[OF B])
```
```   225 qed
```
```   226
```
```   227 lemma basis_dense:
```
```   228   fixes B :: "'a set set"
```
```   229     and f :: "'a set \<Rightarrow> 'a"
```
```   230   assumes "topological_basis B"
```
```   231     and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
```
```   232   shows "\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X)"
```
```   233 proof (intro allI impI)
```
```   234   fix X :: "'a set"
```
```   235   assume "open X" and "X \<noteq> {}"
```
```   236   from topological_basisE[OF \<open>topological_basis B\<close> \<open>open X\<close> choosefrom_basis[OF \<open>X \<noteq> {}\<close>]]
```
```   237   obtain B' where "B' \<in> B" "f X \<in> B'" "B' \<subseteq> X" .
```
```   238   then show "\<exists>B'\<in>B. f B' \<in> X"
```
```   239     by (auto intro!: choosefrom_basis)
```
```   240 qed
```
```   241
```
```   242 end
```
```   243
```
```   244 lemma topological_basis_prod:
```
```   245   assumes A: "topological_basis A"
```
```   246     and B: "topological_basis B"
```
```   247   shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
```
```   248   unfolding topological_basis_def
```
```   249 proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
```
```   250   fix S :: "('a \<times> 'b) set"
```
```   251   assume "open S"
```
```   252   then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
```
```   253   proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
```
```   254     fix x y
```
```   255     assume "(x, y) \<in> S"
```
```   256     from open_prod_elim[OF \<open>open S\<close> this]
```
```   257     obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
```
```   258       by (metis mem_Sigma_iff)
```
```   259     moreover
```
```   260     from A a obtain A0 where "A0 \<in> A" "x \<in> A0" "A0 \<subseteq> a"
```
```   261       by (rule topological_basisE)
```
```   262     moreover
```
```   263     from B b obtain B0 where "B0 \<in> B" "y \<in> B0" "B0 \<subseteq> b"
```
```   264       by (rule topological_basisE)
```
```   265     ultimately show "(x, y) \<in> (\<Union>(a, b)\<in>{X \<in> A \<times> B. fst X \<times> snd X \<subseteq> S}. a \<times> b)"
```
```   266       by (intro UN_I[of "(A0, B0)"]) auto
```
```   267   qed auto
```
```   268 qed (metis A B topological_basis_open open_Times)
```
```   269
```
```   270
```
```   271 subsection \<open>Countable Basis\<close>
```
```   272
```
```   273 locale%important countable_basis = topological_space p for p::"'a set \<Rightarrow> bool" +
```
```   274   fixes B :: "'a set set"
```
```   275   assumes is_basis: "topological_basis B"
```
```   276     and countable_basis: "countable B"
```
```   277 begin
```
```   278
```
```   279 lemma open_countable_basis_ex:
```
```   280   assumes "p X"
```
```   281   shows "\<exists>B' \<subseteq> B. X = \<Union>B'"
```
```   282   using assms countable_basis is_basis
```
```   283   unfolding topological_basis_def by blast
```
```   284
```
```   285 lemma open_countable_basisE:
```
```   286   assumes "p X"
```
```   287   obtains B' where "B' \<subseteq> B" "X = \<Union>B'"
```
```   288   using assms open_countable_basis_ex
```
```   289   by atomize_elim simp
```
```   290
```
```   291 lemma countable_dense_exists:
```
```   292   "\<exists>D::'a set. countable D \<and> (\<forall>X. p X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
```
```   293 proof -
```
```   294   let ?f = "(\<lambda>B'. SOME x. x \<in> B')"
```
```   295   have "countable (?f ` B)" using countable_basis by simp
```
```   296   with basis_dense[OF is_basis, of ?f] show ?thesis
```
```   297     by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI)
```
```   298 qed
```
```   299
```
```   300 lemma countable_dense_setE:
```
```   301   obtains D :: "'a set"
```
```   302   where "countable D" "\<And>X. p X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X"
```
```   303   using countable_dense_exists by blast
```
```   304
```
```   305 end
```
```   306
```
```   307 lemma countable_basis_openI: "countable_basis open B"
```
```   308   if "countable B" "topological_basis B"
```
```   309   using that
```
```   310   by unfold_locales
```
```   311     (simp_all add: topological_basis topological_space.topological_basis topological_space_axioms)
```
```   312
```
```   313 lemma (in first_countable_topology) first_countable_basisE:
```
```   314   fixes x :: 'a
```
```   315   obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
```
```   316     "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)"
```
```   317 proof -
```
```   318   obtain \<A> where \<A>: "(\<forall>i::nat. x \<in> \<A> i \<and> open (\<A> i))" "(\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> S))"
```
```   319     using first_countable_basis[of x] by metis
```
```   320   show thesis
```
```   321   proof
```
```   322     show "countable (range \<A>)"
```
```   323       by simp
```
```   324   qed (use \<A> in auto)
```
```   325 qed
```
```   326
```
```   327 lemma (in first_countable_topology) first_countable_basis_Int_stableE:
```
```   328   obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
```
```   329     "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)"
```
```   330     "\<And>A B. A \<in> \<A> \<Longrightarrow> B \<in> \<A> \<Longrightarrow> A \<inter> B \<in> \<A>"
```
```   331 proof atomize_elim
```
```   332   obtain \<B> where \<B>:
```
```   333     "countable \<B>"
```
```   334     "\<And>B. B \<in> \<B> \<Longrightarrow> x \<in> B"
```
```   335     "\<And>B. B \<in> \<B> \<Longrightarrow> open B"
```
```   336     "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>B\<in>\<B>. B \<subseteq> S"
```
```   337     by (rule first_countable_basisE) blast
```
```   338   define \<A> where [abs_def]:
```
```   339     "\<A> = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into \<B> n) ` N)) ` (Collect finite::nat set set)"
```
```   340   then show "\<exists>\<A>. countable \<A> \<and> (\<forall>A. A \<in> \<A> \<longrightarrow> x \<in> A) \<and> (\<forall>A. A \<in> \<A> \<longrightarrow> open A) \<and>
```
```   341         (\<forall>S. open S \<longrightarrow> x \<in> S \<longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)) \<and> (\<forall>A B. A \<in> \<A> \<longrightarrow> B \<in> \<A> \<longrightarrow> A \<inter> B \<in> \<A>)"
```
```   342   proof (safe intro!: exI[where x=\<A>])
```
```   343     show "countable \<A>"
```
```   344       unfolding \<A>_def by (intro countable_image countable_Collect_finite)
```
```   345     fix A
```
```   346     assume "A \<in> \<A>"
```
```   347     then show "x \<in> A" "open A"
```
```   348       using \<B>(4)[OF open_UNIV] by (auto simp: \<A>_def intro: \<B> from_nat_into)
```
```   349   next
```
```   350     let ?int = "\<lambda>N. \<Inter>(from_nat_into \<B> ` N)"
```
```   351     fix A B
```
```   352     assume "A \<in> \<A>" "B \<in> \<A>"
```
```   353     then obtain N M where "A = ?int N" "B = ?int M" "finite (N \<union> M)"
```
```   354       by (auto simp: \<A>_def)
```
```   355     then show "A \<inter> B \<in> \<A>"
```
```   356       by (auto simp: \<A>_def intro!: image_eqI[where x="N \<union> M"])
```
```   357   next
```
```   358     fix S
```
```   359     assume "open S" "x \<in> S"
```
```   360     then obtain a where a: "a\<in>\<B>" "a \<subseteq> S" using \<B> by blast
```
```   361     then show "\<exists>a\<in>\<A>. a \<subseteq> S" using a \<B>
```
```   362       by (intro bexI[where x=a]) (auto simp: \<A>_def intro: image_eqI[where x="{to_nat_on \<B> a}"])
```
```   363   qed
```
```   364 qed
```
```   365
```
```   366 lemma (in topological_space) first_countableI:
```
```   367   assumes "countable \<A>"
```
```   368     and 1: "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
```
```   369     and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>A\<in>\<A>. A \<subseteq> S"
```
```   370   shows "\<exists>\<A>::nat \<Rightarrow> 'a set. (\<forall>i. x \<in> \<A> i \<and> open (\<A> i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> S))"
```
```   371 proof (safe intro!: exI[of _ "from_nat_into \<A>"])
```
```   372   fix i
```
```   373   have "\<A> \<noteq> {}" using 2[of UNIV] by auto
```
```   374   show "x \<in> from_nat_into \<A> i" "open (from_nat_into \<A> i)"
```
```   375     using range_from_nat_into_subset[OF \<open>\<A> \<noteq> {}\<close>] 1 by auto
```
```   376 next
```
```   377   fix S
```
```   378   assume "open S" "x\<in>S" from 2[OF this]
```
```   379   show "\<exists>i. from_nat_into \<A> i \<subseteq> S"
```
```   380     using subset_range_from_nat_into[OF \<open>countable \<A>\<close>] by auto
```
```   381 qed
```
```   382
```
```   383 instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
```
```   384 proof
```
```   385   fix x :: "'a \<times> 'b"
```
```   386   obtain \<A> where \<A>:
```
```   387       "countable \<A>"
```
```   388       "\<And>a. a \<in> \<A> \<Longrightarrow> fst x \<in> a"
```
```   389       "\<And>a. a \<in> \<A> \<Longrightarrow> open a"
```
```   390       "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>\<A>. a \<subseteq> S"
```
```   391     by (rule first_countable_basisE[of "fst x"]) blast
```
```   392   obtain B where B:
```
```   393       "countable B"
```
```   394       "\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a"
```
```   395       "\<And>a. a \<in> B \<Longrightarrow> open a"
```
```   396       "\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S"
```
```   397     by (rule first_countable_basisE[of "snd x"]) blast
```
```   398   show "\<exists>\<A>::nat \<Rightarrow> ('a \<times> 'b) set.
```
```   399     (\<forall>i. x \<in> \<A> i \<and> open (\<A> i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. \<A> i \<subseteq> S))"
```
```   400   proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B)"], safe)
```
```   401     fix a b
```
```   402     assume x: "a \<in> \<A>" "b \<in> B"
```
```   403     show "x \<in> a \<times> b"
```
```   404       by (simp add: \<A>(2) B(2) mem_Times_iff x)
```
```   405     show "open (a \<times> b)"
```
```   406       by (simp add: \<A>(3) B(3) open_Times x)
```
```   407   next
```
```   408     fix S
```
```   409     assume "open S" "x \<in> S"
```
```   410     then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S"
```
```   411       by (rule open_prod_elim)
```
```   412     moreover
```
```   413     from a'b' \<A>(4)[of a'] B(4)[of b']
```
```   414     obtain a b where "a \<in> \<A>" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
```
```   415       by auto
```
```   416     ultimately
```
```   417     show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B). a \<subseteq> S"
```
```   418       by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
```
```   419   qed (simp add: \<A> B)
```
```   420 qed
```
```   421
```
```   422 class second_countable_topology = topological_space +
```
```   423   assumes ex_countable_subbasis:
```
```   424     "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
```
```   425 begin
```
```   426
```
```   427 lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B"
```
```   428 proof -
```
```   429   from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B"
```
```   430     by blast
```
```   431   let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }"
```
```   432
```
```   433   show ?thesis
```
```   434   proof (intro exI conjI)
```
```   435     show "countable ?B"
```
```   436       by (intro countable_image countable_Collect_finite_subset B)
```
```   437     {
```
```   438       fix S
```
```   439       assume "open S"
```
```   440       then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S"
```
```   441         unfolding B
```
```   442       proof induct
```
```   443         case UNIV
```
```   444         show ?case by (intro exI[of _ "{{}}"]) simp
```
```   445       next
```
```   446         case (Int a b)
```
```   447         then obtain x y where x: "a = \<Union>(Inter ` x)" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
```
```   448           and y: "b = \<Union>(Inter ` y)" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B"
```
```   449           by blast
```
```   450         show ?case
```
```   451           unfolding x y Int_UN_distrib2
```
```   452           by (intro exI[of _ "{i \<union> j| i j.  i \<in> x \<and> j \<in> y}"]) (auto dest: x(2) y(2))
```
```   453       next
```
```   454         case (UN K)
```
```   455         then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. \<Union> (Inter ` B') = k" by auto
```
```   456         then obtain k where
```
```   457             "\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> \<Union>(Inter ` (k ka)) = ka"
```
```   458           unfolding bchoice_iff ..
```
```   459         then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. \<Union> (Inter ` B') = \<Union>K"
```
```   460           by (intro exI[of _ "\<Union>(k ` K)"]) auto
```
```   461       next
```
```   462         case (Basis S)
```
```   463         then show ?case
```
```   464           by (intro exI[of _ "{{S}}"]) auto
```
```   465       qed
```
```   466       then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)"
```
```   467         unfolding subset_image_iff by blast }
```
```   468     then show "topological_basis ?B"
```
```   469       unfolding topological_basis_def
```
```   470       by (safe intro!: open_Inter)
```
```   471          (simp_all add: B generate_topology.Basis subset_eq)
```
```   472   qed
```
```   473 qed
```
```   474
```
```   475
```
```   476 end
```
```   477
```
```   478 lemma univ_second_countable:
```
```   479   obtains \<B> :: "'a::second_countable_topology set set"
```
```   480   where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
```
```   481        "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
```
```   482 by (metis ex_countable_basis topological_basis_def)
```
```   483
```
```   484 proposition Lindelof:
```
```   485   fixes \<F> :: "'a::second_countable_topology set set"
```
```   486   assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
```
```   487   obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
```
```   488 proof -
```
```   489   obtain \<B> :: "'a set set"
```
```   490     where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
```
```   491       and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
```
```   492     using univ_second_countable by blast
```
```   493   define \<D> where "\<D> \<equiv> {S. S \<in> \<B> \<and> (\<exists>U. U \<in> \<F> \<and> S \<subseteq> U)}"
```
```   494   have "countable \<D>"
```
```   495     apply (rule countable_subset [OF _ \<open>countable \<B>\<close>])
```
```   496     apply (force simp: \<D>_def)
```
```   497     done
```
```   498   have "\<And>S. \<exists>U. S \<in> \<D> \<longrightarrow> U \<in> \<F> \<and> S \<subseteq> U"
```
```   499     by (simp add: \<D>_def)
```
```   500   then obtain G where G: "\<And>S. S \<in> \<D> \<longrightarrow> G S \<in> \<F> \<and> S \<subseteq> G S"
```
```   501     by metis
```
```   502   have "\<Union>\<F> \<subseteq> \<Union>\<D>"
```
```   503     unfolding \<D>_def by (blast dest: \<F> \<B>)
```
```   504   moreover have "\<Union>\<D> \<subseteq> \<Union>\<F>"
```
```   505     using \<D>_def by blast
```
```   506   ultimately have eq1: "\<Union>\<F> = \<Union>\<D>" ..
```
```   507   have eq2: "\<Union>\<D> = \<Union> (G ` \<D>)"
```
```   508     using G eq1 by auto
```
```   509   show ?thesis
```
```   510     apply (rule_tac \<F>' = "G ` \<D>" in that)
```
```   511     using G \<open>countable \<D>\<close>
```
```   512     by (auto simp: eq1 eq2)
```
```   513 qed
```
```   514
```
```   515 lemma countable_disjoint_open_subsets:
```
```   516   fixes \<F> :: "'a::second_countable_topology set set"
```
```   517   assumes "\<And>S. S \<in> \<F> \<Longrightarrow> open S" and pw: "pairwise disjnt \<F>"
```
```   518     shows "countable \<F>"
```
```   519 proof -
```
```   520   obtain \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
```
```   521     by (meson assms Lindelof)
```
```   522   with pw have "\<F> \<subseteq> insert {} \<F>'"
```
```   523     by (fastforce simp add: pairwise_def disjnt_iff)
```
```   524   then show ?thesis
```
```   525     by (simp add: \<open>countable \<F>'\<close> countable_subset)
```
```   526 qed
```
```   527
```
```   528 sublocale second_countable_topology <
```
```   529   countable_basis "open" "SOME B. countable B \<and> topological_basis B"
```
```   530   using someI_ex[OF ex_countable_basis]
```
```   531   by unfold_locales safe
```
```   532
```
```   533
```
```   534 instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
```
```   535 proof
```
```   536   obtain A :: "'a set set" where "countable A" "topological_basis A"
```
```   537     using ex_countable_basis by auto
```
```   538   moreover
```
```   539   obtain B :: "'b set set" where "countable B" "topological_basis B"
```
```   540     using ex_countable_basis by auto
```
```   541   ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> open = generate_topology B"
```
```   542     by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod
```
```   543       topological_basis_imp_subbasis)
```
```   544 qed
```
```   545
```
```   546 instance second_countable_topology \<subseteq> first_countable_topology
```
```   547 proof
```
```   548   fix x :: 'a
```
```   549   define B :: "'a set set" where "B = (SOME B. countable B \<and> topological_basis B)"
```
```   550   then have B: "countable B" "topological_basis B"
```
```   551     using countable_basis is_basis
```
```   552     by (auto simp: countable_basis is_basis)
```
```   553   then show "\<exists>A::nat \<Rightarrow> 'a set.
```
```   554     (\<forall>i. x \<in> A i \<and> open (A i)) \<and> (\<forall>S. open S \<and> x \<in> S \<longrightarrow> (\<exists>i. A i \<subseteq> S))"
```
```   555     by (intro first_countableI[of "{b\<in>B. x \<in> b}"])
```
```   556        (fastforce simp: topological_space_class.topological_basis_def)+
```
```   557 qed
```
```   558
```
```   559 instance nat :: second_countable_topology
```
```   560 proof
```
```   561   show "\<exists>B::nat set set. countable B \<and> open = generate_topology B"
```
```   562     by (intro exI[of _ "range lessThan \<union> range greaterThan"]) (auto simp: open_nat_def)
```
```   563 qed
```
```   564
```
```   565 lemma countable_separating_set_linorder1:
```
```   566   shows "\<exists>B::('a::{linorder_topology, second_countable_topology} set). countable B \<and> (\<forall>x y. x < y \<longrightarrow> (\<exists>b \<in> B. x < b \<and> b \<le> y))"
```
```   567 proof -
```
```   568   obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
```
```   569   define B1 where "B1 = {(LEAST x. x \<in> U)| U. U \<in> A}"
```
```   570   then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
```
```   571   define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}"
```
```   572   then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
```
```   573   have "\<exists>b \<in> B1 \<union> B2. x < b \<and> b \<le> y" if "x < y" for x y
```
```   574   proof (cases)
```
```   575     assume "\<exists>z. x < z \<and> z < y"
```
```   576     then obtain z where z: "x < z \<and> z < y" by auto
```
```   577     define U where "U = {x<..<y}"
```
```   578     then have "open U" by simp
```
```   579     moreover have "z \<in> U" using z U_def by simp
```
```   580     ultimately obtain V where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
```
```   581     define w where "w = (SOME x. x \<in> V)"
```
```   582     then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
```
```   583     then have "x < w \<and> w \<le> y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
```
```   584     moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto
```
```   585     ultimately show ?thesis by auto
```
```   586   next
```
```   587     assume "\<not>(\<exists>z. x < z \<and> z < y)"
```
```   588     then have *: "\<And>z. z > x \<Longrightarrow> z \<ge> y" by auto
```
```   589     define U where "U = {x<..}"
```
```   590     then have "open U" by simp
```
```   591     moreover have "y \<in> U" using \<open>x < y\<close> U_def by simp
```
```   592     ultimately obtain "V" where "V \<in> A" "y \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
```
```   593     have "U = {y..}" unfolding U_def using * \<open>x < y\<close> by auto
```
```   594     then have "V \<subseteq> {y..}" using \<open>V \<subseteq> U\<close> by simp
```
```   595     then have "(LEAST w. w \<in> V) = y" using \<open>y \<in> V\<close> by (meson Least_equality atLeast_iff subsetCE)
```
```   596     then have "y \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto
```
```   597     moreover have "x < y \<and> y \<le> y" using \<open>x < y\<close> by simp
```
```   598     ultimately show ?thesis by auto
```
```   599   qed
```
```   600   moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp
```
```   601   ultimately show ?thesis by auto
```
```   602 qed
```
```   603
```
```   604 lemma countable_separating_set_linorder2:
```
```   605   shows "\<exists>B::('a::{linorder_topology, second_countable_topology} set). countable B \<and> (\<forall>x y. x < y \<longrightarrow> (\<exists>b \<in> B. x \<le> b \<and> b < y))"
```
```   606 proof -
```
```   607   obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
```
```   608   define B1 where "B1 = {(GREATEST x. x \<in> U) | U. U \<in> A}"
```
```   609   then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
```
```   610   define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}"
```
```   611   then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
```
```   612   have "\<exists>b \<in> B1 \<union> B2. x \<le> b \<and> b < y" if "x < y" for x y
```
```   613   proof (cases)
```
```   614     assume "\<exists>z. x < z \<and> z < y"
```
```   615     then obtain z where z: "x < z \<and> z < y" by auto
```
```   616     define U where "U = {x<..<y}"
```
```   617     then have "open U" by simp
```
```   618     moreover have "z \<in> U" using z U_def by simp
```
```   619     ultimately obtain "V" where "V \<in> A" "z \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
```
```   620     define w where "w = (SOME x. x \<in> V)"
```
```   621     then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
```
```   622     then have "x \<le> w \<and> w < y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
```
```   623     moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto
```
```   624     ultimately show ?thesis by auto
```
```   625   next
```
```   626     assume "\<not>(\<exists>z. x < z \<and> z < y)"
```
```   627     then have *: "\<And>z. z < y \<Longrightarrow> z \<le> x" using leI by blast
```
```   628     define U where "U = {..<y}"
```
```   629     then have "open U" by simp
```
```   630     moreover have "x \<in> U" using \<open>x < y\<close> U_def by simp
```
```   631     ultimately obtain "V" where "V \<in> A" "x \<in> V" "V \<subseteq> U" using topological_basisE[OF \<open>topological_basis A\<close>] by auto
```
```   632     have "U = {..x}" unfolding U_def using * \<open>x < y\<close> by auto
```
```   633     then have "V \<subseteq> {..x}" using \<open>V \<subseteq> U\<close> by simp
```
```   634     then have "(GREATEST x. x \<in> V) = x" using \<open>x \<in> V\<close> by (meson Greatest_equality atMost_iff subsetCE)
```
```   635     then have "x \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto
```
```   636     moreover have "x \<le> x \<and> x < y" using \<open>x < y\<close> by simp
```
```   637     ultimately show ?thesis by auto
```
```   638   qed
```
```   639   moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp
```
```   640   ultimately show ?thesis by auto
```
```   641 qed
```
```   642
```
```   643 lemma countable_separating_set_dense_linorder:
```
```   644   shows "\<exists>B::('a::{linorder_topology, dense_linorder, second_countable_topology} set). countable B \<and> (\<forall>x y. x < y \<longrightarrow> (\<exists>b \<in> B. x < b \<and> b < y))"
```
```   645 proof -
```
```   646   obtain B::"'a set" where B: "countable B" "\<And>x y. x < y \<Longrightarrow> (\<exists>b \<in> B. x < b \<and> b \<le> y)"
```
```   647     using countable_separating_set_linorder1 by auto
```
```   648   have "\<exists>b \<in> B. x < b \<and> b < y" if "x < y" for x y
```
```   649   proof -
```
```   650     obtain z where "x < z" "z < y" using \<open>x < y\<close> dense by blast
```
```   651     then obtain b where "b \<in> B" "x < b \<and> b \<le> z" using B(2) by auto
```
```   652     then have "x < b \<and> b < y" using \<open>z < y\<close> by auto
```
```   653     then show ?thesis using \<open>b \<in> B\<close> by auto
```
```   654   qed
```
```   655   then show ?thesis using B(1) by auto
```
```   656 qed
```
```   657
```
```   658
```
```   659 subsection \<open>Polish spaces\<close>
```
```   660
```
```   661 text \<open>Textbooks define Polish spaces as completely metrizable.
```
```   662   We assume the topology to be complete for a given metric.\<close>
```
```   663
```
```   664 class polish_space = complete_space + second_countable_topology
```
```   665
```
```   666
```
```   667 subsection \<open>Limit Points\<close>
```
```   668
```
```   669 definition%important (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infixr "islimpt" 60)
```
```   670   where "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
```
```   671
```
```   672 lemma islimptI:
```
```   673   assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
```
```   674   shows "x islimpt S"
```
```   675   using assms unfolding islimpt_def by auto
```
```   676
```
```   677 lemma islimptE:
```
```   678   assumes "x islimpt S" and "x \<in> T" and "open T"
```
```   679   obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x"
```
```   680   using assms unfolding islimpt_def by auto
```
```   681
```
```   682 lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
```
```   683   unfolding islimpt_def eventually_at_topological by auto
```
```   684
```
```   685 lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> x islimpt T"
```
```   686   unfolding islimpt_def by fast
```
```   687
```
```   688 lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
```
```   689   unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
```
```   690
```
```   691 lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
```
```   692   unfolding islimpt_def by blast
```
```   693
```
```   694 text \<open>A perfect space has no isolated points.\<close>
```
```   695
```
```   696 lemma islimpt_UNIV [simp, intro]: "x islimpt UNIV"
```
```   697   for x :: "'a::perfect_space"
```
```   698   unfolding islimpt_UNIV_iff by (rule not_open_singleton)
```
```   699
```
```   700 lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
```
```   701   unfolding closed_def
```
```   702   apply (subst open_subopen)
```
```   703   apply (simp add: islimpt_def subset_eq)
```
```   704   apply (metis ComplE ComplI)
```
```   705   done
```
```   706
```
```   707 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
```
```   708   by (auto simp: islimpt_def)
```
```   709
```
```   710 lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
```
```   711   by (simp add: islimpt_iff_eventually eventually_conj_iff)
```
```   712
```
```   713
```
```   714 lemma islimpt_insert:
```
```   715   fixes x :: "'a::t1_space"
```
```   716   shows "x islimpt (insert a s) \<longleftrightarrow> x islimpt s"
```
```   717 proof
```
```   718   assume *: "x islimpt (insert a s)"
```
```   719   show "x islimpt s"
```
```   720   proof (rule islimptI)
```
```   721     fix t
```
```   722     assume t: "x \<in> t" "open t"
```
```   723     show "\<exists>y\<in>s. y \<in> t \<and> y \<noteq> x"
```
```   724     proof (cases "x = a")
```
```   725       case True
```
```   726       obtain y where "y \<in> insert a s" "y \<in> t" "y \<noteq> x"
```
```   727         using * t by (rule islimptE)
```
```   728       with \<open>x = a\<close> show ?thesis by auto
```
```   729     next
```
```   730       case False
```
```   731       with t have t': "x \<in> t - {a}" "open (t - {a})"
```
```   732         by (simp_all add: open_Diff)
```
```   733       obtain y where "y \<in> insert a s" "y \<in> t - {a}" "y \<noteq> x"
```
```   734         using * t' by (rule islimptE)
```
```   735       then show ?thesis by auto
```
```   736     qed
```
```   737   qed
```
```   738 next
```
```   739   assume "x islimpt s"
```
```   740   then show "x islimpt (insert a s)"
```
```   741     by (rule islimpt_subset) auto
```
```   742 qed
```
```   743
```
```   744 lemma islimpt_finite:
```
```   745   fixes x :: "'a::t1_space"
```
```   746   shows "finite s \<Longrightarrow> \<not> x islimpt s"
```
```   747   by (induct set: finite) (simp_all add: islimpt_insert)
```
```   748
```
```   749 lemma islimpt_Un_finite:
```
```   750   fixes x :: "'a::t1_space"
```
```   751   shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
```
```   752   by (simp add: islimpt_Un islimpt_finite)
```
```   753
```
```   754 lemma islimpt_eq_acc_point:
```
```   755   fixes l :: "'a :: t1_space"
```
```   756   shows "l islimpt S \<longleftrightarrow> (\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> S))"
```
```   757 proof (safe intro!: islimptI)
```
```   758   fix U
```
```   759   assume "l islimpt S" "l \<in> U" "open U" "finite (U \<inter> S)"
```
```   760   then have "l islimpt S" "l \<in> (U - (U \<inter> S - {l}))" "open (U - (U \<inter> S - {l}))"
```
```   761     by (auto intro: finite_imp_closed)
```
```   762   then show False
```
```   763     by (rule islimptE) auto
```
```   764 next
```
```   765   fix T
```
```   766   assume *: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> S)" "l \<in> T" "open T"
```
```   767   then have "infinite (T \<inter> S - {l})"
```
```   768     by auto
```
```   769   then have "\<exists>x. x \<in> (T \<inter> S - {l})"
```
```   770     unfolding ex_in_conv by (intro notI) simp
```
```   771   then show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> l"
```
```   772     by auto
```
```   773 qed
```
```   774
```
```   775 lemma acc_point_range_imp_convergent_subsequence:
```
```   776   fixes l :: "'a :: first_countable_topology"
```
```   777   assumes l: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> range f)"
```
```   778   shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
```
```   779 proof -
```
```   780   from countable_basis_at_decseq[of l]
```
```   781   obtain A where A:
```
```   782       "\<And>i. open (A i)"
```
```   783       "\<And>i. l \<in> A i"
```
```   784       "\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
```
```   785     by blast
```
```   786   define s where "s n i = (SOME j. i < j \<and> f j \<in> A (Suc n))" for n i
```
```   787   {
```
```   788     fix n i
```
```   789     have "infinite (A (Suc n) \<inter> range f - f`{.. i})"
```
```   790       using l A by auto
```
```   791     then have "\<exists>x. x \<in> A (Suc n) \<inter> range f - f`{.. i}"
```
```   792       unfolding ex_in_conv by (intro notI) simp
```
```   793     then have "\<exists>j. f j \<in> A (Suc n) \<and> j \<notin> {.. i}"
```
```   794       by auto
```
```   795     then have "\<exists>a. i < a \<and> f a \<in> A (Suc n)"
```
```   796       by (auto simp: not_le)
```
```   797     then have "i < s n i" "f (s n i) \<in> A (Suc n)"
```
```   798       unfolding s_def by (auto intro: someI2_ex)
```
```   799   }
```
```   800   note s = this
```
```   801   define r where "r = rec_nat (s 0 0) s"
```
```   802   have "strict_mono r"
```
```   803     by (auto simp: r_def s strict_mono_Suc_iff)
```
```   804   moreover
```
```   805   have "(\<lambda>n. f (r n)) \<longlonglongrightarrow> l"
```
```   806   proof (rule topological_tendstoI)
```
```   807     fix S
```
```   808     assume "open S" "l \<in> S"
```
```   809     with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially"
```
```   810       by auto
```
```   811     moreover
```
```   812     {
```
```   813       fix i
```
```   814       assume "Suc 0 \<le> i"
```
```   815       then have "f (r i) \<in> A i"
```
```   816         by (cases i) (simp_all add: r_def s)
```
```   817     }
```
```   818     then have "eventually (\<lambda>i. f (r i) \<in> A i) sequentially"
```
```   819       by (auto simp: eventually_sequentially)
```
```   820     ultimately show "eventually (\<lambda>i. f (r i) \<in> S) sequentially"
```
```   821       by eventually_elim auto
```
```   822   qed
```
```   823   ultimately show "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
```
```   824     by (auto simp: convergent_def comp_def)
```
```   825 qed
```
```   826
```
```   827 lemma islimpt_range_imp_convergent_subsequence:
```
```   828   fixes l :: "'a :: {t1_space, first_countable_topology}"
```
```   829   assumes l: "l islimpt (range f)"
```
```   830   shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
```
```   831   using l unfolding islimpt_eq_acc_point
```
```   832   by (rule acc_point_range_imp_convergent_subsequence)
```
```   833
```
```   834 lemma sequence_unique_limpt:
```
```   835   fixes f :: "nat \<Rightarrow> 'a::t2_space"
```
```   836   assumes "(f \<longlongrightarrow> l) sequentially"
```
```   837     and "l' islimpt (range f)"
```
```   838   shows "l' = l"
```
```   839 proof (rule ccontr)
```
```   840   assume "l' \<noteq> l"
```
```   841   obtain s t where "open s" "open t" "l' \<in> s" "l \<in> t" "s \<inter> t = {}"
```
```   842     using hausdorff [OF \<open>l' \<noteq> l\<close>] by auto
```
```   843   have "eventually (\<lambda>n. f n \<in> t) sequentially"
```
```   844     using assms(1) \<open>open t\<close> \<open>l \<in> t\<close> by (rule topological_tendstoD)
```
```   845   then obtain N where "\<forall>n\<ge>N. f n \<in> t"
```
```   846     unfolding eventually_sequentially by auto
```
```   847
```
```   848   have "UNIV = {..<N} \<union> {N..}"
```
```   849     by auto
```
```   850   then have "l' islimpt (f ` ({..<N} \<union> {N..}))"
```
```   851     using assms(2) by simp
```
```   852   then have "l' islimpt (f ` {..<N} \<union> f ` {N..})"
```
```   853     by (simp add: image_Un)
```
```   854   then have "l' islimpt (f ` {N..})"
```
```   855     by (simp add: islimpt_Un_finite)
```
```   856   then obtain y where "y \<in> f ` {N..}" "y \<in> s" "y \<noteq> l'"
```
```   857     using \<open>l' \<in> s\<close> \<open>open s\<close> by (rule islimptE)
```
```   858   then obtain n where "N \<le> n" "f n \<in> s" "f n \<noteq> l'"
```
```   859     by auto
```
```   860   with \<open>\<forall>n\<ge>N. f n \<in> t\<close> have "f n \<in> s \<inter> t"
```
```   861     by simp
```
```   862   with \<open>s \<inter> t = {}\<close> show False
```
```   863     by simp
```
```   864 qed
```
```   865
```
```   866
```
```   867 subsection \<open>Interior of a Set\<close>
```
```   868
```
```   869 definition%important interior :: "('a::topological_space) set \<Rightarrow> 'a set" where
```
```   870 "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
```
```   871
```
```   872 lemma interiorI [intro?]:
```
```   873   assumes "open T" and "x \<in> T" and "T \<subseteq> S"
```
```   874   shows "x \<in> interior S"
```
```   875   using assms unfolding interior_def by fast
```
```   876
```
```   877 lemma interiorE [elim?]:
```
```   878   assumes "x \<in> interior S"
```
```   879   obtains T where "open T" and "x \<in> T" and "T \<subseteq> S"
```
```   880   using assms unfolding interior_def by fast
```
```   881
```
```   882 lemma open_interior [simp, intro]: "open (interior S)"
```
```   883   by (simp add: interior_def open_Union)
```
```   884
```
```   885 lemma interior_subset: "interior S \<subseteq> S"
```
```   886   by (auto simp: interior_def)
```
```   887
```
```   888 lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
```
```   889   by (auto simp: interior_def)
```
```   890
```
```   891 lemma interior_open: "open S \<Longrightarrow> interior S = S"
```
```   892   by (intro equalityI interior_subset interior_maximal subset_refl)
```
```   893
```
```   894 lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
```
```   895   by (metis open_interior interior_open)
```
```   896
```
```   897 lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
```
```   898   by (metis interior_maximal interior_subset subset_trans)
```
```   899
```
```   900 lemma interior_empty [simp]: "interior {} = {}"
```
```   901   using open_empty by (rule interior_open)
```
```   902
```
```   903 lemma interior_UNIV [simp]: "interior UNIV = UNIV"
```
```   904   using open_UNIV by (rule interior_open)
```
```   905
```
```   906 lemma interior_interior [simp]: "interior (interior S) = interior S"
```
```   907   using open_interior by (rule interior_open)
```
```   908
```
```   909 lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
```
```   910   by (auto simp: interior_def)
```
```   911
```
```   912 lemma interior_unique:
```
```   913   assumes "T \<subseteq> S" and "open T"
```
```   914   assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T"
```
```   915   shows "interior S = T"
```
```   916   by (intro equalityI assms interior_subset open_interior interior_maximal)
```
```   917
```
```   918 lemma interior_singleton [simp]: "interior {a} = {}"
```
```   919   for a :: "'a::perfect_space"
```
```   920   apply (rule interior_unique, simp_all)
```
```   921   using not_open_singleton subset_singletonD
```
```   922   apply fastforce
```
```   923   done
```
```   924
```
```   925 lemma interior_Int [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
```
```   926   by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
```
```   927     Int_lower2 interior_maximal interior_subset open_Int open_interior)
```
```   928
```
```   929 lemma eventually_nhds_in_nhd: "x \<in> interior s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
```
```   930   using interior_subset[of s] by (subst eventually_nhds) blast
```
```   931
```
```   932 lemma interior_limit_point [intro]:
```
```   933   fixes x :: "'a::perfect_space"
```
```   934   assumes x: "x \<in> interior S"
```
```   935   shows "x islimpt S"
```
```   936   using x islimpt_UNIV [of x]
```
```   937   unfolding interior_def islimpt_def
```
```   938   apply (clarsimp, rename_tac T T')
```
```   939   apply (drule_tac x="T \<inter> T'" in spec)
```
```   940   apply (auto simp: open_Int)
```
```   941   done
```
```   942
```
```   943 lemma interior_closed_Un_empty_interior:
```
```   944   assumes cS: "closed S"
```
```   945     and iT: "interior T = {}"
```
```   946   shows "interior (S \<union> T) = interior S"
```
```   947 proof
```
```   948   show "interior S \<subseteq> interior (S \<union> T)"
```
```   949     by (rule interior_mono) (rule Un_upper1)
```
```   950   show "interior (S \<union> T) \<subseteq> interior S"
```
```   951   proof
```
```   952     fix x
```
```   953     assume "x \<in> interior (S \<union> T)"
```
```   954     then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
```
```   955     show "x \<in> interior S"
```
```   956     proof (rule ccontr)
```
```   957       assume "x \<notin> interior S"
```
```   958       with \<open>x \<in> R\<close> \<open>open R\<close> obtain y where "y \<in> R - S"
```
```   959         unfolding interior_def by fast
```
```   960       from \<open>open R\<close> \<open>closed S\<close> have "open (R - S)"
```
```   961         by (rule open_Diff)
```
```   962       from \<open>R \<subseteq> S \<union> T\<close> have "R - S \<subseteq> T"
```
```   963         by fast
```
```   964       from \<open>y \<in> R - S\<close> \<open>open (R - S)\<close> \<open>R - S \<subseteq> T\<close> \<open>interior T = {}\<close> show False
```
```   965         unfolding interior_def by fast
```
```   966     qed
```
```   967   qed
```
```   968 qed
```
```   969
```
```   970 lemma interior_Times: "interior (A \<times> B) = interior A \<times> interior B"
```
```   971 proof (rule interior_unique)
```
```   972   show "interior A \<times> interior B \<subseteq> A \<times> B"
```
```   973     by (intro Sigma_mono interior_subset)
```
```   974   show "open (interior A \<times> interior B)"
```
```   975     by (intro open_Times open_interior)
```
```   976   fix T
```
```   977   assume "T \<subseteq> A \<times> B" and "open T"
```
```   978   then show "T \<subseteq> interior A \<times> interior B"
```
```   979   proof safe
```
```   980     fix x y
```
```   981     assume "(x, y) \<in> T"
```
```   982     then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
```
```   983       using \<open>open T\<close> unfolding open_prod_def by fast
```
```   984     then have "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
```
```   985       using \<open>T \<subseteq> A \<times> B\<close> by auto
```
```   986     then show "x \<in> interior A" and "y \<in> interior B"
```
```   987       by (auto intro: interiorI)
```
```   988   qed
```
```   989 qed
```
```   990
```
```   991 lemma interior_Ici:
```
```   992   fixes x :: "'a :: {dense_linorder,linorder_topology}"
```
```   993   assumes "b < x"
```
```   994   shows "interior {x ..} = {x <..}"
```
```   995 proof (rule interior_unique)
```
```   996   fix T
```
```   997   assume "T \<subseteq> {x ..}" "open T"
```
```   998   moreover have "x \<notin> T"
```
```   999   proof
```
```  1000     assume "x \<in> T"
```
```  1001     obtain y where "y < x" "{y <.. x} \<subseteq> T"
```
```  1002       using open_left[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>b < x\<close>] by auto
```
```  1003     with dense[OF \<open>y < x\<close>] obtain z where "z \<in> T" "z < x"
```
```  1004       by (auto simp: subset_eq Ball_def)
```
```  1005     with \<open>T \<subseteq> {x ..}\<close> show False by auto
```
```  1006   qed
```
```  1007   ultimately show "T \<subseteq> {x <..}"
```
```  1008     by (auto simp: subset_eq less_le)
```
```  1009 qed auto
```
```  1010
```
```  1011 lemma interior_Iic:
```
```  1012   fixes x :: "'a ::{dense_linorder,linorder_topology}"
```
```  1013   assumes "x < b"
```
```  1014   shows "interior {.. x} = {..< x}"
```
```  1015 proof (rule interior_unique)
```
```  1016   fix T
```
```  1017   assume "T \<subseteq> {.. x}" "open T"
```
```  1018   moreover have "x \<notin> T"
```
```  1019   proof
```
```  1020     assume "x \<in> T"
```
```  1021     obtain y where "x < y" "{x ..< y} \<subseteq> T"
```
```  1022       using open_right[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>x < b\<close>] by auto
```
```  1023     with dense[OF \<open>x < y\<close>] obtain z where "z \<in> T" "x < z"
```
```  1024       by (auto simp: subset_eq Ball_def less_le)
```
```  1025     with \<open>T \<subseteq> {.. x}\<close> show False by auto
```
```  1026   qed
```
```  1027   ultimately show "T \<subseteq> {..< x}"
```
```  1028     by (auto simp: subset_eq less_le)
```
```  1029 qed auto
```
```  1030
```
```  1031 lemma countable_disjoint_nonempty_interior_subsets:
```
```  1032   fixes \<F> :: "'a::second_countable_topology set set"
```
```  1033   assumes pw: "pairwise disjnt \<F>" and int: "\<And>S. \<lbrakk>S \<in> \<F>; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
```
```  1034   shows "countable \<F>"
```
```  1035 proof (rule countable_image_inj_on)
```
```  1036   have "disjoint (interior ` \<F>)"
```
```  1037     using pw by (simp add: disjoint_image_subset interior_subset)
```
```  1038   then show "countable (interior ` \<F>)"
```
```  1039     by (auto intro: countable_disjoint_open_subsets)
```
```  1040   show "inj_on interior \<F>"
```
```  1041     using pw apply (clarsimp simp: inj_on_def pairwise_def)
```
```  1042     apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
```
```  1043     done
```
```  1044 qed
```
```  1045
```
```  1046 subsection \<open>Closure of a Set\<close>
```
```  1047
```
```  1048 definition%important closure :: "('a::topological_space) set \<Rightarrow> 'a set" where
```
```  1049 "closure S = S \<union> {x . x islimpt S}"
```
```  1050
```
```  1051 lemma interior_closure: "interior S = - (closure (- S))"
```
```  1052   by (auto simp: interior_def closure_def islimpt_def)
```
```  1053
```
```  1054 lemma closure_interior: "closure S = - interior (- S)"
```
```  1055   by (simp add: interior_closure)
```
```  1056
```
```  1057 lemma closed_closure[simp, intro]: "closed (closure S)"
```
```  1058   by (simp add: closure_interior closed_Compl)
```
```  1059
```
```  1060 lemma closure_subset: "S \<subseteq> closure S"
```
```  1061   by (simp add: closure_def)
```
```  1062
```
```  1063 lemma closure_hull: "closure S = closed hull S"
```
```  1064   by (auto simp: hull_def closure_interior interior_def)
```
```  1065
```
```  1066 lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
```
```  1067   unfolding closure_hull using closed_Inter by (rule hull_eq)
```
```  1068
```
```  1069 lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
```
```  1070   by (simp only: closure_eq)
```
```  1071
```
```  1072 lemma closure_closure [simp]: "closure (closure S) = closure S"
```
```  1073   unfolding closure_hull by (rule hull_hull)
```
```  1074
```
```  1075 lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
```
```  1076   unfolding closure_hull by (rule hull_mono)
```
```  1077
```
```  1078 lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
```
```  1079   unfolding closure_hull by (rule hull_minimal)
```
```  1080
```
```  1081 lemma closure_unique:
```
```  1082   assumes "S \<subseteq> T"
```
```  1083     and "closed T"
```
```  1084     and "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
```
```  1085   shows "closure S = T"
```
```  1086   using assms unfolding closure_hull by (rule hull_unique)
```
```  1087
```
```  1088 lemma closure_empty [simp]: "closure {} = {}"
```
```  1089   using closed_empty by (rule closure_closed)
```
```  1090
```
```  1091 lemma closure_UNIV [simp]: "closure UNIV = UNIV"
```
```  1092   using closed_UNIV by (rule closure_closed)
```
```  1093
```
```  1094 lemma closure_Un [simp]: "closure (S \<union> T) = closure S \<union> closure T"
```
```  1095   by (simp add: closure_interior)
```
```  1096
```
```  1097 lemma closure_eq_empty [iff]: "closure S = {} \<longleftrightarrow> S = {}"
```
```  1098   using closure_empty closure_subset[of S] by blast
```
```  1099
```
```  1100 lemma closure_subset_eq: "closure S \<subseteq> S \<longleftrightarrow> closed S"
```
```  1101   using closure_eq[of S] closure_subset[of S] by simp
```
```  1102
```
```  1103 lemma open_Int_closure_eq_empty: "open S \<Longrightarrow> (S \<inter> closure T) = {} \<longleftrightarrow> S \<inter> T = {}"
```
```  1104   using open_subset_interior[of S "- T"]
```
```  1105   using interior_subset[of "- T"]
```
```  1106   by (auto simp: closure_interior)
```
```  1107
```
```  1108 lemma open_Int_closure_subset: "open S \<Longrightarrow> S \<inter> closure T \<subseteq> closure (S \<inter> T)"
```
```  1109 proof
```
```  1110   fix x
```
```  1111   assume *: "open S" "x \<in> S \<inter> closure T"
```
```  1112   have "x islimpt (S \<inter> T)" if **: "x islimpt T"
```
```  1113   proof (rule islimptI)
```
```  1114     fix A
```
```  1115     assume "x \<in> A" "open A"
```
```  1116     with * have "x \<in> A \<inter> S" "open (A \<inter> S)"
```
```  1117       by (simp_all add: open_Int)
```
```  1118     with ** obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x"
```
```  1119       by (rule islimptE)
```
```  1120     then have "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
```
```  1121       by simp_all
```
```  1122     then show "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" ..
```
```  1123   qed
```
```  1124   with * show "x \<in> closure (S \<inter> T)"
```
```  1125     unfolding closure_def by blast
```
```  1126 qed
```
```  1127
```
```  1128 lemma closure_complement: "closure (- S) = - interior S"
```
```  1129   by (simp add: closure_interior)
```
```  1130
```
```  1131 lemma interior_complement: "interior (- S) = - closure S"
```
```  1132   by (simp add: closure_interior)
```
```  1133
```
```  1134 lemma interior_diff: "interior(S - T) = interior S - closure T"
```
```  1135   by (simp add: Diff_eq interior_complement)
```
```  1136
```
```  1137 lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
```
```  1138 proof (rule closure_unique)
```
```  1139   show "A \<times> B \<subseteq> closure A \<times> closure B"
```
```  1140     by (intro Sigma_mono closure_subset)
```
```  1141   show "closed (closure A \<times> closure B)"
```
```  1142     by (intro closed_Times closed_closure)
```
```  1143   fix T
```
```  1144   assume "A \<times> B \<subseteq> T" and "closed T"
```
```  1145   then show "closure A \<times> closure B \<subseteq> T"
```
```  1146     apply (simp add: closed_def open_prod_def, clarify)
```
```  1147     apply (rule ccontr)
```
```  1148     apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
```
```  1149     apply (simp add: closure_interior interior_def)
```
```  1150     apply (drule_tac x=C in spec)
```
```  1151     apply (drule_tac x=D in spec, auto)
```
```  1152     done
```
```  1153 qed
```
```  1154
```
```  1155 lemma islimpt_in_closure: "(x islimpt S) = (x\<in>closure(S-{x}))"
```
```  1156   unfolding closure_def using islimpt_punctured by blast
```
```  1157
```
```  1158 lemma connected_imp_connected_closure: "connected S \<Longrightarrow> connected (closure S)"
```
```  1159   by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD)
```
```  1160
```
```  1161 lemma bdd_below_closure:
```
```  1162   fixes A :: "real set"
```
```  1163   assumes "bdd_below A"
```
```  1164   shows "bdd_below (closure A)"
```
```  1165 proof -
```
```  1166   from assms obtain m where "\<And>x. x \<in> A \<Longrightarrow> m \<le> x"
```
```  1167     by (auto simp: bdd_below_def)
```
```  1168   then have "A \<subseteq> {m..}" by auto
```
```  1169   then have "closure A \<subseteq> {m..}"
```
```  1170     using closed_real_atLeast by (rule closure_minimal)
```
```  1171   then show ?thesis
```
```  1172     by (auto simp: bdd_below_def)
```
```  1173 qed
```
```  1174
```
```  1175
```
```  1176 subsection \<open>Frontier (also known as boundary)\<close>
```
```  1177
```
```  1178 definition%important frontier :: "('a::topological_space) set \<Rightarrow> 'a set" where
```
```  1179 "frontier S = closure S - interior S"
```
```  1180
```
```  1181 lemma frontier_closed [iff]: "closed (frontier S)"
```
```  1182   by (simp add: frontier_def closed_Diff)
```
```  1183
```
```  1184 lemma frontier_closures: "frontier S = closure S \<inter> closure (- S)"
```
```  1185   by (auto simp: frontier_def interior_closure)
```
```  1186
```
```  1187 lemma frontier_Int: "frontier(S \<inter> T) = closure(S \<inter> T) \<inter> (frontier S \<union> frontier T)"
```
```  1188 proof -
```
```  1189   have "closure (S \<inter> T) \<subseteq> closure S" "closure (S \<inter> T) \<subseteq> closure T"
```
```  1190     by (simp_all add: closure_mono)
```
```  1191   then show ?thesis
```
```  1192     by (auto simp: frontier_closures)
```
```  1193 qed
```
```  1194
```
```  1195 lemma frontier_Int_subset: "frontier(S \<inter> T) \<subseteq> frontier S \<union> frontier T"
```
```  1196   by (auto simp: frontier_Int)
```
```  1197
```
```  1198 lemma frontier_Int_closed:
```
```  1199   assumes "closed S" "closed T"
```
```  1200   shows "frontier(S \<inter> T) = (frontier S \<inter> T) \<union> (S \<inter> frontier T)"
```
```  1201 proof -
```
```  1202   have "closure (S \<inter> T) = T \<inter> S"
```
```  1203     using assms by (simp add: Int_commute closed_Int)
```
```  1204   moreover have "T \<inter> (closure S \<inter> closure (- S)) = frontier S \<inter> T"
```
```  1205     by (simp add: Int_commute frontier_closures)
```
```  1206   ultimately show ?thesis
```
```  1207     by (simp add: Int_Un_distrib Int_assoc Int_left_commute assms frontier_closures)
```
```  1208 qed
```
```  1209
```
```  1210 lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
```
```  1211   by (metis frontier_def closure_closed Diff_subset)
```
```  1212
```
```  1213 lemma frontier_empty [simp]: "frontier {} = {}"
```
```  1214   by (simp add: frontier_def)
```
```  1215
```
```  1216 lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
```
```  1217 proof -
```
```  1218   {
```
```  1219     assume "frontier S \<subseteq> S"
```
```  1220     then have "closure S \<subseteq> S"
```
```  1221       using interior_subset unfolding frontier_def by auto
```
```  1222     then have "closed S"
```
```  1223       using closure_subset_eq by auto
```
```  1224   }
```
```  1225   then show ?thesis using frontier_subset_closed[of S] ..
```
```  1226 qed
```
```  1227
```
```  1228 lemma frontier_complement [simp]: "frontier (- S) = frontier S"
```
```  1229   by (auto simp: frontier_def closure_complement interior_complement)
```
```  1230
```
```  1231 lemma frontier_Un_subset: "frontier(S \<union> T) \<subseteq> frontier S \<union> frontier T"
```
```  1232   by (metis compl_sup frontier_Int_subset frontier_complement)
```
```  1233
```
```  1234 lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
```
```  1235   using frontier_complement frontier_subset_eq[of "- S"]
```
```  1236   unfolding open_closed by auto
```
```  1237
```
```  1238 lemma frontier_UNIV [simp]: "frontier UNIV = {}"
```
```  1239   using frontier_complement frontier_empty by fastforce
```
```  1240
```
```  1241 lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)"
```
```  1242   by (simp add: Int_commute frontier_def interior_closure)
```
```  1243
```
```  1244 lemma frontier_interior_subset: "frontier(interior S) \<subseteq> frontier S"
```
```  1245   by (simp add: Diff_mono frontier_interiors interior_mono interior_subset)
```
```  1246
```
```  1247 lemma closure_Un_frontier: "closure S = S \<union> frontier S"
```
```  1248 proof -
```
```  1249   have "S \<union> interior S = S"
```
```  1250     using interior_subset by auto
```
```  1251   then show ?thesis
```
```  1252     using closure_subset by (auto simp: frontier_def)
```
```  1253 qed
```
```  1254
```
```  1255
```
```  1256 subsection%unimportant \<open>Filters and the ``eventually true'' quantifier\<close>
```
```  1257
```
```  1258 text \<open>Identify Trivial limits, where we can't approach arbitrarily closely.\<close>
```
```  1259
```
```  1260 lemma trivial_limit_within: "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
```
```  1261 proof
```
```  1262   assume "trivial_limit (at a within S)"
```
```  1263   then show "\<not> a islimpt S"
```
```  1264     unfolding trivial_limit_def
```
```  1265     unfolding eventually_at_topological
```
```  1266     unfolding islimpt_def
```
```  1267     apply (clarsimp simp add: set_eq_iff)
```
```  1268     apply (rename_tac T, rule_tac x=T in exI)
```
```  1269     apply (clarsimp, drule_tac x=y in bspec, simp_all)
```
```  1270     done
```
```  1271 next
```
```  1272   assume "\<not> a islimpt S"
```
```  1273   then show "trivial_limit (at a within S)"
```
```  1274     unfolding trivial_limit_def eventually_at_topological islimpt_def
```
```  1275     by metis
```
```  1276 qed
```
```  1277
```
```  1278 lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV"
```
```  1279   using trivial_limit_within [of a UNIV] by simp
```
```  1280
```
```  1281 lemma trivial_limit_at: "\<not> trivial_limit (at a)"
```
```  1282   for a :: "'a::perfect_space"
```
```  1283   by (rule at_neq_bot)
```
```  1284
```
```  1285 lemma not_trivial_limit_within: "\<not> trivial_limit (at x within S) = (x \<in> closure (S - {x}))"
```
```  1286   using islimpt_in_closure by (metis trivial_limit_within)
```
```  1287
```
```  1288 lemma not_in_closure_trivial_limitI:
```
```  1289   "x \<notin> closure s \<Longrightarrow> trivial_limit (at x within s)"
```
```  1290   using not_trivial_limit_within[of x s]
```
```  1291   by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD)
```
```  1292
```
```  1293 lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)"
```
```  1294   if "x \<in> closure s \<Longrightarrow> filterlim f l (at x within s)"
```
```  1295   by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that)
```
```  1296
```
```  1297 lemma at_within_eq_bot_iff: "at c within A = bot \<longleftrightarrow> c \<notin> closure (A - {c})"
```
```  1298   using not_trivial_limit_within[of c A] by blast
```
```  1299
```
```  1300 text \<open>Some property holds "sufficiently close" to the limit point.\<close>
```
```  1301
```
```  1302 lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
```
```  1303   by simp
```
```  1304
```
```  1305 lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
```
```  1306   by (simp add: filter_eq_iff)
```
```  1307
```
```  1308 lemma Lim_topological:
```
```  1309   "(f \<longlongrightarrow> l) net \<longleftrightarrow>
```
```  1310     trivial_limit net \<or> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
```
```  1311   unfolding tendsto_def trivial_limit_eq by auto
```
```  1312
```
```  1313 lemma eventually_within_Un:
```
```  1314   "eventually P (at x within (s \<union> t)) \<longleftrightarrow>
```
```  1315     eventually P (at x within s) \<and> eventually P (at x within t)"
```
```  1316   unfolding eventually_at_filter
```
```  1317   by (auto elim!: eventually_rev_mp)
```
```  1318
```
```  1319 lemma Lim_within_union:
```
```  1320  "(f \<longlongrightarrow> l) (at x within (s \<union> t)) \<longleftrightarrow>
```
```  1321   (f \<longlongrightarrow> l) (at x within s) \<and> (f \<longlongrightarrow> l) (at x within t)"
```
```  1322   unfolding tendsto_def
```
```  1323   by (auto simp: eventually_within_Un)
```
```  1324
```
```  1325
```
```  1326 subsection \<open>Limits\<close>
```
```  1327
```
```  1328 lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f \<longlongrightarrow> l) net"
```
```  1329   by (rule topological_tendstoI) (auto elim: eventually_mono)
```
```  1330
```
```  1331 text \<open>The expected monotonicity property.\<close>
```
```  1332
```
```  1333 lemma Lim_Un:
```
```  1334   assumes "(f \<longlongrightarrow> l) (at x within S)" "(f \<longlongrightarrow> l) (at x within T)"
```
```  1335   shows "(f \<longlongrightarrow> l) (at x within (S \<union> T))"
```
```  1336   using assms unfolding at_within_union by (rule filterlim_sup)
```
```  1337
```
```  1338 lemma Lim_Un_univ:
```
```  1339   "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T) \<Longrightarrow>
```
```  1340     S \<union> T = UNIV \<Longrightarrow> (f \<longlongrightarrow> l) (at x)"
```
```  1341   by (metis Lim_Un)
```
```  1342
```
```  1343 text \<open>Interrelations between restricted and unrestricted limits.\<close>
```
```  1344
```
```  1345 lemma Lim_at_imp_Lim_at_within: "(f \<longlongrightarrow> l) (at x) \<Longrightarrow> (f \<longlongrightarrow> l) (at x within S)"
```
```  1346   by (metis order_refl filterlim_mono subset_UNIV at_le)
```
```  1347
```
```  1348 lemma eventually_within_interior:
```
```  1349   assumes "x \<in> interior S"
```
```  1350   shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)"
```
```  1351   (is "?lhs = ?rhs")
```
```  1352 proof
```
```  1353   from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
```
```  1354   {
```
```  1355     assume ?lhs
```
```  1356     then obtain A where "open A" and "x \<in> A" and "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
```
```  1357       by (auto simp: eventually_at_topological)
```
```  1358     with T have "open (A \<inter> T)" and "x \<in> A \<inter> T" and "\<forall>y \<in> A \<inter> T. y \<noteq> x \<longrightarrow> P y"
```
```  1359       by auto
```
```  1360     then show ?rhs
```
```  1361       by (auto simp: eventually_at_topological)
```
```  1362   next
```
```  1363     assume ?rhs
```
```  1364     then show ?lhs
```
```  1365       by (auto elim: eventually_mono simp: eventually_at_filter)
```
```  1366   }
```
```  1367 qed
```
```  1368
```
```  1369 lemma at_within_interior: "x \<in> interior S \<Longrightarrow> at x within S = at x"
```
```  1370   unfolding filter_eq_iff by (intro allI eventually_within_interior)
```
```  1371
```
```  1372 lemma Lim_within_LIMSEQ:
```
```  1373   fixes a :: "'a::first_countable_topology"
```
```  1374   assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S \<longlonglongrightarrow> a \<longrightarrow> (\<lambda>n. X (S n)) \<longlonglongrightarrow> L"
```
```  1375   shows "(X \<longlongrightarrow> L) (at a within T)"
```
```  1376   using assms unfolding tendsto_def [where l=L]
```
```  1377   by (simp add: sequentially_imp_eventually_within)
```
```  1378
```
```  1379 lemma Lim_right_bound:
```
```  1380   fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow>
```
```  1381     'b::{linorder_topology, conditionally_complete_linorder}"
```
```  1382   assumes mono: "\<And>a b. a \<in> I \<Longrightarrow> b \<in> I \<Longrightarrow> x < a \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b"
```
```  1383     and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
```
```  1384   shows "(f \<longlongrightarrow> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
```
```  1385 proof (cases "{x<..} \<inter> I = {}")
```
```  1386   case True
```
```  1387   then show ?thesis by simp
```
```  1388 next
```
```  1389   case False
```
```  1390   show ?thesis
```
```  1391   proof (rule order_tendstoI)
```
```  1392     fix a
```
```  1393     assume a: "a < Inf (f ` ({x<..} \<inter> I))"
```
```  1394     {
```
```  1395       fix y
```
```  1396       assume "y \<in> {x<..} \<inter> I"
```
```  1397       with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
```
```  1398         by (auto intro!: cInf_lower bdd_belowI2)
```
```  1399       with a have "a < f y"
```
```  1400         by (blast intro: less_le_trans)
```
```  1401     }
```
```  1402     then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
```
```  1403       by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
```
```  1404   next
```
```  1405     fix a
```
```  1406     assume "Inf (f ` ({x<..} \<inter> I)) < a"
```
```  1407     from cInf_lessD[OF _ this] False obtain y where y: "x < y" "y \<in> I" "f y < a"
```
```  1408       by auto
```
```  1409     then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
```
```  1410       unfolding eventually_at_right[OF \<open>x < y\<close>] by (metis less_imp_le le_less_trans mono)
```
```  1411     then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
```
```  1412       unfolding eventually_at_filter by eventually_elim simp
```
```  1413   qed
```
```  1414 qed
```
```  1415
```
```  1416 (*could prove directly from islimpt_sequential_inj, but only for metric spaces*)
```
```  1417 lemma islimpt_sequential:
```
```  1418   fixes x :: "'a::first_countable_topology"
```
```  1419   shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
```
```  1420     (is "?lhs = ?rhs")
```
```  1421 proof
```
```  1422   assume ?lhs
```
```  1423   from countable_basis_at_decseq[of x] obtain A where A:
```
```  1424       "\<And>i. open (A i)"
```
```  1425       "\<And>i. x \<in> A i"
```
```  1426       "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
```
```  1427     by blast
```
```  1428   define f where "f n = (SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y)" for n
```
```  1429   {
```
```  1430     fix n
```
```  1431     from \<open>?lhs\<close> have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
```
```  1432       unfolding islimpt_def using A(1,2)[of n] by auto
```
```  1433     then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
```
```  1434       unfolding f_def by (rule someI_ex)
```
```  1435     then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
```
```  1436   }
```
```  1437   then have "\<forall>n. f n \<in> S - {x}" by auto
```
```  1438   moreover have "(\<lambda>n. f n) \<longlonglongrightarrow> x"
```
```  1439   proof (rule topological_tendstoI)
```
```  1440     fix S
```
```  1441     assume "open S" "x \<in> S"
```
```  1442     from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
```
```  1443     show "eventually (\<lambda>x. f x \<in> S) sequentially"
```
```  1444       by (auto elim!: eventually_mono)
```
```  1445   qed
```
```  1446   ultimately show ?rhs by fast
```
```  1447 next
```
```  1448   assume ?rhs
```
```  1449   then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f \<longlonglongrightarrow> x"
```
```  1450     by auto
```
```  1451   show ?lhs
```
```  1452     unfolding islimpt_def
```
```  1453   proof safe
```
```  1454     fix T
```
```  1455     assume "open T" "x \<in> T"
```
```  1456     from lim[THEN topological_tendstoD, OF this] f
```
```  1457     show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
```
```  1458       unfolding eventually_sequentially by auto
```
```  1459   qed
```
```  1460 qed
```
```  1461
```
```  1462 text\<open>Deducing things about the limit from the elements.\<close>
```
```  1463
```
```  1464 lemma Lim_in_closed_set:
```
```  1465   assumes "closed S"
```
```  1466     and "eventually (\<lambda>x. f(x) \<in> S) net"
```
```  1467     and "\<not> trivial_limit net" "(f \<longlongrightarrow> l) net"
```
```  1468   shows "l \<in> S"
```
```  1469 proof (rule ccontr)
```
```  1470   assume "l \<notin> S"
```
```  1471   with \<open>closed S\<close> have "open (- S)" "l \<in> - S"
```
```  1472     by (simp_all add: open_Compl)
```
```  1473   with assms(4) have "eventually (\<lambda>x. f x \<in> - S) net"
```
```  1474     by (rule topological_tendstoD)
```
```  1475   with assms(2) have "eventually (\<lambda>x. False) net"
```
```  1476     by (rule eventually_elim2) simp
```
```  1477   with assms(3) show "False"
```
```  1478     by (simp add: eventually_False)
```
```  1479 qed
```
```  1480
```
```  1481 text\<open>These are special for limits out of the same topological space.\<close>
```
```  1482
```
```  1483 lemma Lim_within_id: "(id \<longlongrightarrow> a) (at a within s)"
```
```  1484   unfolding id_def by (rule tendsto_ident_at)
```
```  1485
```
```  1486 lemma Lim_at_id: "(id \<longlongrightarrow> a) (at a)"
```
```  1487   unfolding id_def by (rule tendsto_ident_at)
```
```  1488
```
```  1489 text\<open>It's also sometimes useful to extract the limit point from the filter.\<close>
```
```  1490
```
```  1491 abbreviation netlimit :: "'a::t2_space filter \<Rightarrow> 'a"
```
```  1492   where "netlimit F \<equiv> Lim F (\<lambda>x. x)"
```
```  1493
```
```  1494 lemma netlimit_within: "\<not> trivial_limit (at a within S) \<Longrightarrow> netlimit (at a within S) = a"
```
```  1495   by (rule tendsto_Lim) (auto intro: tendsto_intros)
```
```  1496
```
```  1497 lemma netlimit_at [simp]:
```
```  1498   fixes a :: "'a::{perfect_space,t2_space}"
```
```  1499   shows "netlimit (at a) = a"
```
```  1500   using netlimit_within [of a UNIV] by simp
```
```  1501
```
```  1502 lemma lim_within_interior:
```
```  1503   "x \<in> interior S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within S) \<longleftrightarrow> (f \<longlongrightarrow> l) (at x)"
```
```  1504   by (metis at_within_interior)
```
```  1505
```
```  1506 lemma netlimit_within_interior:
```
```  1507   fixes x :: "'a::{t2_space,perfect_space}"
```
```  1508   assumes "x \<in> interior S"
```
```  1509   shows "netlimit (at x within S) = x"
```
```  1510   using assms by (metis at_within_interior netlimit_at)
```
```  1511
```
```  1512 text\<open>Useful lemmas on closure and set of possible sequential limits.\<close>
```
```  1513
```
```  1514 lemma closure_sequential:
```
```  1515   fixes l :: "'a::first_countable_topology"
```
```  1516   shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x \<longlongrightarrow> l) sequentially)"
```
```  1517   (is "?lhs = ?rhs")
```
```  1518 proof
```
```  1519   assume "?lhs"
```
```  1520   moreover
```
```  1521   {
```
```  1522     assume "l \<in> S"
```
```  1523     then have "?rhs" using tendsto_const[of l sequentially] by auto
```
```  1524   }
```
```  1525   moreover
```
```  1526   {
```
```  1527     assume "l islimpt S"
```
```  1528     then have "?rhs" unfolding islimpt_sequential by auto
```
```  1529   }
```
```  1530   ultimately show "?rhs"
```
```  1531     unfolding closure_def by auto
```
```  1532 next
```
```  1533   assume "?rhs"
```
```  1534   then show "?lhs" unfolding closure_def islimpt_sequential by auto
```
```  1535 qed
```
```  1536
```
```  1537 lemma closed_sequential_limits:
```
```  1538   fixes S :: "'a::first_countable_topology set"
```
```  1539   shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x \<longlongrightarrow> l) sequentially \<longrightarrow> l \<in> S)"
```
```  1540 by (metis closure_sequential closure_subset_eq subset_iff)
```
```  1541
```
```  1542 lemma tendsto_If_within_closures:
```
```  1543   assumes f: "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
```
```  1544       (f \<longlongrightarrow> l x) (at x within s \<union> (closure s \<inter> closure t))"
```
```  1545   assumes g: "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
```
```  1546       (g \<longlongrightarrow> l x) (at x within t \<union> (closure s \<inter> closure t))"
```
```  1547   assumes "x \<in> s \<union> t"
```
```  1548   shows "((\<lambda>x. if x \<in> s then f x else g x) \<longlongrightarrow> l x) (at x within s \<union> t)"
```
```  1549 proof -
```
```  1550   have *: "(s \<union> t) \<inter> {x. x \<in> s} = s" "(s \<union> t) \<inter> {x. x \<notin> s} = t - s"
```
```  1551     by auto
```
```  1552   have "(f \<longlongrightarrow> l x) (at x within s)"
```
```  1553     by (rule filterlim_at_within_closure_implies_filterlim)
```
```  1554        (use \<open>x \<in> _\<close> in \<open>auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f]\<close>)
```
```  1555   moreover
```
```  1556   have "(g \<longlongrightarrow> l x) (at x within t - s)"
```
```  1557     by (rule filterlim_at_within_closure_implies_filterlim)
```
```  1558       (use \<open>x \<in> _\<close> in
```
```  1559         \<open>auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset\<close>)
```
```  1560   ultimately show ?thesis
```
```  1561     by (intro filterlim_at_within_If) (simp_all only: *)
```
```  1562 qed
```
```  1563
```
```  1564
```
```  1565 subsection \<open>Compactness\<close>
```
```  1566
```
```  1567 lemma brouwer_compactness_lemma:
```
```  1568   fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
```
```  1569   assumes "compact s"
```
```  1570     and "continuous_on s f"
```
```  1571     and "\<not> (\<exists>x\<in>s. f x = 0)"
```
```  1572   obtains d where "0 < d" and "\<forall>x\<in>s. d \<le> norm (f x)"
```
```  1573 proof (cases "s = {}")
```
```  1574   case True
```
```  1575   show thesis
```
```  1576     by (rule that [of 1]) (auto simp: True)
```
```  1577 next
```
```  1578   case False
```
```  1579   have "continuous_on s (norm \<circ> f)"
```
```  1580     by (rule continuous_intros continuous_on_norm assms(2))+
```
```  1581   with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
```
```  1582     using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
```
```  1583     unfolding o_def
```
```  1584     by auto
```
```  1585   have "(norm \<circ> f) x > 0"
```
```  1586     using assms(3) and x(1)
```
```  1587     by auto
```
```  1588   then show ?thesis
```
```  1589     by (rule that) (insert x(2), auto simp: o_def)
```
```  1590 qed
```
```  1591
```
```  1592 subsubsection \<open>Bolzano-Weierstrass property\<close>
```
```  1593
```
```  1594 proposition Heine_Borel_imp_Bolzano_Weierstrass:
```
```  1595   assumes "compact s"
```
```  1596     and "infinite t"
```
```  1597     and "t \<subseteq> s"
```
```  1598   shows "\<exists>x \<in> s. x islimpt t"
```
```  1599 proof (rule ccontr)
```
```  1600   assume "\<not> (\<exists>x \<in> s. x islimpt t)"
```
```  1601   then obtain f where f: "\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)"
```
```  1602     unfolding islimpt_def
```
```  1603     using bchoice[of s "\<lambda> x T. x \<in> T \<and> open T \<and> (\<forall>y\<in>t. y \<in> T \<longrightarrow> y = x)"]
```
```  1604     by auto
```
```  1605   obtain g where g: "g \<subseteq> {t. \<exists>x. x \<in> s \<and> t = f x}" "finite g" "s \<subseteq> \<Union>g"
```
```  1606     using assms(1)[unfolded compact_eq_Heine_Borel, THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]]
```
```  1607     using f by auto
```
```  1608   from g(1,3) have g':"\<forall>x\<in>g. \<exists>xa \<in> s. x = f xa"
```
```  1609     by auto
```
```  1610   {
```
```  1611     fix x y
```
```  1612     assume "x \<in> t" "y \<in> t" "f x = f y"
```
```  1613     then have "x \<in> f x"  "y \<in> f x \<longrightarrow> y = x"
```
```  1614       using f[THEN bspec[where x=x]] and \<open>t \<subseteq> s\<close> by auto
```
```  1615     then have "x = y"
```
```  1616       using \<open>f x = f y\<close> and f[THEN bspec[where x=y]] and \<open>y \<in> t\<close> and \<open>t \<subseteq> s\<close>
```
```  1617       by auto
```
```  1618   }
```
```  1619   then have "inj_on f t"
```
```  1620     unfolding inj_on_def by simp
```
```  1621   then have "infinite (f ` t)"
```
```  1622     using assms(2) using finite_imageD by auto
```
```  1623   moreover
```
```  1624   {
```
```  1625     fix x
```
```  1626     assume "x \<in> t" "f x \<notin> g"
```
```  1627     from g(3) assms(3) \<open>x \<in> t\<close> obtain h where "h \<in> g" and "x \<in> h"
```
```  1628       by auto
```
```  1629     then obtain y where "y \<in> s" "h = f y"
```
```  1630       using g'[THEN bspec[where x=h]] by auto
```
```  1631     then have "y = x"
```
```  1632       using f[THEN bspec[where x=y]] and \<open>x\<in>t\<close> and \<open>x\<in>h\<close>[unfolded \<open>h = f y\<close>]
```
```  1633       by auto
```
```  1634     then have False
```
```  1635       using \<open>f x \<notin> g\<close> \<open>h \<in> g\<close> unfolding \<open>h = f y\<close>
```
```  1636       by auto
```
```  1637   }
```
```  1638   then have "f ` t \<subseteq> g" by auto
```
```  1639   ultimately show False
```
```  1640     using g(2) using finite_subset by auto
```
```  1641 qed
```
```  1642
```
```  1643 lemma sequence_infinite_lemma:
```
```  1644   fixes f :: "nat \<Rightarrow> 'a::t1_space"
```
```  1645   assumes "\<forall>n. f n \<noteq> l"
```
```  1646     and "(f \<longlongrightarrow> l) sequentially"
```
```  1647   shows "infinite (range f)"
```
```  1648 proof
```
```  1649   assume "finite (range f)"
```
```  1650   then have "closed (range f)"
```
```  1651     by (rule finite_imp_closed)
```
```  1652   then have "open (- range f)"
```
```  1653     by (rule open_Compl)
```
```  1654   from assms(1) have "l \<in> - range f"
```
```  1655     by auto
```
```  1656   from assms(2) have "eventually (\<lambda>n. f n \<in> - range f) sequentially"
```
```  1657     using \<open>open (- range f)\<close> \<open>l \<in> - range f\<close>
```
```  1658     by (rule topological_tendstoD)
```
```  1659   then show False
```
```  1660     unfolding eventually_sequentially
```
```  1661     by auto
```
```  1662 qed
```
```  1663
```
```  1664 lemma Bolzano_Weierstrass_imp_closed:
```
```  1665   fixes s :: "'a::{first_countable_topology,t2_space} set"
```
```  1666   assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
```
```  1667   shows "closed s"
```
```  1668 proof -
```
```  1669   {
```
```  1670     fix x l
```
```  1671     assume as: "\<forall>n::nat. x n \<in> s" "(x \<longlongrightarrow> l) sequentially"
```
```  1672     then have "l \<in> s"
```
```  1673     proof (cases "\<forall>n. x n \<noteq> l")
```
```  1674       case False
```
```  1675       then show "l\<in>s" using as(1) by auto
```
```  1676     next
```
```  1677       case True note cas = this
```
```  1678       with as(2) have "infinite (range x)"
```
```  1679         using sequence_infinite_lemma[of x l] by auto
```
```  1680       then obtain l' where "l'\<in>s" "l' islimpt (range x)"
```
```  1681         using assms[THEN spec[where x="range x"]] as(1) by auto
```
```  1682       then show "l\<in>s" using sequence_unique_limpt[of x l l']
```
```  1683         using as cas by auto
```
```  1684     qed
```
```  1685   }
```
```  1686   then show ?thesis
```
```  1687     unfolding closed_sequential_limits by fast
```
```  1688 qed
```
```  1689
```
```  1690 lemma closure_insert:
```
```  1691   fixes x :: "'a::t1_space"
```
```  1692   shows "closure (insert x s) = insert x (closure s)"
```
```  1693   apply (rule closure_unique)
```
```  1694   apply (rule insert_mono [OF closure_subset])
```
```  1695   apply (rule closed_insert [OF closed_closure])
```
```  1696   apply (simp add: closure_minimal)
```
```  1697   done
```
```  1698
```
```  1699
```
```  1700 text\<open>In particular, some common special cases.\<close>
```
```  1701
```
```  1702 lemma compact_Un [intro]:
```
```  1703   assumes "compact s"
```
```  1704     and "compact t"
```
```  1705   shows " compact (s \<union> t)"
```
```  1706 proof (rule compactI)
```
```  1707   fix f
```
```  1708   assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
```
```  1709   from * \<open>compact s\<close> obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
```
```  1710     unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
```
```  1711   moreover
```
```  1712   from * \<open>compact t\<close> obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
```
```  1713     unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
```
```  1714   ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
```
```  1715     by (auto intro!: exI[of _ "s' \<union> t'"])
```
```  1716 qed
```
```  1717
```
```  1718 lemma compact_Union [intro]: "finite S \<Longrightarrow> (\<And>T. T \<in> S \<Longrightarrow> compact T) \<Longrightarrow> compact (\<Union>S)"
```
```  1719   by (induct set: finite) auto
```
```  1720
```
```  1721 lemma compact_UN [intro]:
```
```  1722   "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
```
```  1723   by (rule compact_Union) auto
```
```  1724
```
```  1725 lemma closed_Int_compact [intro]:
```
```  1726   assumes "closed s"
```
```  1727     and "compact t"
```
```  1728   shows "compact (s \<inter> t)"
```
```  1729   using compact_Int_closed [of t s] assms
```
```  1730   by (simp add: Int_commute)
```
```  1731
```
```  1732 lemma compact_Int [intro]:
```
```  1733   fixes s t :: "'a :: t2_space set"
```
```  1734   assumes "compact s"
```
```  1735     and "compact t"
```
```  1736   shows "compact (s \<inter> t)"
```
```  1737   using assms by (intro compact_Int_closed compact_imp_closed)
```
```  1738
```
```  1739 lemma compact_sing [simp]: "compact {a}"
```
```  1740   unfolding compact_eq_Heine_Borel by auto
```
```  1741
```
```  1742 lemma compact_insert [simp]:
```
```  1743   assumes "compact s"
```
```  1744   shows "compact (insert x s)"
```
```  1745 proof -
```
```  1746   have "compact ({x} \<union> s)"
```
```  1747     using compact_sing assms by (rule compact_Un)
```
```  1748   then show ?thesis by simp
```
```  1749 qed
```
```  1750
```
```  1751 lemma finite_imp_compact: "finite s \<Longrightarrow> compact s"
```
```  1752   by (induct set: finite) simp_all
```
```  1753
```
```  1754 lemma open_delete:
```
```  1755   fixes s :: "'a::t1_space set"
```
```  1756   shows "open s \<Longrightarrow> open (s - {x})"
```
```  1757   by (simp add: open_Diff)
```
```  1758
```
```  1759
```
```  1760 text\<open>Compactness expressed with filters\<close>
```
```  1761
```
```  1762 lemma closure_iff_nhds_not_empty:
```
```  1763   "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})"
```
```  1764 proof safe
```
```  1765   assume x: "x \<in> closure X"
```
```  1766   fix S A
```
```  1767   assume "open S" "x \<in> S" "X \<inter> A = {}" "S \<subseteq> A"
```
```  1768   then have "x \<notin> closure (-S)"
```
```  1769     by (auto simp: closure_complement subset_eq[symmetric] intro: interiorI)
```
```  1770   with x have "x \<in> closure X - closure (-S)"
```
```  1771     by auto
```
```  1772   also have "\<dots> \<subseteq> closure (X \<inter> S)"
```
```  1773     using \<open>open S\<close> open_Int_closure_subset[of S X] by (simp add: closed_Compl ac_simps)
```
```  1774   finally have "X \<inter> S \<noteq> {}" by auto
```
```  1775   then show False using \<open>X \<inter> A = {}\<close> \<open>S \<subseteq> A\<close> by auto
```
```  1776 next
```
```  1777   assume "\<forall>A S. S \<subseteq> A \<longrightarrow> open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {}"
```
```  1778   from this[THEN spec, of "- X", THEN spec, of "- closure X"]
```
```  1779   show "x \<in> closure X"
```
```  1780     by (simp add: closure_subset open_Compl)
```
```  1781 qed
```
```  1782
```
```  1783 lemma compact_filter:
```
```  1784   "compact U \<longleftrightarrow> (\<forall>F. F \<noteq> bot \<longrightarrow> eventually (\<lambda>x. x \<in> U) F \<longrightarrow> (\<exists>x\<in>U. inf (nhds x) F \<noteq> bot))"
```
```  1785 proof (intro allI iffI impI compact_fip[THEN iffD2] notI)
```
```  1786   fix F
```
```  1787   assume "compact U"
```
```  1788   assume F: "F \<noteq> bot" "eventually (\<lambda>x. x \<in> U) F"
```
```  1789   then have "U \<noteq> {}"
```
```  1790     by (auto simp: eventually_False)
```
```  1791
```
```  1792   define Z where "Z = closure ` {A. eventually (\<lambda>x. x \<in> A) F}"
```
```  1793   then have "\<forall>z\<in>Z. closed z"
```
```  1794     by auto
```
```  1795   moreover
```
```  1796   have ev_Z: "\<And>z. z \<in> Z \<Longrightarrow> eventually (\<lambda>x. x \<in> z) F"
```
```  1797     unfolding Z_def by (auto elim: eventually_mono intro: subsetD[OF closure_subset])
```
```  1798   have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
```
```  1799   proof (intro allI impI)
```
```  1800     fix B assume "finite B" "B \<subseteq> Z"
```
```  1801     with \<open>finite B\<close> ev_Z F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
```
```  1802       by (auto simp: eventually_ball_finite_distrib eventually_conj_iff)
```
```  1803     with F show "U \<inter> \<Inter>B \<noteq> {}"
```
```  1804       by (intro notI) (simp add: eventually_False)
```
```  1805   qed
```
```  1806   ultimately have "U \<inter> \<Inter>Z \<noteq> {}"
```
```  1807     using \<open>compact U\<close> unfolding compact_fip by blast
```
```  1808   then obtain x where "x \<in> U" and x: "\<And>z. z \<in> Z \<Longrightarrow> x \<in> z"
```
```  1809     by auto
```
```  1810
```
```  1811   have "\<And>P. eventually P (inf (nhds x) F) \<Longrightarrow> P \<noteq> bot"
```
```  1812     unfolding eventually_inf eventually_nhds
```
```  1813   proof safe
```
```  1814     fix P Q R S
```
```  1815     assume "eventually R F" "open S" "x \<in> S"
```
```  1816     with open_Int_closure_eq_empty[of S "{x. R x}"] x[of "closure {x. R x}"]
```
```  1817     have "S \<inter> {x. R x} \<noteq> {}" by (auto simp: Z_def)
```
```  1818     moreover assume "Ball S Q" "\<forall>x. Q x \<and> R x \<longrightarrow> bot x"
```
```  1819     ultimately show False by (auto simp: set_eq_iff)
```
```  1820   qed
```
```  1821   with \<open>x \<in> U\<close> show "\<exists>x\<in>U. inf (nhds x) F \<noteq> bot"
```
```  1822     by (metis eventually_bot)
```
```  1823 next
```
```  1824   fix A
```
```  1825   assume A: "\<forall>a\<in>A. closed a" "\<forall>B\<subseteq>A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}" "U \<inter> \<Inter>A = {}"
```
```  1826   define F where "F = (INF a\<in>insert U A. principal a)"
```
```  1827   have "F \<noteq> bot"
```
```  1828     unfolding F_def
```
```  1829   proof (rule INF_filter_not_bot)
```
```  1830     fix X
```
```  1831     assume X: "X \<subseteq> insert U A" "finite X"
```
```  1832     with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
```
```  1833       by auto
```
```  1834     with X show "(INF a\<in>X. principal a) \<noteq> bot"
```
```  1835       by (auto simp: INF_principal_finite principal_eq_bot_iff)
```
```  1836   qed
```
```  1837   moreover
```
```  1838   have "F \<le> principal U"
```
```  1839     unfolding F_def by auto
```
```  1840   then have "eventually (\<lambda>x. x \<in> U) F"
```
```  1841     by (auto simp: le_filter_def eventually_principal)
```
```  1842   moreover
```
```  1843   assume "\<forall>F. F \<noteq> bot \<longrightarrow> eventually (\<lambda>x. x \<in> U) F \<longrightarrow> (\<exists>x\<in>U. inf (nhds x) F \<noteq> bot)"
```
```  1844   ultimately obtain x where "x \<in> U" and x: "inf (nhds x) F \<noteq> bot"
```
```  1845     by auto
```
```  1846
```
```  1847   { fix V assume "V \<in> A"
```
```  1848     then have "F \<le> principal V"
```
```  1849       unfolding F_def by (intro INF_lower2[of V]) auto
```
```  1850     then have V: "eventually (\<lambda>x. x \<in> V) F"
```
```  1851       by (auto simp: le_filter_def eventually_principal)
```
```  1852     have "x \<in> closure V"
```
```  1853       unfolding closure_iff_nhds_not_empty
```
```  1854     proof (intro impI allI)
```
```  1855       fix S A
```
```  1856       assume "open S" "x \<in> S" "S \<subseteq> A"
```
```  1857       then have "eventually (\<lambda>x. x \<in> A) (nhds x)"
```
```  1858         by (auto simp: eventually_nhds)
```
```  1859       with V have "eventually (\<lambda>x. x \<in> V \<inter> A) (inf (nhds x) F)"
```
```  1860         by (auto simp: eventually_inf)
```
```  1861       with x show "V \<inter> A \<noteq> {}"
```
```  1862         by (auto simp del: Int_iff simp add: trivial_limit_def)
```
```  1863     qed
```
```  1864     then have "x \<in> V"
```
```  1865       using \<open>V \<in> A\<close> A(1) by simp
```
```  1866   }
```
```  1867   with \<open>x\<in>U\<close> have "x \<in> U \<inter> \<Inter>A" by auto
```
```  1868   with \<open>U \<inter> \<Inter>A = {}\<close> show False by auto
```
```  1869 qed
```
```  1870
```
```  1871 definition%important countably_compact :: "('a::topological_space) set \<Rightarrow> bool" where
```
```  1872 "countably_compact U \<longleftrightarrow>
```
```  1873   (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A
```
```  1874      \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))"
```
```  1875
```
```  1876 lemma countably_compactE:
```
```  1877   assumes "countably_compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C" "countable C"
```
```  1878   obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'"
```
```  1879   using assms unfolding countably_compact_def by metis
```
```  1880
```
```  1881 lemma countably_compactI:
```
```  1882   assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union>C \<Longrightarrow> countable C \<Longrightarrow> (\<exists>C'\<subseteq>C. finite C' \<and> s \<subseteq> \<Union>C')"
```
```  1883   shows "countably_compact s"
```
```  1884   using assms unfolding countably_compact_def by metis
```
```  1885
```
```  1886 lemma compact_imp_countably_compact: "compact U \<Longrightarrow> countably_compact U"
```
```  1887   by (auto simp: compact_eq_Heine_Borel countably_compact_def)
```
```  1888
```
```  1889 lemma countably_compact_imp_compact:
```
```  1890   assumes "countably_compact U"
```
```  1891     and ccover: "countable B" "\<forall>b\<in>B. open b"
```
```  1892     and basis: "\<And>T x. open T \<Longrightarrow> x \<in> T \<Longrightarrow> x \<in> U \<Longrightarrow> \<exists>b\<in>B. x \<in> b \<and> b \<inter> U \<subseteq> T"
```
```  1893   shows "compact U"
```
```  1894   using \<open>countably_compact U\<close>
```
```  1895   unfolding compact_eq_Heine_Borel countably_compact_def
```
```  1896 proof safe
```
```  1897   fix A
```
```  1898   assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
```
```  1899   assume *: "\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T)"
```
```  1900   moreover define C where "C = {b\<in>B. \<exists>a\<in>A. b \<inter> U \<subseteq> a}"
```
```  1901   ultimately have "countable C" "\<forall>a\<in>C. open a"
```
```  1902     unfolding C_def using ccover by auto
```
```  1903   moreover
```
```  1904   have "\<Union>A \<inter> U \<subseteq> \<Union>C"
```
```  1905   proof safe
```
```  1906     fix x a
```
```  1907     assume "x \<in> U" "x \<in> a" "a \<in> A"
```
```  1908     with basis[of a x] A obtain b where "b \<in> B" "x \<in> b" "b \<inter> U \<subseteq> a"
```
```  1909       by blast
```
```  1910     with \<open>a \<in> A\<close> show "x \<in> \<Union>C"
```
```  1911       unfolding C_def by auto
```
```  1912   qed
```
```  1913   then have "U \<subseteq> \<Union>C" using \<open>U \<subseteq> \<Union>A\<close> by auto
```
```  1914   ultimately obtain T where T: "T\<subseteq>C" "finite T" "U \<subseteq> \<Union>T"
```
```  1915     using * by metis
```
```  1916   then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
```
```  1917     by (auto simp: C_def)
```
```  1918   then obtain f where "\<forall>t\<in>T. f t \<in> A \<and> t \<inter> U \<subseteq> f t"
```
```  1919     unfolding bchoice_iff Bex_def ..
```
```  1920   with T show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
```
```  1921     unfolding C_def by (intro exI[of _ "f`T"]) fastforce
```
```  1922 qed
```
```  1923
```
```  1924 proposition countably_compact_imp_compact_second_countable:
```
```  1925   "countably_compact U \<Longrightarrow> compact (U :: 'a :: second_countable_topology set)"
```
```  1926 proof (rule countably_compact_imp_compact)
```
```  1927   fix T and x :: 'a
```
```  1928   assume "open T" "x \<in> T"
```
```  1929   from topological_basisE[OF is_basis this] obtain b where
```
```  1930     "b \<in> (SOME B. countable B \<and> topological_basis B)" "x \<in> b" "b \<subseteq> T" .
```
```  1931   then show "\<exists>b\<in>SOME B. countable B \<and> topological_basis B. x \<in> b \<and> b \<inter> U \<subseteq> T"
```
```  1932     by blast
```
```  1933 qed (insert countable_basis topological_basis_open[OF is_basis], auto)
```
```  1934
```
```  1935 lemma countably_compact_eq_compact:
```
```  1936   "countably_compact U \<longleftrightarrow> compact (U :: 'a :: second_countable_topology set)"
```
```  1937   using countably_compact_imp_compact_second_countable compact_imp_countably_compact by blast
```
```  1938
```
```  1939 subsubsection\<open>Sequential compactness\<close>
```
```  1940
```
```  1941 definition%important seq_compact :: "'a::topological_space set \<Rightarrow> bool" where
```
```  1942 "seq_compact S \<longleftrightarrow>
```
```  1943   (\<forall>f. (\<forall>n. f n \<in> S)
```
```  1944     \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
```
```  1945
```
```  1946 lemma seq_compactI:
```
```  1947   assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
```
```  1948   shows "seq_compact S"
```
```  1949   unfolding seq_compact_def using assms by fast
```
```  1950
```
```  1951 lemma seq_compactE:
```
```  1952   assumes "seq_compact S" "\<forall>n. f n \<in> S"
```
```  1953   obtains l r where "l \<in> S" "strict_mono (r :: nat \<Rightarrow> nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
```
```  1954   using assms unfolding seq_compact_def by fast
```
```  1955
```
```  1956 lemma closed_sequentially: (* TODO: move upwards *)
```
```  1957   assumes "closed s" and "\<forall>n. f n \<in> s" and "f \<longlonglongrightarrow> l"
```
```  1958   shows "l \<in> s"
```
```  1959 proof (rule ccontr)
```
```  1960   assume "l \<notin> s"
```
```  1961   with \<open>closed s\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "eventually (\<lambda>n. f n \<in> - s) sequentially"
```
```  1962     by (fast intro: topological_tendstoD)
```
```  1963   with \<open>\<forall>n. f n \<in> s\<close> show "False"
```
```  1964     by simp
```
```  1965 qed
```
```  1966
```
```  1967 lemma seq_compact_Int_closed:
```
```  1968   assumes "seq_compact s" and "closed t"
```
```  1969   shows "seq_compact (s \<inter> t)"
```
```  1970 proof (rule seq_compactI)
```
```  1971   fix f assume "\<forall>n::nat. f n \<in> s \<inter> t"
```
```  1972   hence "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
```
```  1973     by simp_all
```
```  1974   from \<open>seq_compact s\<close> and \<open>\<forall>n. f n \<in> s\<close>
```
```  1975   obtain l r where "l \<in> s" and r: "strict_mono r" and l: "(f \<circ> r) \<longlonglongrightarrow> l"
```
```  1976     by (rule seq_compactE)
```
```  1977   from \<open>\<forall>n. f n \<in> t\<close> have "\<forall>n. (f \<circ> r) n \<in> t"
```
```  1978     by simp
```
```  1979   from \<open>closed t\<close> and this and l have "l \<in> t"
```
```  1980     by (rule closed_sequentially)
```
```  1981   with \<open>l \<in> s\<close> and r and l show "\<exists>l\<in>s \<inter> t. \<exists>r. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
```
```  1982     by fast
```
```  1983 qed
```
```  1984
```
```  1985 lemma seq_compact_closed_subset:
```
```  1986   assumes "closed s" and "s \<subseteq> t" and "seq_compact t"
```
```  1987   shows "seq_compact s"
```
```  1988   using assms seq_compact_Int_closed [of t s] by (simp add: Int_absorb1)
```
```  1989
```
```  1990 lemma seq_compact_imp_countably_compact:
```
```  1991   fixes U :: "'a :: first_countable_topology set"
```
```  1992   assumes "seq_compact U"
```
```  1993   shows "countably_compact U"
```
```  1994 proof (safe intro!: countably_compactI)
```
```  1995   fix A
```
```  1996   assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
```
```  1997   have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> strict_mono (r :: nat \<Rightarrow> nat) \<and> (X \<circ> r) \<longlonglongrightarrow> x"
```
```  1998     using \<open>seq_compact U\<close> by (fastforce simp: seq_compact_def subset_eq)
```
```  1999   show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
```
```  2000   proof cases
```
```  2001     assume "finite A"
```
```  2002     with A show ?thesis by auto
```
```  2003   next
```
```  2004     assume "infinite A"
```
```  2005     then have "A \<noteq> {}" by auto
```
```  2006     show ?thesis
```
```  2007     proof (rule ccontr)
```
```  2008       assume "\<not> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T)"
```
```  2009       then have "\<forall>T. \<exists>x. T \<subseteq> A \<and> finite T \<longrightarrow> (x \<in> U - \<Union>T)"
```
```  2010         by auto
```
```  2011       then obtain X' where T: "\<And>T. T \<subseteq> A \<Longrightarrow> finite T \<Longrightarrow> X' T \<in> U - \<Union>T"
```
```  2012         by metis
```
```  2013       define X where "X n = X' (from_nat_into A ` {.. n})" for n
```
```  2014       have X: "\<And>n. X n \<in> U - (\<Union>i\<le>n. from_nat_into A i)"
```
```  2015         using \<open>A \<noteq> {}\<close> unfolding X_def by (intro T) (auto intro: from_nat_into)
```
```  2016       then have "range X \<subseteq> U"
```
```  2017         by auto
```
```  2018       with subseq[of X] obtain r x where "x \<in> U" and r: "strict_mono r" "(X \<circ> r) \<longlonglongrightarrow> x"
```
```  2019         by auto
```
```  2020       from \<open>x\<in>U\<close> \<open>U \<subseteq> \<Union>A\<close> from_nat_into_surj[OF \<open>countable A\<close>]
```
```  2021       obtain n where "x \<in> from_nat_into A n" by auto
```
```  2022       with r(2) A(1) from_nat_into[OF \<open>A \<noteq> {}\<close>, of n]
```
```  2023       have "eventually (\<lambda>i. X (r i) \<in> from_nat_into A n) sequentially"
```
```  2024         unfolding tendsto_def by (auto simp: comp_def)
```
```  2025       then obtain N where "\<And>i. N \<le> i \<Longrightarrow> X (r i) \<in> from_nat_into A n"
```
```  2026         by (auto simp: eventually_sequentially)
```
```  2027       moreover from X have "\<And>i. n \<le> r i \<Longrightarrow> X (r i) \<notin> from_nat_into A n"
```
```  2028         by auto
```
```  2029       moreover from \<open>strict_mono r\<close>[THEN seq_suble, of "max n N"] have "\<exists>i. n \<le> r i \<and> N \<le> i"
```
```  2030         by (auto intro!: exI[of _ "max n N"])
```
```  2031       ultimately show False
```
```  2032         by auto
```
```  2033     qed
```
```  2034   qed
```
```  2035 qed
```
```  2036
```
```  2037 lemma compact_imp_seq_compact:
```
```  2038   fixes U :: "'a :: first_countable_topology set"
```
```  2039   assumes "compact U"
```
```  2040   shows "seq_compact U"
```
```  2041   unfolding seq_compact_def
```
```  2042 proof safe
```
```  2043   fix X :: "nat \<Rightarrow> 'a"
```
```  2044   assume "\<forall>n. X n \<in> U"
```
```  2045   then have "eventually (\<lambda>x. x \<in> U) (filtermap X sequentially)"
```
```  2046     by (auto simp: eventually_filtermap)
```
```  2047   moreover
```
```  2048   have "filtermap X sequentially \<noteq> bot"
```
```  2049     by (simp add: trivial_limit_def eventually_filtermap)
```
```  2050   ultimately
```
```  2051   obtain x where "x \<in> U" and x: "inf (nhds x) (filtermap X sequentially) \<noteq> bot" (is "?F \<noteq> _")
```
```  2052     using \<open>compact U\<close> by (auto simp: compact_filter)
```
```  2053
```
```  2054   from countable_basis_at_decseq[of x]
```
```  2055   obtain A where A:
```
```  2056       "\<And>i. open (A i)"
```
```  2057       "\<And>i. x \<in> A i"
```
```  2058       "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
```
```  2059     by blast
```
```  2060   define s where "s n i = (SOME j. i < j \<and> X j \<in> A (Suc n))" for n i
```
```  2061   {
```
```  2062     fix n i
```
```  2063     have "\<exists>a. i < a \<and> X a \<in> A (Suc n)"
```
```  2064     proof (rule ccontr)
```
```  2065       assume "\<not> (\<exists>a>i. X a \<in> A (Suc n))"
```
```  2066       then have "\<And>a. Suc i \<le> a \<Longrightarrow> X a \<notin> A (Suc n)"
```
```  2067         by auto
```
```  2068       then have "eventually (\<lambda>x. x \<notin> A (Suc n)) (filtermap X sequentially)"
```
```  2069         by (auto simp: eventually_filtermap eventually_sequentially)
```
```  2070       moreover have "eventually (\<lambda>x. x \<in> A (Suc n)) (nhds x)"
```
```  2071         using A(1,2)[of "Suc n"] by (auto simp: eventually_nhds)
```
```  2072       ultimately have "eventually (\<lambda>x. False) ?F"
```
```  2073         by (auto simp: eventually_inf)
```
```  2074       with x show False
```
```  2075         by (simp add: eventually_False)
```
```  2076     qed
```
```  2077     then have "i < s n i" "X (s n i) \<in> A (Suc n)"
```
```  2078       unfolding s_def by (auto intro: someI2_ex)
```
```  2079   }
```
```  2080   note s = this
```
```  2081   define r where "r = rec_nat (s 0 0) s"
```
```  2082   have "strict_mono r"
```
```  2083     by (auto simp: r_def s strict_mono_Suc_iff)
```
```  2084   moreover
```
```  2085   have "(\<lambda>n. X (r n)) \<longlonglongrightarrow> x"
```
```  2086   proof (rule topological_tendstoI)
```
```  2087     fix S
```
```  2088     assume "open S" "x \<in> S"
```
```  2089     with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially"
```
```  2090       by auto
```
```  2091     moreover
```
```  2092     {
```
```  2093       fix i
```
```  2094       assume "Suc 0 \<le> i"
```
```  2095       then have "X (r i) \<in> A i"
```
```  2096         by (cases i) (simp_all add: r_def s)
```
```  2097     }
```
```  2098     then have "eventually (\<lambda>i. X (r i) \<in> A i) sequentially"
```
```  2099       by (auto simp: eventually_sequentially)
```
```  2100     ultimately show "eventually (\<lambda>i. X (r i) \<in> S) sequentially"
```
```  2101       by eventually_elim auto
```
```  2102   qed
```
```  2103   ultimately show "\<exists>x \<in> U. \<exists>r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
```
```  2104     using \<open>x \<in> U\<close> by (auto simp: convergent_def comp_def)
```
```  2105 qed
```
```  2106
```
```  2107 lemma countably_compact_imp_acc_point:
```
```  2108   assumes "countably_compact s"
```
```  2109     and "countable t"
```
```  2110     and "infinite t"
```
```  2111     and "t \<subseteq> s"
```
```  2112   shows "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t)"
```
```  2113 proof (rule ccontr)
```
```  2114   define C where "C = (\<lambda>F. interior (F \<union> (- t))) ` {F. finite F \<and> F \<subseteq> t }"
```
```  2115   note \<open>countably_compact s\<close>
```
```  2116   moreover have "\<forall>t\<in>C. open t"
```
```  2117     by (auto simp: C_def)
```
```  2118   moreover
```
```  2119   assume "\<not> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t))"
```
```  2120   then have s: "\<And>x. x \<in> s \<Longrightarrow> \<exists>U. x\<in>U \<and> open U \<and> finite (U \<inter> t)" by metis
```
```  2121   have "s \<subseteq> \<Union>C"
```
```  2122     using \<open>t \<subseteq> s\<close>
```
```  2123     unfolding C_def
```
```  2124     apply (safe dest!: s)
```
```  2125     apply (rule_tac a="U \<inter> t" in UN_I)
```
```  2126     apply (auto intro!: interiorI simp add: finite_subset)
```
```  2127     done
```
```  2128   moreover
```
```  2129   from \<open>countable t\<close> have "countable C"
```
```  2130     unfolding C_def by (auto intro: countable_Collect_finite_subset)
```
```  2131   ultimately
```
```  2132   obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> \<Union>D"
```
```  2133     by (rule countably_compactE)
```
```  2134   then obtain E where E: "E \<subseteq> {F. finite F \<and> F \<subseteq> t }" "finite E"
```
```  2135     and s: "s \<subseteq> (\<Union>F\<in>E. interior (F \<union> (- t)))"
```
```  2136     by (metis (lifting) finite_subset_image C_def)
```
```  2137   from s \<open>t \<subseteq> s\<close> have "t \<subseteq> \<Union>E"
```
```  2138     using interior_subset by blast
```
```  2139   moreover have "finite (\<Union>E)"
```
```  2140     using E by auto
```
```  2141   ultimately show False using \<open>infinite t\<close>
```
```  2142     by (auto simp: finite_subset)
```
```  2143 qed
```
```  2144
```
```  2145 lemma countable_acc_point_imp_seq_compact:
```
```  2146   fixes s :: "'a::first_countable_topology set"
```
```  2147   assumes "\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s \<longrightarrow>
```
```  2148     (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t))"
```
```  2149   shows "seq_compact s"
```
```  2150 proof -
```
```  2151   {
```
```  2152     fix f :: "nat \<Rightarrow> 'a"
```
```  2153     assume f: "\<forall>n. f n \<in> s"
```
```  2154     have "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
```
```  2155     proof (cases "finite (range f)")
```
```  2156       case True
```
```  2157       obtain l where "infinite {n. f n = f l}"
```
```  2158         using pigeonhole_infinite[OF _ True] by auto
```
```  2159       then obtain r :: "nat \<Rightarrow> nat" where "strict_mono  r" and fr: "\<forall>n. f (r n) = f l"
```
```  2160         using infinite_enumerate by blast
```
```  2161       then have "strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> f l"
```
```  2162         by (simp add: fr o_def)
```
```  2163       with f show "\<exists>l\<in>s. \<exists>r. strict_mono  r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
```
```  2164         by auto
```
```  2165     next
```
```  2166       case False
```
```  2167       with f assms have "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)"
```
```  2168         by auto
```
```  2169       then obtain l where "l \<in> s" "\<forall>U. l\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)" ..
```
```  2170       from this(2) have "\<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
```
```  2171         using acc_point_range_imp_convergent_subsequence[of l f] by auto
```
```  2172       with \<open>l \<in> s\<close> show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" ..
```
```  2173     qed
```
```  2174   }
```
```  2175   then show ?thesis
```
```  2176     unfolding seq_compact_def by auto
```
```  2177 qed
```
```  2178
```
```  2179 lemma seq_compact_eq_countably_compact:
```
```  2180   fixes U :: "'a :: first_countable_topology set"
```
```  2181   shows "seq_compact U \<longleftrightarrow> countably_compact U"
```
```  2182   using
```
```  2183     countable_acc_point_imp_seq_compact
```
```  2184     countably_compact_imp_acc_point
```
```  2185     seq_compact_imp_countably_compact
```
```  2186   by metis
```
```  2187
```
```  2188 lemma seq_compact_eq_acc_point:
```
```  2189   fixes s :: "'a :: first_countable_topology set"
```
```  2190   shows "seq_compact s \<longleftrightarrow>
```
```  2191     (\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s --> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t)))"
```
```  2192   using
```
```  2193     countable_acc_point_imp_seq_compact[of s]
```
```  2194     countably_compact_imp_acc_point[of s]
```
```  2195     seq_compact_imp_countably_compact[of s]
```
```  2196   by metis
```
```  2197
```
```  2198 lemma seq_compact_eq_compact:
```
```  2199   fixes U :: "'a :: second_countable_topology set"
```
```  2200   shows "seq_compact U \<longleftrightarrow> compact U"
```
```  2201   using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
```
```  2202
```
```  2203 proposition Bolzano_Weierstrass_imp_seq_compact:
```
```  2204   fixes s :: "'a::{t1_space, first_countable_topology} set"
```
```  2205   shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
```
```  2206   by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
```
```  2207
```
```  2208
```
```  2209 subsection%unimportant \<open>Cartesian products\<close>
```
```  2210
```
```  2211 lemma seq_compact_Times: "seq_compact s \<Longrightarrow> seq_compact t \<Longrightarrow> seq_compact (s \<times> t)"
```
```  2212   unfolding seq_compact_def
```
```  2213   apply clarify
```
```  2214   apply (drule_tac x="fst \<circ> f" in spec)
```
```  2215   apply (drule mp, simp add: mem_Times_iff)
```
```  2216   apply (clarify, rename_tac l1 r1)
```
```  2217   apply (drule_tac x="snd \<circ> f \<circ> r1" in spec)
```
```  2218   apply (drule mp, simp add: mem_Times_iff)
```
```  2219   apply (clarify, rename_tac l2 r2)
```
```  2220   apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
```
```  2221   apply (rule_tac x="r1 \<circ> r2" in exI)
```
```  2222   apply (rule conjI, simp add: strict_mono_def)
```
```  2223   apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption)
```
```  2224   apply (drule (1) tendsto_Pair) back
```
```  2225   apply (simp add: o_def)
```
```  2226   done
```
```  2227
```
```  2228 lemma compact_Times:
```
```  2229   assumes "compact s" "compact t"
```
```  2230   shows "compact (s \<times> t)"
```
```  2231 proof (rule compactI)
```
```  2232   fix C
```
```  2233   assume C: "\<forall>t\<in>C. open t" "s \<times> t \<subseteq> \<Union>C"
```
```  2234   have "\<forall>x\<in>s. \<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
```
```  2235   proof
```
```  2236     fix x
```
```  2237     assume "x \<in> s"
```
```  2238     have "\<forall>y\<in>t. \<exists>a b c. c \<in> C \<and> open a \<and> open b \<and> x \<in> a \<and> y \<in> b \<and> a \<times> b \<subseteq> c" (is "\<forall>y\<in>t. ?P y")
```
```  2239     proof
```
```  2240       fix y
```
```  2241       assume "y \<in> t"
```
```  2242       with \<open>x \<in> s\<close> C obtain c where "c \<in> C" "(x, y) \<in> c" "open c" by auto
```
```  2243       then show "?P y" by (auto elim!: open_prod_elim)
```
```  2244     qed
```
```  2245     then obtain a b c where b: "\<And>y. y \<in> t \<Longrightarrow> open (b y)"
```
```  2246       and c: "\<And>y. y \<in> t \<Longrightarrow> c y \<in> C \<and> open (a y) \<and> open (b y) \<and> x \<in> a y \<and> y \<in> b y \<and> a y \<times> b y \<subseteq> c y"
```
```  2247       by metis
```
```  2248     then have "\<forall>y\<in>t. open (b y)" "t \<subseteq> (\<Union>y\<in>t. b y)" by auto
```
```  2249     with compactE_image[OF \<open>compact t\<close>] obtain D where D: "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
```
```  2250       by metis
```
```  2251     moreover from D c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
```
```  2252       by (fastforce simp: subset_eq)
```
```  2253     ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
```
```  2254       using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>(a`D)"] conjI) (auto intro!: open_INT)
```
```  2255   qed
```
```  2256   then obtain a d where a: "\<And>x. x\<in>s \<Longrightarrow> open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
```
```  2257     and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>(d x)"
```
```  2258     unfolding subset_eq UN_iff by metis
```
```  2259   moreover
```
```  2260   from compactE_image[OF \<open>compact s\<close> a]
```
```  2261   obtain e where e: "e \<subseteq> s" "finite e" and s: "s \<subseteq> (\<Union>x\<in>e. a x)"
```
```  2262     by auto
```
```  2263   moreover
```
```  2264   {
```
```  2265     from s have "s \<times> t \<subseteq> (\<Union>x\<in>e. a x \<times> t)"
```
```  2266       by auto
```
```  2267     also have "\<dots> \<subseteq> (\<Union>x\<in>e. \<Union>(d x))"
```
```  2268       using d \<open>e \<subseteq> s\<close> by (intro UN_mono) auto
```
```  2269     finally have "s \<times> t \<subseteq> (\<Union>x\<in>e. \<Union>(d x))" .
```
```  2270   }
```
```  2271   ultimately show "\<exists>C'\<subseteq>C. finite C' \<and> s \<times> t \<subseteq> \<Union>C'"
```
```  2272     by (intro exI[of _ "(\<Union>x\<in>e. d x)"]) (auto simp: subset_eq)
```
```  2273 qed
```
```  2274
```
```  2275
```
```  2276 lemma tube_lemma:
```
```  2277   assumes "compact K"
```
```  2278   assumes "open W"
```
```  2279   assumes "{x0} \<times> K \<subseteq> W"
```
```  2280   shows "\<exists>X0. x0 \<in> X0 \<and> open X0 \<and> X0 \<times> K \<subseteq> W"
```
```  2281 proof -
```
```  2282   {
```
```  2283     fix y assume "y \<in> K"
```
```  2284     then have "(x0, y) \<in> W" using assms by auto
```
```  2285     with \<open>open W\<close>
```
```  2286     have "\<exists>X0 Y. open X0 \<and> open Y \<and> x0 \<in> X0 \<and> y \<in> Y \<and> X0 \<times> Y \<subseteq> W"
```
```  2287       by (rule open_prod_elim) blast
```
```  2288   }
```
```  2289   then obtain X0 Y where
```
```  2290     *: "\<forall>y \<in> K. open (X0 y) \<and> open (Y y) \<and> x0 \<in> X0 y \<and> y \<in> Y y \<and> X0 y \<times> Y y \<subseteq> W"
```
```  2291     by metis
```
```  2292   from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
```
```  2293   with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
```
```  2294     by (meson compactE)
```
```  2295   then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
```
```  2296     by (force intro!: choice)
```
```  2297   with * CC show ?thesis
```
```  2298     by (force intro!: exI[where x="\<Inter>C\<in>CC. X0 (c C)"]) (* SLOW *)
```
```  2299 qed
```
```  2300
```
```  2301 lemma continuous_on_prod_compactE:
```
```  2302   fixes fx::"'a::topological_space \<times> 'b::topological_space \<Rightarrow> 'c::metric_space"
```
```  2303     and e::real
```
```  2304   assumes cont_fx: "continuous_on (U \<times> C) fx"
```
```  2305   assumes "compact C"
```
```  2306   assumes [intro]: "x0 \<in> U"
```
```  2307   notes [continuous_intros] = continuous_on_compose2[OF cont_fx]
```
```  2308   assumes "e > 0"
```
```  2309   obtains X0 where "x0 \<in> X0" "open X0"
```
```  2310     "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
```
```  2311 proof -
```
```  2312   define psi where "psi = (\<lambda>(x, t). dist (fx (x, t)) (fx (x0, t)))"
```
```  2313   define W0 where "W0 = {(x, t) \<in> U \<times> C. psi (x, t) < e}"
```
```  2314   have W0_eq: "W0 = psi -` {..<e} \<inter> U \<times> C"
```
```  2315     by (auto simp: vimage_def W0_def)
```
```  2316   have "open {..<e}" by simp
```
```  2317   have "continuous_on (U \<times> C) psi"
```
```  2318     by (auto intro!: continuous_intros simp: psi_def split_beta')
```
```  2319   from this[unfolded continuous_on_open_invariant, rule_format, OF \<open>open {..<e}\<close>]
```
```  2320   obtain W where W: "open W" "W \<inter> U \<times> C = W0 \<inter> U \<times> C"
```
```  2321     unfolding W0_eq by blast
```
```  2322   have "{x0} \<times> C \<subseteq> W \<inter> U \<times> C"
```
```  2323     unfolding W
```
```  2324     by (auto simp: W0_def psi_def \<open>0 < e\<close>)
```
```  2325   then have "{x0} \<times> C \<subseteq> W" by blast
```
```  2326   from tube_lemma[OF \<open>compact C\<close> \<open>open W\<close> this]
```
```  2327   obtain X0 where X0: "x0 \<in> X0" "open X0" "X0 \<times> C \<subseteq> W"
```
```  2328     by blast
```
```  2329
```
```  2330   have "\<forall>x\<in>X0 \<inter> U. \<forall>t \<in> C. dist (fx (x, t)) (fx (x0, t)) \<le> e"
```
```  2331   proof safe
```
```  2332     fix x assume x: "x \<in> X0" "x \<in> U"
```
```  2333     fix t assume t: "t \<in> C"
```
```  2334     have "dist (fx (x, t)) (fx (x0, t)) = psi (x, t)"
```
```  2335       by (auto simp: psi_def)
```
```  2336     also
```
```  2337     {
```
```  2338       have "(x, t) \<in> X0 \<times> C"
```
```  2339         using t x
```
```  2340         by auto
```
```  2341       also note \<open>\<dots> \<subseteq> W\<close>
```
```  2342       finally have "(x, t) \<in> W" .
```
```  2343       with t x have "(x, t) \<in> W \<inter> U \<times> C"
```
```  2344         by blast
```
```  2345       also note \<open>W \<inter> U \<times> C = W0 \<inter> U \<times> C\<close>
```
```  2346       finally  have "psi (x, t) < e"
```
```  2347         by (auto simp: W0_def)
```
```  2348     }
```
```  2349     finally show "dist (fx (x, t)) (fx (x0, t)) \<le> e" by simp
```
```  2350   qed
```
```  2351   from X0(1,2) this show ?thesis ..
```
```  2352 qed
```
```  2353
```
```  2354
```
```  2355 subsection \<open>Continuity\<close>
```
```  2356
```
```  2357 lemma continuous_at_imp_continuous_within:
```
```  2358   "continuous (at x) f \<Longrightarrow> continuous (at x within s) f"
```
```  2359   unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto
```
```  2360
```
```  2361 lemma Lim_trivial_limit: "trivial_limit net \<Longrightarrow> (f \<longlongrightarrow> l) net"
```
```  2362   by simp
```
```  2363
```
```  2364 lemmas continuous_on = continuous_on_def \<comment> \<open>legacy theorem name\<close>
```
```  2365
```
```  2366 lemma continuous_within_subset:
```
```  2367   "continuous (at x within s) f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous (at x within t) f"
```
```  2368   unfolding continuous_within by(metis tendsto_within_subset)
```
```  2369
```
```  2370 lemma continuous_on_interior:
```
```  2371   "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
```
```  2372   by (metis continuous_on_eq_continuous_at continuous_on_subset interiorE)
```
```  2373
```
```  2374 lemma continuous_on_eq:
```
```  2375   "\<lbrakk>continuous_on s f; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> continuous_on s g"
```
```  2376   unfolding continuous_on_def tendsto_def eventually_at_topological
```
```  2377   by simp
```
```  2378
```
```  2379 text \<open>Characterization of various kinds of continuity in terms of sequences.\<close>
```
```  2380
```
```  2381 lemma continuous_within_sequentiallyI:
```
```  2382   fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::topological_space"
```
```  2383   assumes "\<And>u::nat \<Rightarrow> 'a. u \<longlonglongrightarrow> a \<Longrightarrow> (\<forall>n. u n \<in> s) \<Longrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f a"
```
```  2384   shows "continuous (at a within s) f"
```
```  2385   using assms unfolding continuous_within tendsto_def[where l = "f a"]
```
```  2386   by (auto intro!: sequentially_imp_eventually_within)
```
```  2387
```
```  2388 lemma continuous_within_tendsto_compose:
```
```  2389   fixes f::"'a::t2_space \<Rightarrow> 'b::topological_space"
```
```  2390   assumes "continuous (at a within s) f"
```
```  2391           "eventually (\<lambda>n. x n \<in> s) F"
```
```  2392           "(x \<longlongrightarrow> a) F "
```
```  2393   shows "((\<lambda>n. f (x n)) \<longlongrightarrow> f a) F"
```
```  2394 proof -
```
```  2395   have *: "filterlim x (inf (nhds a) (principal s)) F"
```
```  2396     using assms(2) assms(3) unfolding at_within_def filterlim_inf by (auto simp: filterlim_principal eventually_mono)
```
```  2397   show ?thesis
```
```  2398     by (auto simp: assms(1) continuous_within[symmetric] tendsto_at_within_iff_tendsto_nhds[symmetric] intro!: filterlim_compose[OF _ *])
```
```  2399 qed
```
```  2400
```
```  2401 lemma continuous_within_tendsto_compose':
```
```  2402   fixes f::"'a::t2_space \<Rightarrow> 'b::topological_space"
```
```  2403   assumes "continuous (at a within s) f"
```
```  2404     "\<And>n. x n \<in> s"
```
```  2405     "(x \<longlongrightarrow> a) F "
```
```  2406   shows "((\<lambda>n. f (x n)) \<longlongrightarrow> f a) F"
```
```  2407   by (auto intro!: continuous_within_tendsto_compose[OF assms(1)] simp add: assms)
```
```  2408
```
```  2409 lemma continuous_within_sequentially:
```
```  2410   fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::topological_space"
```
```  2411   shows "continuous (at a within s) f \<longleftrightarrow>
```
```  2412     (\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x \<longlongrightarrow> a) sequentially
```
```  2413          \<longrightarrow> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)"
```
```  2414   using continuous_within_tendsto_compose'[of a s f _ sequentially]
```
```  2415     continuous_within_sequentiallyI[of a s f]
```
```  2416   by (auto simp: o_def)
```
```  2417
```
```  2418 lemma continuous_at_sequentiallyI:
```
```  2419   fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::topological_space"
```
```  2420   assumes "\<And>u. u \<longlonglongrightarrow> a \<Longrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f a"
```
```  2421   shows "continuous (at a) f"
```
```  2422   using continuous_within_sequentiallyI[of a UNIV f] assms by auto
```
```  2423
```
```  2424 lemma continuous_at_sequentially:
```
```  2425   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
```
```  2426   shows "continuous (at a) f \<longleftrightarrow>
```
```  2427     (\<forall>x. (x \<longlongrightarrow> a) sequentially --> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)"
```
```  2428   using continuous_within_sequentially[of a UNIV f] by simp
```
```  2429
```
```  2430 lemma continuous_on_sequentiallyI:
```
```  2431   fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::topological_space"
```
```  2432   assumes "\<And>u a. (\<forall>n. u n \<in> s) \<Longrightarrow> a \<in> s \<Longrightarrow> u \<longlonglongrightarrow> a \<Longrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f a"
```
```  2433   shows "continuous_on s f"
```
```  2434   using assms unfolding continuous_on_eq_continuous_within
```
```  2435   using continuous_within_sequentiallyI[of _ s f] by auto
```
```  2436
```
```  2437 lemma continuous_on_sequentially:
```
```  2438   fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::topological_space"
```
```  2439   shows "continuous_on s f \<longleftrightarrow>
```
```  2440     (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x \<longlongrightarrow> a) sequentially
```
```  2441       --> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)"
```
```  2442     (is "?lhs = ?rhs")
```
```  2443 proof
```
```  2444   assume ?rhs
```
```  2445   then show ?lhs
```
```  2446     using continuous_within_sequentially[of _ s f]
```
```  2447     unfolding continuous_on_eq_continuous_within
```
```  2448     by auto
```
```  2449 next
```
```  2450   assume ?lhs
```
```  2451   then show ?rhs
```
```  2452     unfolding continuous_on_eq_continuous_within
```
```  2453     using continuous_within_sequentially[of _ s f]
```
```  2454     by auto
```
```  2455 qed
```
```  2456
```
```  2457 text \<open>Continuity in terms of open preimages.\<close>
```
```  2458
```
```  2459 lemma continuous_at_open:
```
```  2460   "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
```
```  2461   unfolding continuous_within_topological [of x UNIV f]
```
```  2462   unfolding imp_conjL
```
```  2463   by (intro all_cong imp_cong ex_cong conj_cong refl) auto
```
```  2464
```
```  2465 lemma continuous_imp_tendsto:
```
```  2466   assumes "continuous (at x0) f"
```
```  2467     and "x \<longlonglongrightarrow> x0"
```
```  2468   shows "(f \<circ> x) \<longlonglongrightarrow> (f x0)"
```
```  2469 proof (rule topological_tendstoI)
```
```  2470   fix S
```
```  2471   assume "open S" "f x0 \<in> S"
```
```  2472   then obtain T where T_def: "open T" "x0 \<in> T" "\<forall>x\<in>T. f x \<in> S"
```
```  2473      using assms continuous_at_open by metis
```
```  2474   then have "eventually (\<lambda>n. x n \<in> T) sequentially"
```
```  2475     using assms T_def by (auto simp: tendsto_def)
```
```  2476   then show "eventually (\<lambda>n. (f \<circ> x) n \<in> S) sequentially"
```
```  2477     using T_def by (auto elim!: eventually_mono)
```
```  2478 qed
```
```  2479
```
```  2480 subsection \<open>Homeomorphisms\<close>
```
```  2481
```
```  2482 definition%important "homeomorphism s t f g \<longleftrightarrow>
```
```  2483   (\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
```
```  2484   (\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
```
```  2485
```
```  2486 lemma homeomorphismI [intro?]:
```
```  2487   assumes "continuous_on S f" "continuous_on T g"
```
```  2488           "f ` S \<subseteq> T" "g ` T \<subseteq> S" "\<And>x. x \<in> S \<Longrightarrow> g(f x) = x" "\<And>y. y \<in> T \<Longrightarrow> f(g y) = y"
```
```  2489     shows "homeomorphism S T f g"
```
```  2490   using assms by (force simp: homeomorphism_def)
```
```  2491
```
```  2492 lemma homeomorphism_translation:
```
```  2493   fixes a :: "'a :: real_normed_vector"
```
```  2494   shows "homeomorphism ((+) a ` S) S ((+) (- a)) ((+) a)"
```
```  2495 unfolding homeomorphism_def by (auto simp: algebra_simps continuous_intros)
```
```  2496
```
```  2497 lemma homeomorphism_ident: "homeomorphism T T (\<lambda>a. a) (\<lambda>a. a)"
```
```  2498   by (rule homeomorphismI) auto
```
```  2499
```
```  2500 lemma homeomorphism_compose:
```
```  2501   assumes "homeomorphism S T f g" "homeomorphism T U h k"
```
```  2502     shows "homeomorphism S U (h o f) (g o k)"
```
```  2503   using assms
```
```  2504   unfolding homeomorphism_def
```
```  2505   by (intro conjI ballI continuous_on_compose) (auto simp: image_iff)
```
```  2506
```
```  2507
```
```  2508 lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f"
```
```  2509   by (simp add: homeomorphism_def)
```
```  2510
```
```  2511 lemma homeomorphism_sym: "homeomorphism S t f g = homeomorphism t S g f"
```
```  2512   by (force simp: homeomorphism_def)
```
```  2513
```
```  2514 definition%important homeomorphic :: "'a::topological_space set \<Rightarrow> 'b::topological_space set \<Rightarrow> bool"
```
```  2515     (infixr "homeomorphic" 60)
```
```  2516   where "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
```
```  2517
```
```  2518 lemma homeomorphic_empty [iff]:
```
```  2519      "S homeomorphic {} \<longleftrightarrow> S = {}" "{} homeomorphic S \<longleftrightarrow> S = {}"
```
```  2520   by (auto simp: homeomorphic_def homeomorphism_def)
```
```  2521
```
```  2522 lemma homeomorphic_refl: "s homeomorphic s"
```
```  2523   unfolding homeomorphic_def homeomorphism_def
```
```  2524   using continuous_on_id
```
```  2525   apply (rule_tac x = "(\<lambda>x. x)" in exI)
```
```  2526   apply (rule_tac x = "(\<lambda>x. x)" in exI)
```
```  2527   apply blast
```
```  2528   done
```
```  2529
```
```  2530 lemma homeomorphic_sym: "s homeomorphic t \<longleftrightarrow> t homeomorphic s"
```
```  2531   unfolding homeomorphic_def homeomorphism_def
```
```  2532   by blast
```
```  2533
```
```  2534 lemma homeomorphic_trans [trans]:
```
```  2535   assumes "S homeomorphic T"
```
```  2536       and "T homeomorphic U"
```
```  2537     shows "S homeomorphic U"
```
```  2538   using assms
```
```  2539   unfolding homeomorphic_def
```
```  2540 by (metis homeomorphism_compose)
```
```  2541
```
```  2542 lemma homeomorphic_minimal:
```
```  2543   "s homeomorphic t \<longleftrightarrow>
```
```  2544     (\<exists>f g. (\<forall>x\<in>s. f(x) \<in> t \<and> (g(f(x)) = x)) \<and>
```
```  2545            (\<forall>y\<in>t. g(y) \<in> s \<and> (f(g(y)) = y)) \<and>
```
```  2546            continuous_on s f \<and> continuous_on t g)"
```
```  2547    (is "?lhs = ?rhs")
```
```  2548 proof
```
```  2549   assume ?lhs
```
```  2550   then show ?rhs
```
```  2551     by (fastforce simp: homeomorphic_def homeomorphism_def)
```
```  2552 next
```
```  2553   assume ?rhs
```
```  2554   then show ?lhs
```
```  2555     apply clarify
```
```  2556     unfolding homeomorphic_def homeomorphism_def
```
```  2557     by (metis equalityI image_subset_iff subsetI)
```
```  2558  qed
```
```  2559
```
```  2560 lemma homeomorphicI [intro?]:
```
```  2561    "\<lbrakk>f ` S = T; g ` T = S;
```
```  2562      continuous_on S f; continuous_on T g;
```
```  2563      \<And>x. x \<in> S \<Longrightarrow> g(f(x)) = x;
```
```  2564      \<And>y. y \<in> T \<Longrightarrow> f(g(y)) = y\<rbrakk> \<Longrightarrow> S homeomorphic T"
```
```  2565 unfolding homeomorphic_def homeomorphism_def by metis
```
```  2566
```
```  2567 lemma homeomorphism_of_subsets:
```
```  2568    "\<lbrakk>homeomorphism S T f g; S' \<subseteq> S; T'' \<subseteq> T; f ` S' = T'\<rbrakk>
```
```  2569     \<Longrightarrow> homeomorphism S' T' f g"
```
```  2570 apply (auto simp: homeomorphism_def elim!: continuous_on_subset)
```
```  2571 by (metis subsetD imageI)
```
```  2572
```
```  2573 lemma homeomorphism_apply1: "\<lbrakk>homeomorphism S T f g; x \<in> S\<rbrakk> \<Longrightarrow> g(f x) = x"
```
```  2574   by (simp add: homeomorphism_def)
```
```  2575
```
```  2576 lemma homeomorphism_apply2: "\<lbrakk>homeomorphism S T f g; x \<in> T\<rbrakk> \<Longrightarrow> f(g x) = x"
```
```  2577   by (simp add: homeomorphism_def)
```
```  2578
```
```  2579 lemma homeomorphism_image1: "homeomorphism S T f g \<Longrightarrow> f ` S = T"
```
```  2580   by (simp add: homeomorphism_def)
```
```  2581
```
```  2582 lemma homeomorphism_image2: "homeomorphism S T f g \<Longrightarrow> g ` T = S"
```
```  2583   by (simp add: homeomorphism_def)
```
```  2584
```
```  2585 lemma homeomorphism_cont1: "homeomorphism S T f g \<Longrightarrow> continuous_on S f"
```
```  2586   by (simp add: homeomorphism_def)
```
```  2587
```
```  2588 lemma homeomorphism_cont2: "homeomorphism S T f g \<Longrightarrow> continuous_on T g"
```
```  2589   by (simp add: homeomorphism_def)
```
```  2590
```
```  2591 lemma continuous_on_no_limpt:
```
```  2592    "(\<And>x. \<not> x islimpt S) \<Longrightarrow> continuous_on S f"
```
```  2593   unfolding continuous_on_def
```
```  2594   by (metis UNIV_I empty_iff eventually_at_topological islimptE open_UNIV tendsto_def trivial_limit_within)
```
```  2595
```
```  2596 lemma continuous_on_finite:
```
```  2597   fixes S :: "'a::t1_space set"
```
```  2598   shows "finite S \<Longrightarrow> continuous_on S f"
```
```  2599 by (metis continuous_on_no_limpt islimpt_finite)
```
```  2600
```
```  2601 lemma homeomorphic_finite:
```
```  2602   fixes S :: "'a::t1_space set" and T :: "'b::t1_space set"
```
```  2603   assumes "finite T"
```
```  2604   shows "S homeomorphic T \<longleftrightarrow> finite S \<and> finite T \<and> card S = card T" (is "?lhs = ?rhs")
```
```  2605 proof
```
```  2606   assume "S homeomorphic T"
```
```  2607   with assms show ?rhs
```
```  2608     apply (auto simp: homeomorphic_def homeomorphism_def)
```
```  2609      apply (metis finite_imageI)
```
```  2610     by (metis card_image_le finite_imageI le_antisym)
```
```  2611 next
```
```  2612   assume R: ?rhs
```
```  2613   with finite_same_card_bij obtain h where "bij_betw h S T"
```
```  2614     by auto
```
```  2615   with R show ?lhs
```
```  2616     apply (auto simp: homeomorphic_def homeomorphism_def continuous_on_finite)
```
```  2617     apply (rule_tac x=h in exI)
```
```  2618     apply (rule_tac x="inv_into S h" in exI)
```
```  2619     apply (auto simp:  bij_betw_inv_into_left bij_betw_inv_into_right bij_betw_imp_surj_on inv_into_into bij_betwE)
```
```  2620     apply (metis bij_betw_def bij_betw_inv_into)
```
```  2621     done
```
```  2622 qed
```
```  2623
```
```  2624 text \<open>Relatively weak hypotheses if a set is compact.\<close>
```
```  2625
```
```  2626 lemma homeomorphism_compact:
```
```  2627   fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
```
```  2628   assumes "compact s" "continuous_on s f"  "f ` s = t"  "inj_on f s"
```
```  2629   shows "\<exists>g. homeomorphism s t f g"
```
```  2630 proof -
```
```  2631   define g where "g x = (SOME y. y\<in>s \<and> f y = x)" for x
```
```  2632   have g: "\<forall>x\<in>s. g (f x) = x"
```
```  2633     using assms(3) assms(4)[unfolded inj_on_def] unfolding g_def by auto
```
```  2634   {
```
```  2635     fix y
```
```  2636     assume "y \<in> t"
```
```  2637     then obtain x where x:"f x = y" "x\<in>s"
```
```  2638       using assms(3) by auto
```
```  2639     then have "g (f x) = x" using g by auto
```
```  2640     then have "f (g y) = y" unfolding x(1)[symmetric] by auto
```
```  2641   }
```
```  2642   then have g':"\<forall>x\<in>t. f (g x) = x" by auto
```
```  2643   moreover
```
```  2644   {
```
```  2645     fix x
```
```  2646     have "x\<in>s \<Longrightarrow> x \<in> g ` t"
```
```  2647       using g[THEN bspec[where x=x]]
```
```  2648       unfolding image_iff
```
```  2649       using assms(3)
```
```  2650       by (auto intro!: bexI[where x="f x"])
```
```  2651     moreover
```
```  2652     {
```
```  2653       assume "x\<in>g ` t"
```
```  2654       then obtain y where y:"y\<in>t" "g y = x" by auto
```
```  2655       then obtain x' where x':"x'\<in>s" "f x' = y"
```
```  2656         using assms(3) by auto
```
```  2657       then have "x \<in> s"
```
```  2658         unfolding g_def
```
```  2659         using someI2[of "\<lambda>b. b\<in>s \<and> f b = y" x' "\<lambda>x. x\<in>s"]
```
```  2660         unfolding y(2)[symmetric] and g_def
```
```  2661         by auto
```
```  2662     }
```
```  2663     ultimately have "x\<in>s \<longleftrightarrow> x \<in> g ` t" ..
```
```  2664   }
```
```  2665   then have "g ` t = s" by auto
```
```  2666   ultimately show ?thesis
```
```  2667     unfolding homeomorphism_def homeomorphic_def
```
```  2668     apply (rule_tac x=g in exI)
```
```  2669     using g and assms(3) and continuous_on_inv[OF assms(2,1), of g, unfolded assms(3)] and assms(2)
```
```  2670     apply auto
```
```  2671     done
```
```  2672 qed
```
```  2673
```
```  2674 lemma homeomorphic_compact:
```
```  2675   fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
```
```  2676   shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s \<Longrightarrow> s homeomorphic t"
```
```  2677   unfolding homeomorphic_def by (metis homeomorphism_compact)
```
```  2678
```
```  2679 text\<open>Preservation of topological properties.\<close>
```
```  2680
```
```  2681 lemma homeomorphic_compactness: "s homeomorphic t \<Longrightarrow> (compact s \<longleftrightarrow> compact t)"
```
```  2682   unfolding homeomorphic_def homeomorphism_def
```
```  2683   by (metis compact_continuous_image)
```
```  2684
```
```  2685
```
```  2686 subsection%unimportant \<open>On Linorder Topologies\<close>
```
```  2687
```
```  2688 lemma islimpt_greaterThanLessThan1:
```
```  2689   fixes a b::"'a::{linorder_topology, dense_order}"
```
```  2690   assumes "a < b"
```
```  2691   shows  "a islimpt {a<..<b}"
```
```  2692 proof (rule islimptI)
```
```  2693   fix T
```
```  2694   assume "open T" "a \<in> T"
```
```  2695   from open_right[OF this \<open>a < b\<close>]
```
```  2696   obtain c where c: "a < c" "{a..<c} \<subseteq> T" by auto
```
```  2697   with assms dense[of a "min c b"]
```
```  2698   show "\<exists>y\<in>{a<..<b}. y \<in> T \<and> y \<noteq> a"
```
```  2699     by (metis atLeastLessThan_iff greaterThanLessThan_iff min_less_iff_conj
```
```  2700       not_le order.strict_implies_order subset_eq)
```
```  2701 qed
```
```  2702
```
```  2703 lemma islimpt_greaterThanLessThan2:
```
```  2704   fixes a b::"'a::{linorder_topology, dense_order}"
```
```  2705   assumes "a < b"
```
```  2706   shows  "b islimpt {a<..<b}"
```
```  2707 proof (rule islimptI)
```
```  2708   fix T
```
```  2709   assume "open T" "b \<in> T"
```
```  2710   from open_left[OF this \<open>a < b\<close>]
```
```  2711   obtain c where c: "c < b" "{c<..b} \<subseteq> T" by auto
```
```  2712   with assms dense[of "max a c" b]
```
```  2713   show "\<exists>y\<in>{a<..<b}. y \<in> T \<and> y \<noteq> b"
```
```  2714     by (metis greaterThanAtMost_iff greaterThanLessThan_iff max_less_iff_conj
```
```  2715       not_le order.strict_implies_order subset_eq)
```
```  2716 qed
```
```  2717
```
```  2718 lemma closure_greaterThanLessThan[simp]:
```
```  2719   fixes a b::"'a::{linorder_topology, dense_order}"
```
```  2720   shows "a < b \<Longrightarrow> closure {a <..< b} = {a .. b}" (is "_ \<Longrightarrow> ?l = ?r")
```
```  2721 proof
```
```  2722   have "?l \<subseteq> closure ?r"
```
```  2723     by (rule closure_mono) auto
```
```  2724   thus "closure {a<..<b} \<subseteq> {a..b}" by simp
```
```  2725 qed (auto simp: closure_def order.order_iff_strict islimpt_greaterThanLessThan1
```
```  2726   islimpt_greaterThanLessThan2)
```
```  2727
```
```  2728 lemma closure_greaterThan[simp]:
```
```  2729   fixes a b::"'a::{no_top, linorder_topology, dense_order}"
```
```  2730   shows "closure {a<..} = {a..}"
```
```  2731 proof -
```
```  2732   from gt_ex obtain b where "a < b" by auto
```
```  2733   hence "{a<..} = {a<..<b} \<union> {b..}" by auto
```
```  2734   also have "closure \<dots> = {a..}" using \<open>a < b\<close> unfolding closure_Un
```
```  2735     by auto
```
```  2736   finally show ?thesis .
```
```  2737 qed
```
```  2738
```
```  2739 lemma closure_lessThan[simp]:
```
```  2740   fixes b::"'a::{no_bot, linorder_topology, dense_order}"
```
```  2741   shows "closure {..<b} = {..b}"
```
```  2742 proof -
```
```  2743   from lt_ex obtain a where "a < b" by auto
```
```  2744   hence "{..<b} = {a<..<b} \<union> {..a}" by auto
```
```  2745   also have "closure \<dots> = {..b}" using \<open>a < b\<close> unfolding closure_Un
```
```  2746     by auto
```
```  2747   finally show ?thesis .
```
```  2748 qed
```
```  2749
```
```  2750 lemma closure_atLeastLessThan[simp]:
```
```  2751   fixes a b::"'a::{linorder_topology, dense_order}"
```
```  2752   assumes "a < b"
```
```  2753   shows "closure {a ..< b} = {a .. b}"
```
```  2754 proof -
```
```  2755   from assms have "{a ..< b} = {a} \<union> {a <..< b}" by auto
```
```  2756   also have "closure \<dots> = {a .. b}" unfolding closure_Un
```
```  2757     by (auto simp: assms less_imp_le)
```
```  2758   finally show ?thesis .
```
```  2759 qed
```
```  2760
```
```  2761 lemma closure_greaterThanAtMost[simp]:
```
```  2762   fixes a b::"'a::{linorder_topology, dense_order}"
```
```  2763   assumes "a < b"
```
```  2764   shows "closure {a <.. b} = {a .. b}"
```
```  2765 proof -
```
```  2766   from assms have "{a <.. b} = {b} \<union> {a <..< b}" by auto
```
```  2767   also have "closure \<dots> = {a .. b}" unfolding closure_Un
```
```  2768     by (auto simp: assms less_imp_le)
```
```  2769   finally show ?thesis .
```
```  2770 qed
```
```  2771
```
```  2772
```
`  2773 end`