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;
immler@69516
     1
(*  Author:     L C Paulson, University of Cambridge
immler@69516
     2
    Author:     Amine Chaieb, University of Cambridge
immler@69516
     3
    Author:     Robert Himmelmann, TU Muenchen
immler@69516
     4
    Author:     Brian Huffman, Portland State University
immler@69516
     5
*)
immler@69516
     6
immler@69676
     7
chapter \<open>Topology\<close>
immler@69516
     8
immler@69516
     9
theory Elementary_Topology
immler@69516
    10
imports
immler@69516
    11
  "HOL-Library.Set_Idioms"
immler@69615
    12
  "HOL-Library.Disjoint_Sets"
immler@69516
    13
  Product_Vector
immler@69516
    14
begin
immler@69516
    15
immler@69516
    16
immler@69676
    17
section \<open>Elementary Topology\<close>
immler@69676
    18
immler@69544
    19
subsection \<open>TODO: move?\<close>
immler@69516
    20
immler@69544
    21
lemma open_subopen: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S)"
immler@69544
    22
  using openI by auto
immler@69516
    23
immler@69516
    24
immler@69613
    25
subsubsection%unimportant \<open>Archimedean properties and useful consequences\<close>
immler@69613
    26
immler@69613
    27
text\<open>Bernoulli's inequality\<close>
immler@69613
    28
proposition Bernoulli_inequality:
immler@69613
    29
  fixes x :: real
immler@69613
    30
  assumes "-1 \<le> x"
immler@69613
    31
    shows "1 + n * x \<le> (1 + x) ^ n"
immler@69613
    32
proof (induct n)
immler@69613
    33
  case 0
immler@69613
    34
  then show ?case by simp
immler@69613
    35
next
immler@69613
    36
  case (Suc n)
immler@69613
    37
  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
immler@69613
    38
    by (simp add: algebra_simps)
immler@69613
    39
  also have "... = (1 + x) * (1 + n*x)"
immler@69613
    40
    by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
immler@69613
    41
  also have "... \<le> (1 + x) ^ Suc n"
immler@69613
    42
    using Suc.hyps assms mult_left_mono by fastforce
immler@69613
    43
  finally show ?case .
immler@69613
    44
qed
immler@69613
    45
immler@69613
    46
corollary Bernoulli_inequality_even:
immler@69613
    47
  fixes x :: real
immler@69613
    48
  assumes "even n"
immler@69613
    49
    shows "1 + n * x \<le> (1 + x) ^ n"
immler@69613
    50
proof (cases "-1 \<le> x \<or> n=0")
immler@69613
    51
  case True
immler@69613
    52
  then show ?thesis
immler@69613
    53
    by (auto simp: Bernoulli_inequality)
immler@69613
    54
next
immler@69613
    55
  case False
immler@69613
    56
  then have "real n \<ge> 1"
immler@69613
    57
    by simp
immler@69613
    58
  with False have "n * x \<le> -1"
immler@69613
    59
    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
immler@69613
    60
  then have "1 + n * x \<le> 0"
immler@69613
    61
    by auto
immler@69613
    62
  also have "... \<le> (1 + x) ^ n"
immler@69613
    63
    using assms
immler@69613
    64
    using zero_le_even_power by blast
immler@69613
    65
  finally show ?thesis .
immler@69613
    66
qed
immler@69613
    67
immler@69613
    68
corollary real_arch_pow:
immler@69613
    69
  fixes x :: real
immler@69613
    70
  assumes x: "1 < x"
immler@69613
    71
  shows "\<exists>n. y < x^n"
immler@69613
    72
proof -
immler@69613
    73
  from x have x0: "x - 1 > 0"
immler@69613
    74
    by arith
immler@69613
    75
  from reals_Archimedean3[OF x0, rule_format, of y]
immler@69613
    76
  obtain n :: nat where n: "y < real n * (x - 1)" by metis
immler@69613
    77
  from x0 have x00: "x- 1 \<ge> -1" by arith
immler@69613
    78
  from Bernoulli_inequality[OF x00, of n] n
immler@69613
    79
  have "y < x^n" by auto
immler@69613
    80
  then show ?thesis by metis
immler@69613
    81
qed
immler@69613
    82
immler@69613
    83
corollary real_arch_pow_inv:
immler@69613
    84
  fixes x y :: real
immler@69613
    85
  assumes y: "y > 0"
immler@69613
    86
    and x1: "x < 1"
immler@69613
    87
  shows "\<exists>n. x^n < y"
immler@69613
    88
proof (cases "x > 0")
immler@69613
    89
  case True
immler@69613
    90
  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
immler@69613
    91
  from real_arch_pow[OF ix, of "1/y"]
immler@69613
    92
  obtain n where n: "1/y < (1/x)^n" by blast
immler@69613
    93
  then show ?thesis using y \<open>x > 0\<close>
immler@69613
    94
    by (auto simp add: field_simps)
immler@69613
    95
next
immler@69613
    96
  case False
immler@69613
    97
  with y x1 show ?thesis
immler@69613
    98
    by (metis less_le_trans not_less power_one_right)
immler@69613
    99
qed
immler@69613
   100
immler@69613
   101
lemma forall_pos_mono:
immler@69613
   102
  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
immler@69613
   103
    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
immler@69613
   104
  by (metis real_arch_inverse)
immler@69613
   105
immler@69613
   106
lemma forall_pos_mono_1:
immler@69613
   107
  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
immler@69613
   108
    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
immler@69613
   109
  apply (rule forall_pos_mono)
immler@69613
   110
  apply auto
immler@69613
   111
  apply (metis Suc_pred of_nat_Suc)
immler@69613
   112
  done
immler@69613
   113
immler@69613
   114
subsubsection%unimportant \<open>Affine transformations of intervals\<close>
immler@69613
   115
immler@69613
   116
lemma real_affinity_le: "0 < m \<Longrightarrow> m * x + c \<le> y \<longleftrightarrow> x \<le> inverse m * y + - (c / m)"
immler@69613
   117
  for m :: "'a::linordered_field"
immler@69613
   118
  by (simp add: field_simps)
immler@69613
   119
immler@69613
   120
lemma real_le_affinity: "0 < m \<Longrightarrow> y \<le> m * x + c \<longleftrightarrow> inverse m * y + - (c / m) \<le> x"
immler@69613
   121
  for m :: "'a::linordered_field"
immler@69613
   122
  by (simp add: field_simps)
immler@69613
   123
immler@69613
   124
lemma real_affinity_lt: "0 < m \<Longrightarrow> m * x + c < y \<longleftrightarrow> x < inverse m * y + - (c / m)"
immler@69613
   125
  for m :: "'a::linordered_field"
immler@69613
   126
  by (simp add: field_simps)
immler@69613
   127
immler@69613
   128
lemma real_lt_affinity: "0 < m \<Longrightarrow> y < m * x + c \<longleftrightarrow> inverse m * y + - (c / m) < x"
immler@69613
   129
  for m :: "'a::linordered_field"
immler@69613
   130
  by (simp add: field_simps)
immler@69613
   131
immler@69613
   132
lemma real_affinity_eq: "m \<noteq> 0 \<Longrightarrow> m * x + c = y \<longleftrightarrow> x = inverse m * y + - (c / m)"
immler@69613
   133
  for m :: "'a::linordered_field"
immler@69613
   134
  by (simp add: field_simps)
immler@69613
   135
immler@69613
   136
lemma real_eq_affinity: "m \<noteq> 0 \<Longrightarrow> y = m * x + c  \<longleftrightarrow> inverse m * y + - (c / m) = x"
immler@69613
   137
  for m :: "'a::linordered_field"
immler@69613
   138
  by (simp add: field_simps)
immler@69613
   139
immler@69613
   140
immler@69613
   141
immler@69516
   142
subsection \<open>Topological Basis\<close>
immler@69516
   143
immler@69516
   144
context topological_space
immler@69516
   145
begin
immler@69516
   146
immler@69516
   147
definition%important "topological_basis B \<longleftrightarrow>
immler@69516
   148
  (\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
immler@69516
   149
immler@69516
   150
lemma topological_basis:
immler@69516
   151
  "topological_basis B \<longleftrightarrow> (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
immler@69516
   152
  unfolding topological_basis_def
immler@69516
   153
  apply safe
immler@69516
   154
     apply fastforce
immler@69516
   155
    apply fastforce
immler@69516
   156
   apply (erule_tac x=x in allE, simp)
immler@69516
   157
   apply (rule_tac x="{x}" in exI, auto)
immler@69516
   158
  done
immler@69516
   159
immler@69516
   160
lemma topological_basis_iff:
immler@69516
   161
  assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
immler@69516
   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'))"
immler@69516
   163
    (is "_ \<longleftrightarrow> ?rhs")
immler@69516
   164
proof safe
immler@69516
   165
  fix O' and x::'a
immler@69516
   166
  assume H: "topological_basis B" "open O'" "x \<in> O'"
immler@69516
   167
  then have "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def)
immler@69516
   168
  then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto
immler@69516
   169
  then show "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto
immler@69516
   170
next
immler@69516
   171
  assume H: ?rhs
immler@69516
   172
  show "topological_basis B"
immler@69516
   173
    using assms unfolding topological_basis_def
immler@69516
   174
  proof safe
immler@69516
   175
    fix O' :: "'a set"
immler@69516
   176
    assume "open O'"
immler@69516
   177
    with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'"
immler@69516
   178
      by (force intro: bchoice simp: Bex_def)
immler@69516
   179
    then show "\<exists>B'\<subseteq>B. \<Union>B' = O'"
immler@69516
   180
      by (auto intro: exI[where x="{f x |x. x \<in> O'}"])
immler@69516
   181
  qed
immler@69516
   182
qed
immler@69516
   183
immler@69516
   184
lemma topological_basisI:
immler@69516
   185
  assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
immler@69516
   186
    and "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'"
immler@69516
   187
  shows "topological_basis B"
immler@69516
   188
  using assms by (subst topological_basis_iff) auto
immler@69516
   189
immler@69516
   190
lemma topological_basisE:
immler@69516
   191
  fixes O'
immler@69516
   192
  assumes "topological_basis B"
immler@69516
   193
    and "open O'"
immler@69516
   194
    and "x \<in> O'"
immler@69516
   195
  obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'"
immler@69516
   196
proof atomize_elim
immler@69516
   197
  from assms have "\<And>B'. B'\<in>B \<Longrightarrow> open B'"
immler@69516
   198
    by (simp add: topological_basis_def)
immler@69516
   199
  with topological_basis_iff assms
immler@69516
   200
  show  "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'"
immler@69516
   201
    using assms by (simp add: Bex_def)
immler@69516
   202
qed
immler@69516
   203
immler@69516
   204
lemma topological_basis_open:
immler@69516
   205
  assumes "topological_basis B"
immler@69516
   206
    and "X \<in> B"
immler@69516
   207
  shows "open X"
immler@69516
   208
  using assms by (simp add: topological_basis_def)
immler@69516
   209
immler@69516
   210
lemma topological_basis_imp_subbasis:
immler@69516
   211
  assumes B: "topological_basis B"
immler@69516
   212
  shows "open = generate_topology B"
immler@69516
   213
proof (intro ext iffI)
immler@69516
   214
  fix S :: "'a set"
immler@69516
   215
  assume "open S"
immler@69516
   216
  with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'"
immler@69516
   217
    unfolding topological_basis_def by blast
immler@69516
   218
  then show "generate_topology B S"
immler@69516
   219
    by (auto intro: generate_topology.intros dest: topological_basis_open)
immler@69516
   220
next
immler@69516
   221
  fix S :: "'a set"
immler@69516
   222
  assume "generate_topology B S"
immler@69516
   223
  then show "open S"
immler@69516
   224
    by induct (auto dest: topological_basis_open[OF B])
immler@69516
   225
qed
immler@69516
   226
immler@69516
   227
lemma basis_dense:
immler@69516
   228
  fixes B :: "'a set set"
immler@69516
   229
    and f :: "'a set \<Rightarrow> 'a"
immler@69516
   230
  assumes "topological_basis B"
immler@69516
   231
    and choosefrom_basis: "\<And>B'. B' \<noteq> {} \<Longrightarrow> f B' \<in> B'"
immler@69516
   232
  shows "\<forall>X. open X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>B' \<in> B. f B' \<in> X)"
immler@69516
   233
proof (intro allI impI)
immler@69516
   234
  fix X :: "'a set"
immler@69516
   235
  assume "open X" and "X \<noteq> {}"
immler@69516
   236
  from topological_basisE[OF \<open>topological_basis B\<close> \<open>open X\<close> choosefrom_basis[OF \<open>X \<noteq> {}\<close>]]
immler@69516
   237
  obtain B' where "B' \<in> B" "f X \<in> B'" "B' \<subseteq> X" .
immler@69516
   238
  then show "\<exists>B'\<in>B. f B' \<in> X"
immler@69516
   239
    by (auto intro!: choosefrom_basis)
immler@69516
   240
qed
immler@69516
   241
immler@69516
   242
end
immler@69516
   243
immler@69516
   244
lemma topological_basis_prod:
immler@69516
   245
  assumes A: "topological_basis A"
immler@69516
   246
    and B: "topological_basis B"
immler@69516
   247
  shows "topological_basis ((\<lambda>(a, b). a \<times> b) ` (A \<times> B))"
immler@69516
   248
  unfolding topological_basis_def
immler@69516
   249
proof (safe, simp_all del: ex_simps add: subset_image_iff ex_simps(1)[symmetric])
immler@69516
   250
  fix S :: "('a \<times> 'b) set"
immler@69516
   251
  assume "open S"
immler@69516
   252
  then show "\<exists>X\<subseteq>A \<times> B. (\<Union>(a,b)\<in>X. a \<times> b) = S"
immler@69516
   253
  proof (safe intro!: exI[of _ "{x\<in>A \<times> B. fst x \<times> snd x \<subseteq> S}"])
immler@69516
   254
    fix x y
immler@69516
   255
    assume "(x, y) \<in> S"
immler@69516
   256
    from open_prod_elim[OF \<open>open S\<close> this]
immler@69516
   257
    obtain a b where a: "open a""x \<in> a" and b: "open b" "y \<in> b" and "a \<times> b \<subseteq> S"
immler@69516
   258
      by (metis mem_Sigma_iff)
immler@69516
   259
    moreover
immler@69516
   260
    from A a obtain A0 where "A0 \<in> A" "x \<in> A0" "A0 \<subseteq> a"
immler@69516
   261
      by (rule topological_basisE)
immler@69516
   262
    moreover
immler@69516
   263
    from B b obtain B0 where "B0 \<in> B" "y \<in> B0" "B0 \<subseteq> b"
immler@69516
   264
      by (rule topological_basisE)
immler@69516
   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)"
immler@69516
   266
      by (intro UN_I[of "(A0, B0)"]) auto
immler@69516
   267
  qed auto
immler@69516
   268
qed (metis A B topological_basis_open open_Times)
immler@69516
   269
immler@69516
   270
immler@69516
   271
subsection \<open>Countable Basis\<close>
immler@69516
   272
immler@69748
   273
locale%important countable_basis = topological_space p for p::"'a set \<Rightarrow> bool" +
immler@69748
   274
  fixes B :: "'a set set"
immler@69516
   275
  assumes is_basis: "topological_basis B"
immler@69516
   276
    and countable_basis: "countable B"
immler@69516
   277
begin
immler@69516
   278
immler@69516
   279
lemma open_countable_basis_ex:
immler@69748
   280
  assumes "p X"
immler@69516
   281
  shows "\<exists>B' \<subseteq> B. X = \<Union>B'"
immler@69516
   282
  using assms countable_basis is_basis
immler@69516
   283
  unfolding topological_basis_def by blast
immler@69516
   284
immler@69516
   285
lemma open_countable_basisE:
immler@69748
   286
  assumes "p X"
immler@69516
   287
  obtains B' where "B' \<subseteq> B" "X = \<Union>B'"
immler@69516
   288
  using assms open_countable_basis_ex
immler@69516
   289
  by atomize_elim simp
immler@69516
   290
immler@69516
   291
lemma countable_dense_exists:
immler@69748
   292
  "\<exists>D::'a set. countable D \<and> (\<forall>X. p X \<longrightarrow> X \<noteq> {} \<longrightarrow> (\<exists>d \<in> D. d \<in> X))"
immler@69516
   293
proof -
immler@69516
   294
  let ?f = "(\<lambda>B'. SOME x. x \<in> B')"
immler@69516
   295
  have "countable (?f ` B)" using countable_basis by simp
immler@69516
   296
  with basis_dense[OF is_basis, of ?f] show ?thesis
immler@69516
   297
    by (intro exI[where x="?f ` B"]) (metis (mono_tags) all_not_in_conv imageI someI)
immler@69516
   298
qed
immler@69516
   299
immler@69516
   300
lemma countable_dense_setE:
immler@69516
   301
  obtains D :: "'a set"
immler@69748
   302
  where "countable D" "\<And>X. p X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d \<in> D. d \<in> X"
immler@69516
   303
  using countable_dense_exists by blast
immler@69516
   304
immler@69516
   305
end
immler@69516
   306
immler@69748
   307
lemma countable_basis_openI: "countable_basis open B"
immler@69748
   308
  if "countable B" "topological_basis B"
immler@69748
   309
  using that
immler@69748
   310
  by unfold_locales
immler@69748
   311
    (simp_all add: topological_basis topological_space.topological_basis topological_space_axioms)
immler@69748
   312
immler@69516
   313
lemma (in first_countable_topology) first_countable_basisE:
immler@69516
   314
  fixes x :: 'a
immler@69516
   315
  obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
immler@69516
   316
    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)"
immler@69516
   317
proof -
immler@69516
   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))"
immler@69516
   319
    using first_countable_basis[of x] by metis
immler@69516
   320
  show thesis
immler@69516
   321
  proof 
immler@69516
   322
    show "countable (range \<A>)"
immler@69516
   323
      by simp
immler@69516
   324
  qed (use \<A> in auto)
immler@69516
   325
qed
immler@69516
   326
immler@69516
   327
lemma (in first_countable_topology) first_countable_basis_Int_stableE:
immler@69516
   328
  obtains \<A> where "countable \<A>" "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
immler@69516
   329
    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> (\<exists>A\<in>\<A>. A \<subseteq> S)"
immler@69516
   330
    "\<And>A B. A \<in> \<A> \<Longrightarrow> B \<in> \<A> \<Longrightarrow> A \<inter> B \<in> \<A>"
immler@69516
   331
proof atomize_elim
immler@69516
   332
  obtain \<B> where \<B>:
immler@69516
   333
    "countable \<B>"
immler@69516
   334
    "\<And>B. B \<in> \<B> \<Longrightarrow> x \<in> B"
immler@69516
   335
    "\<And>B. B \<in> \<B> \<Longrightarrow> open B"
immler@69516
   336
    "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>B\<in>\<B>. B \<subseteq> S"
immler@69516
   337
    by (rule first_countable_basisE) blast
immler@69516
   338
  define \<A> where [abs_def]:
immler@69516
   339
    "\<A> = (\<lambda>N. \<Inter>((\<lambda>n. from_nat_into \<B> n) ` N)) ` (Collect finite::nat set set)"
immler@69516
   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>
immler@69516
   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>)"
immler@69516
   342
  proof (safe intro!: exI[where x=\<A>])
immler@69516
   343
    show "countable \<A>"
immler@69516
   344
      unfolding \<A>_def by (intro countable_image countable_Collect_finite)
immler@69516
   345
    fix A
immler@69516
   346
    assume "A \<in> \<A>"
immler@69516
   347
    then show "x \<in> A" "open A"
immler@69516
   348
      using \<B>(4)[OF open_UNIV] by (auto simp: \<A>_def intro: \<B> from_nat_into)
immler@69516
   349
  next
immler@69516
   350
    let ?int = "\<lambda>N. \<Inter>(from_nat_into \<B> ` N)"
immler@69516
   351
    fix A B
immler@69516
   352
    assume "A \<in> \<A>" "B \<in> \<A>"
immler@69516
   353
    then obtain N M where "A = ?int N" "B = ?int M" "finite (N \<union> M)"
immler@69516
   354
      by (auto simp: \<A>_def)
immler@69516
   355
    then show "A \<inter> B \<in> \<A>"
immler@69516
   356
      by (auto simp: \<A>_def intro!: image_eqI[where x="N \<union> M"])
immler@69516
   357
  next
immler@69516
   358
    fix S
immler@69516
   359
    assume "open S" "x \<in> S"
immler@69516
   360
    then obtain a where a: "a\<in>\<B>" "a \<subseteq> S" using \<B> by blast
immler@69516
   361
    then show "\<exists>a\<in>\<A>. a \<subseteq> S" using a \<B>
immler@69516
   362
      by (intro bexI[where x=a]) (auto simp: \<A>_def intro: image_eqI[where x="{to_nat_on \<B> a}"])
immler@69516
   363
  qed
immler@69516
   364
qed
immler@69516
   365
immler@69516
   366
lemma (in topological_space) first_countableI:
immler@69516
   367
  assumes "countable \<A>"
immler@69516
   368
    and 1: "\<And>A. A \<in> \<A> \<Longrightarrow> x \<in> A" "\<And>A. A \<in> \<A> \<Longrightarrow> open A"
immler@69516
   369
    and 2: "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> \<exists>A\<in>\<A>. A \<subseteq> S"
immler@69516
   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))"
immler@69516
   371
proof (safe intro!: exI[of _ "from_nat_into \<A>"])
immler@69516
   372
  fix i
immler@69516
   373
  have "\<A> \<noteq> {}" using 2[of UNIV] by auto
immler@69516
   374
  show "x \<in> from_nat_into \<A> i" "open (from_nat_into \<A> i)"
immler@69516
   375
    using range_from_nat_into_subset[OF \<open>\<A> \<noteq> {}\<close>] 1 by auto
immler@69516
   376
next
immler@69516
   377
  fix S
immler@69516
   378
  assume "open S" "x\<in>S" from 2[OF this]
immler@69516
   379
  show "\<exists>i. from_nat_into \<A> i \<subseteq> S"
immler@69516
   380
    using subset_range_from_nat_into[OF \<open>countable \<A>\<close>] by auto
immler@69516
   381
qed
immler@69516
   382
immler@69516
   383
instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
immler@69516
   384
proof
immler@69516
   385
  fix x :: "'a \<times> 'b"
immler@69516
   386
  obtain \<A> where \<A>:
immler@69516
   387
      "countable \<A>"
immler@69516
   388
      "\<And>a. a \<in> \<A> \<Longrightarrow> fst x \<in> a"
immler@69516
   389
      "\<And>a. a \<in> \<A> \<Longrightarrow> open a"
immler@69516
   390
      "\<And>S. open S \<Longrightarrow> fst x \<in> S \<Longrightarrow> \<exists>a\<in>\<A>. a \<subseteq> S"
immler@69516
   391
    by (rule first_countable_basisE[of "fst x"]) blast
immler@69516
   392
  obtain B where B:
immler@69516
   393
      "countable B"
immler@69516
   394
      "\<And>a. a \<in> B \<Longrightarrow> snd x \<in> a"
immler@69516
   395
      "\<And>a. a \<in> B \<Longrightarrow> open a"
immler@69516
   396
      "\<And>S. open S \<Longrightarrow> snd x \<in> S \<Longrightarrow> \<exists>a\<in>B. a \<subseteq> S"
immler@69516
   397
    by (rule first_countable_basisE[of "snd x"]) blast
immler@69516
   398
  show "\<exists>\<A>::nat \<Rightarrow> ('a \<times> 'b) set.
immler@69516
   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))"
immler@69516
   400
  proof (rule first_countableI[of "(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B)"], safe)
immler@69516
   401
    fix a b
immler@69516
   402
    assume x: "a \<in> \<A>" "b \<in> B"
immler@69516
   403
    show "x \<in> a \<times> b" 
immler@69516
   404
      by (simp add: \<A>(2) B(2) mem_Times_iff x)
immler@69516
   405
    show "open (a \<times> b)"
immler@69516
   406
      by (simp add: \<A>(3) B(3) open_Times x)
immler@69516
   407
  next
immler@69516
   408
    fix S
immler@69516
   409
    assume "open S" "x \<in> S"
immler@69516
   410
    then obtain a' b' where a'b': "open a'" "open b'" "x \<in> a' \<times> b'" "a' \<times> b' \<subseteq> S"
immler@69516
   411
      by (rule open_prod_elim)
immler@69516
   412
    moreover
immler@69516
   413
    from a'b' \<A>(4)[of a'] B(4)[of b']
immler@69516
   414
    obtain a b where "a \<in> \<A>" "a \<subseteq> a'" "b \<in> B" "b \<subseteq> b'"
immler@69516
   415
      by auto
immler@69516
   416
    ultimately
immler@69516
   417
    show "\<exists>a\<in>(\<lambda>(a, b). a \<times> b) ` (\<A> \<times> B). a \<subseteq> S"
immler@69516
   418
      by (auto intro!: bexI[of _ "a \<times> b"] bexI[of _ a] bexI[of _ b])
immler@69516
   419
  qed (simp add: \<A> B)
immler@69516
   420
qed
immler@69516
   421
immler@69516
   422
class second_countable_topology = topological_space +
immler@69516
   423
  assumes ex_countable_subbasis:
immler@69748
   424
    "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
immler@69516
   425
begin
immler@69516
   426
immler@69516
   427
lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B"
immler@69516
   428
proof -
immler@69516
   429
  from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B"
immler@69516
   430
    by blast
immler@69516
   431
  let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }"
immler@69516
   432
immler@69516
   433
  show ?thesis
immler@69516
   434
  proof (intro exI conjI)
immler@69516
   435
    show "countable ?B"
immler@69516
   436
      by (intro countable_image countable_Collect_finite_subset B)
immler@69516
   437
    {
immler@69516
   438
      fix S
immler@69516
   439
      assume "open S"
immler@69516
   440
      then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S"
immler@69516
   441
        unfolding B
immler@69516
   442
      proof induct
immler@69516
   443
        case UNIV
immler@69516
   444
        show ?case by (intro exI[of _ "{{}}"]) simp
immler@69516
   445
      next
immler@69516
   446
        case (Int a b)
immler@69516
   447
        then obtain x y where x: "a = \<Union>(Inter ` x)" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
immler@69516
   448
          and y: "b = \<Union>(Inter ` y)" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B"
immler@69516
   449
          by blast
immler@69516
   450
        show ?case
immler@69516
   451
          unfolding x y Int_UN_distrib2
immler@69516
   452
          by (intro exI[of _ "{i \<union> j| i j.  i \<in> x \<and> j \<in> y}"]) (auto dest: x(2) y(2))
immler@69516
   453
      next
immler@69516
   454
        case (UN K)
immler@69516
   455
        then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. \<Union> (Inter ` B') = k" by auto
immler@69516
   456
        then obtain k where
immler@69516
   457
            "\<forall>ka\<in>K. k ka \<subseteq> {b. finite b \<and> b \<subseteq> B} \<and> \<Union>(Inter ` (k ka)) = ka"
immler@69516
   458
          unfolding bchoice_iff ..
immler@69516
   459
        then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. \<Union> (Inter ` B') = \<Union>K"
immler@69516
   460
          by (intro exI[of _ "\<Union>(k ` K)"]) auto
immler@69516
   461
      next
immler@69516
   462
        case (Basis S)
immler@69516
   463
        then show ?case
immler@69516
   464
          by (intro exI[of _ "{{S}}"]) auto
immler@69516
   465
      qed
immler@69516
   466
      then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)"
immler@69516
   467
        unfolding subset_image_iff by blast }
immler@69516
   468
    then show "topological_basis ?B"
immler@69748
   469
      unfolding topological_basis_def
immler@69748
   470
      by (safe intro!: open_Inter)
immler@69516
   471
         (simp_all add: B generate_topology.Basis subset_eq)
immler@69516
   472
  qed
immler@69516
   473
qed
immler@69516
   474
immler@69615
   475
immler@69516
   476
end
immler@69516
   477
immler@69615
   478
lemma univ_second_countable:
immler@69615
   479
  obtains \<B> :: "'a::second_countable_topology set set"
immler@69615
   480
  where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
immler@69615
   481
       "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
immler@69615
   482
by (metis ex_countable_basis topological_basis_def)
immler@69615
   483
immler@69615
   484
proposition Lindelof:
immler@69615
   485
  fixes \<F> :: "'a::second_countable_topology set set"
immler@69615
   486
  assumes \<F>: "\<And>S. S \<in> \<F> \<Longrightarrow> open S"
immler@69615
   487
  obtains \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
immler@69615
   488
proof -
immler@69615
   489
  obtain \<B> :: "'a set set"
immler@69615
   490
    where "countable \<B>" "\<And>C. C \<in> \<B> \<Longrightarrow> open C"
immler@69615
   491
      and \<B>: "\<And>S. open S \<Longrightarrow> \<exists>U. U \<subseteq> \<B> \<and> S = \<Union>U"
immler@69615
   492
    using univ_second_countable by blast
immler@69615
   493
  define \<D> where "\<D> \<equiv> {S. S \<in> \<B> \<and> (\<exists>U. U \<in> \<F> \<and> S \<subseteq> U)}"
immler@69615
   494
  have "countable \<D>"
immler@69615
   495
    apply (rule countable_subset [OF _ \<open>countable \<B>\<close>])
immler@69615
   496
    apply (force simp: \<D>_def)
immler@69615
   497
    done
immler@69615
   498
  have "\<And>S. \<exists>U. S \<in> \<D> \<longrightarrow> U \<in> \<F> \<and> S \<subseteq> U"
immler@69615
   499
    by (simp add: \<D>_def)
immler@69615
   500
  then obtain G where G: "\<And>S. S \<in> \<D> \<longrightarrow> G S \<in> \<F> \<and> S \<subseteq> G S"
immler@69615
   501
    by metis
immler@69615
   502
  have "\<Union>\<F> \<subseteq> \<Union>\<D>"
immler@69615
   503
    unfolding \<D>_def by (blast dest: \<F> \<B>)
immler@69615
   504
  moreover have "\<Union>\<D> \<subseteq> \<Union>\<F>"
immler@69615
   505
    using \<D>_def by blast
immler@69615
   506
  ultimately have eq1: "\<Union>\<F> = \<Union>\<D>" ..
immler@69615
   507
  have eq2: "\<Union>\<D> = \<Union> (G ` \<D>)"
immler@69615
   508
    using G eq1 by auto
immler@69615
   509
  show ?thesis
immler@69615
   510
    apply (rule_tac \<F>' = "G ` \<D>" in that)
immler@69615
   511
    using G \<open>countable \<D>\<close>
immler@69615
   512
    by (auto simp: eq1 eq2)
immler@69615
   513
qed
immler@69615
   514
immler@69615
   515
lemma countable_disjoint_open_subsets:
immler@69615
   516
  fixes \<F> :: "'a::second_countable_topology set set"
immler@69615
   517
  assumes "\<And>S. S \<in> \<F> \<Longrightarrow> open S" and pw: "pairwise disjnt \<F>"
immler@69615
   518
    shows "countable \<F>"
immler@69615
   519
proof -
immler@69615
   520
  obtain \<F>' where "\<F>' \<subseteq> \<F>" "countable \<F>'" "\<Union>\<F>' = \<Union>\<F>"
immler@69615
   521
    by (meson assms Lindelof)
immler@69615
   522
  with pw have "\<F> \<subseteq> insert {} \<F>'"
immler@69615
   523
    by (fastforce simp add: pairwise_def disjnt_iff)
immler@69615
   524
  then show ?thesis
immler@69615
   525
    by (simp add: \<open>countable \<F>'\<close> countable_subset)
immler@69615
   526
qed
immler@69615
   527
immler@69516
   528
sublocale second_countable_topology <
immler@69748
   529
  countable_basis "open" "SOME B. countable B \<and> topological_basis B"
immler@69516
   530
  using someI_ex[OF ex_countable_basis]
immler@69516
   531
  by unfold_locales safe
immler@69516
   532
immler@69615
   533
immler@69516
   534
instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
immler@69516
   535
proof
immler@69516
   536
  obtain A :: "'a set set" where "countable A" "topological_basis A"
immler@69516
   537
    using ex_countable_basis by auto
immler@69516
   538
  moreover
immler@69516
   539
  obtain B :: "'b set set" where "countable B" "topological_basis B"
immler@69516
   540
    using ex_countable_basis by auto
immler@69516
   541
  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> open = generate_topology B"
immler@69516
   542
    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod
immler@69516
   543
      topological_basis_imp_subbasis)
immler@69516
   544
qed
immler@69516
   545
immler@69516
   546
instance second_countable_topology \<subseteq> first_countable_topology
immler@69516
   547
proof
immler@69516
   548
  fix x :: 'a
immler@69516
   549
  define B :: "'a set set" where "B = (SOME B. countable B \<and> topological_basis B)"
immler@69516
   550
  then have B: "countable B" "topological_basis B"
immler@69516
   551
    using countable_basis is_basis
immler@69516
   552
    by (auto simp: countable_basis is_basis)
immler@69516
   553
  then show "\<exists>A::nat \<Rightarrow> 'a set.
immler@69516
   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))"
immler@69516
   555
    by (intro first_countableI[of "{b\<in>B. x \<in> b}"])
immler@69516
   556
       (fastforce simp: topological_space_class.topological_basis_def)+
immler@69516
   557
qed
immler@69516
   558
immler@69516
   559
instance nat :: second_countable_topology
immler@69516
   560
proof
immler@69516
   561
  show "\<exists>B::nat set set. countable B \<and> open = generate_topology B"
immler@69516
   562
    by (intro exI[of _ "range lessThan \<union> range greaterThan"]) (auto simp: open_nat_def)
immler@69516
   563
qed
immler@69516
   564
immler@69516
   565
lemma countable_separating_set_linorder1:
immler@69516
   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))"
immler@69516
   567
proof -
immler@69516
   568
  obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
immler@69516
   569
  define B1 where "B1 = {(LEAST x. x \<in> U)| U. U \<in> A}"
immler@69516
   570
  then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
immler@69516
   571
  define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}"
immler@69516
   572
  then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
immler@69516
   573
  have "\<exists>b \<in> B1 \<union> B2. x < b \<and> b \<le> y" if "x < y" for x y
immler@69516
   574
  proof (cases)
immler@69516
   575
    assume "\<exists>z. x < z \<and> z < y"
immler@69516
   576
    then obtain z where z: "x < z \<and> z < y" by auto
immler@69516
   577
    define U where "U = {x<..<y}"
immler@69516
   578
    then have "open U" by simp
immler@69516
   579
    moreover have "z \<in> U" using z U_def by simp
immler@69516
   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
immler@69516
   581
    define w where "w = (SOME x. x \<in> V)"
immler@69516
   582
    then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
immler@69516
   583
    then have "x < w \<and> w \<le> y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
immler@69516
   584
    moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto
immler@69516
   585
    ultimately show ?thesis by auto
immler@69516
   586
  next
immler@69516
   587
    assume "\<not>(\<exists>z. x < z \<and> z < y)"
immler@69516
   588
    then have *: "\<And>z. z > x \<Longrightarrow> z \<ge> y" by auto
immler@69516
   589
    define U where "U = {x<..}"
immler@69516
   590
    then have "open U" by simp
immler@69516
   591
    moreover have "y \<in> U" using \<open>x < y\<close> U_def by simp
immler@69516
   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
immler@69516
   593
    have "U = {y..}" unfolding U_def using * \<open>x < y\<close> by auto
immler@69516
   594
    then have "V \<subseteq> {y..}" using \<open>V \<subseteq> U\<close> by simp
immler@69516
   595
    then have "(LEAST w. w \<in> V) = y" using \<open>y \<in> V\<close> by (meson Least_equality atLeast_iff subsetCE)
immler@69516
   596
    then have "y \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto
immler@69516
   597
    moreover have "x < y \<and> y \<le> y" using \<open>x < y\<close> by simp
immler@69516
   598
    ultimately show ?thesis by auto
immler@69516
   599
  qed
immler@69516
   600
  moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp
immler@69516
   601
  ultimately show ?thesis by auto
immler@69516
   602
qed
immler@69516
   603
immler@69516
   604
lemma countable_separating_set_linorder2:
immler@69516
   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))"
immler@69516
   606
proof -
immler@69516
   607
  obtain A::"'a set set" where "countable A" "topological_basis A" using ex_countable_basis by auto
immler@69516
   608
  define B1 where "B1 = {(GREATEST x. x \<in> U) | U. U \<in> A}"
immler@69516
   609
  then have "countable B1" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
immler@69516
   610
  define B2 where "B2 = {(SOME x. x \<in> U)| U. U \<in> A}"
immler@69516
   611
  then have "countable B2" using \<open>countable A\<close> by (simp add: Setcompr_eq_image)
immler@69516
   612
  have "\<exists>b \<in> B1 \<union> B2. x \<le> b \<and> b < y" if "x < y" for x y
immler@69516
   613
  proof (cases)
immler@69516
   614
    assume "\<exists>z. x < z \<and> z < y"
immler@69516
   615
    then obtain z where z: "x < z \<and> z < y" by auto
immler@69516
   616
    define U where "U = {x<..<y}"
immler@69516
   617
    then have "open U" by simp
immler@69516
   618
    moreover have "z \<in> U" using z U_def by simp
immler@69516
   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
immler@69516
   620
    define w where "w = (SOME x. x \<in> V)"
immler@69516
   621
    then have "w \<in> V" using \<open>z \<in> V\<close> by (metis someI2)
immler@69516
   622
    then have "x \<le> w \<and> w < y" using \<open>w \<in> V\<close> \<open>V \<subseteq> U\<close> U_def by fastforce
immler@69516
   623
    moreover have "w \<in> B1 \<union> B2" using w_def B2_def \<open>V \<in> A\<close> by auto
immler@69516
   624
    ultimately show ?thesis by auto
immler@69516
   625
  next
immler@69516
   626
    assume "\<not>(\<exists>z. x < z \<and> z < y)"
immler@69516
   627
    then have *: "\<And>z. z < y \<Longrightarrow> z \<le> x" using leI by blast
immler@69516
   628
    define U where "U = {..<y}"
immler@69516
   629
    then have "open U" by simp
immler@69516
   630
    moreover have "x \<in> U" using \<open>x < y\<close> U_def by simp
immler@69516
   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
immler@69516
   632
    have "U = {..x}" unfolding U_def using * \<open>x < y\<close> by auto
immler@69516
   633
    then have "V \<subseteq> {..x}" using \<open>V \<subseteq> U\<close> by simp
immler@69516
   634
    then have "(GREATEST x. x \<in> V) = x" using \<open>x \<in> V\<close> by (meson Greatest_equality atMost_iff subsetCE)
immler@69516
   635
    then have "x \<in> B1 \<union> B2" using \<open>V \<in> A\<close> B1_def by auto
immler@69516
   636
    moreover have "x \<le> x \<and> x < y" using \<open>x < y\<close> by simp
immler@69516
   637
    ultimately show ?thesis by auto
immler@69516
   638
  qed
immler@69516
   639
  moreover have "countable (B1 \<union> B2)" using \<open>countable B1\<close> \<open>countable B2\<close> by simp
immler@69516
   640
  ultimately show ?thesis by auto
immler@69516
   641
qed
immler@69516
   642
immler@69516
   643
lemma countable_separating_set_dense_linorder:
immler@69516
   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))"
immler@69516
   645
proof -
immler@69516
   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)"
immler@69516
   647
    using countable_separating_set_linorder1 by auto
immler@69516
   648
  have "\<exists>b \<in> B. x < b \<and> b < y" if "x < y" for x y
immler@69516
   649
  proof -
immler@69516
   650
    obtain z where "x < z" "z < y" using \<open>x < y\<close> dense by blast
immler@69516
   651
    then obtain b where "b \<in> B" "x < b \<and> b \<le> z" using B(2) by auto
immler@69516
   652
    then have "x < b \<and> b < y" using \<open>z < y\<close> by auto
immler@69516
   653
    then show ?thesis using \<open>b \<in> B\<close> by auto
immler@69516
   654
  qed
immler@69516
   655
  then show ?thesis using B(1) by auto
immler@69516
   656
qed
immler@69516
   657
immler@69615
   658
immler@69683
   659
subsection \<open>Polish spaces\<close>
immler@69516
   660
immler@69516
   661
text \<open>Textbooks define Polish spaces as completely metrizable.
immler@69516
   662
  We assume the topology to be complete for a given metric.\<close>
immler@69516
   663
immler@69516
   664
class polish_space = complete_space + second_countable_topology
immler@69516
   665
immler@69516
   666
immler@69544
   667
subsection \<open>Limit Points\<close>
immler@69516
   668
immler@69516
   669
definition%important (in topological_space) islimpt:: "'a \<Rightarrow> 'a set \<Rightarrow> bool"  (infixr "islimpt" 60)
immler@69516
   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))"
immler@69516
   671
immler@69516
   672
lemma islimptI:
immler@69516
   673
  assumes "\<And>T. x \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
immler@69516
   674
  shows "x islimpt S"
immler@69516
   675
  using assms unfolding islimpt_def by auto
immler@69516
   676
immler@69516
   677
lemma islimptE:
immler@69516
   678
  assumes "x islimpt S" and "x \<in> T" and "open T"
immler@69516
   679
  obtains y where "y \<in> S" and "y \<in> T" and "y \<noteq> x"
immler@69516
   680
  using assms unfolding islimpt_def by auto
immler@69516
   681
immler@69516
   682
lemma islimpt_iff_eventually: "x islimpt S \<longleftrightarrow> \<not> eventually (\<lambda>y. y \<notin> S) (at x)"
immler@69516
   683
  unfolding islimpt_def eventually_at_topological by auto
immler@69516
   684
immler@69516
   685
lemma islimpt_subset: "x islimpt S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> x islimpt T"
immler@69516
   686
  unfolding islimpt_def by fast
immler@69516
   687
immler@69516
   688
lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
immler@69516
   689
  unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
immler@69516
   690
immler@69516
   691
lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
immler@69516
   692
  unfolding islimpt_def by blast
immler@69516
   693
immler@69516
   694
text \<open>A perfect space has no isolated points.\<close>
immler@69516
   695
immler@69516
   696
lemma islimpt_UNIV [simp, intro]: "x islimpt UNIV"
immler@69516
   697
  for x :: "'a::perfect_space"
immler@69516
   698
  unfolding islimpt_UNIV_iff by (rule not_open_singleton)
immler@69516
   699
immler@69516
   700
lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
immler@69516
   701
  unfolding closed_def
immler@69516
   702
  apply (subst open_subopen)
immler@69516
   703
  apply (simp add: islimpt_def subset_eq)
immler@69516
   704
  apply (metis ComplE ComplI)
immler@69516
   705
  done
immler@69516
   706
immler@69516
   707
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
immler@69516
   708
  by (auto simp: islimpt_def)
immler@69516
   709
immler@69516
   710
lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
immler@69516
   711
  by (simp add: islimpt_iff_eventually eventually_conj_iff)
immler@69516
   712
immler@69544
   713
immler@69544
   714
lemma islimpt_insert:
immler@69544
   715
  fixes x :: "'a::t1_space"
immler@69544
   716
  shows "x islimpt (insert a s) \<longleftrightarrow> x islimpt s"
immler@69544
   717
proof
immler@69544
   718
  assume *: "x islimpt (insert a s)"
immler@69544
   719
  show "x islimpt s"
immler@69544
   720
  proof (rule islimptI)
immler@69544
   721
    fix t
immler@69544
   722
    assume t: "x \<in> t" "open t"
immler@69544
   723
    show "\<exists>y\<in>s. y \<in> t \<and> y \<noteq> x"
immler@69544
   724
    proof (cases "x = a")
immler@69544
   725
      case True
immler@69544
   726
      obtain y where "y \<in> insert a s" "y \<in> t" "y \<noteq> x"
immler@69544
   727
        using * t by (rule islimptE)
immler@69544
   728
      with \<open>x = a\<close> show ?thesis by auto
immler@69544
   729
    next
immler@69544
   730
      case False
immler@69544
   731
      with t have t': "x \<in> t - {a}" "open (t - {a})"
immler@69544
   732
        by (simp_all add: open_Diff)
immler@69544
   733
      obtain y where "y \<in> insert a s" "y \<in> t - {a}" "y \<noteq> x"
immler@69544
   734
        using * t' by (rule islimptE)
immler@69544
   735
      then show ?thesis by auto
immler@69544
   736
    qed
immler@69516
   737
  qed
immler@69544
   738
next
immler@69544
   739
  assume "x islimpt s"
immler@69544
   740
  then show "x islimpt (insert a s)"
immler@69544
   741
    by (rule islimpt_subset) auto
immler@69544
   742
qed
immler@69544
   743
immler@69544
   744
lemma islimpt_finite:
immler@69544
   745
  fixes x :: "'a::t1_space"
immler@69544
   746
  shows "finite s \<Longrightarrow> \<not> x islimpt s"
immler@69544
   747
  by (induct set: finite) (simp_all add: islimpt_insert)
immler@69544
   748
immler@69544
   749
lemma islimpt_Un_finite:
immler@69544
   750
  fixes x :: "'a::t1_space"
immler@69544
   751
  shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
immler@69544
   752
  by (simp add: islimpt_Un islimpt_finite)
immler@69544
   753
immler@69544
   754
lemma islimpt_eq_acc_point:
immler@69544
   755
  fixes l :: "'a :: t1_space"
immler@69544
   756
  shows "l islimpt S \<longleftrightarrow> (\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> S))"
immler@69544
   757
proof (safe intro!: islimptI)
immler@69544
   758
  fix U
immler@69544
   759
  assume "l islimpt S" "l \<in> U" "open U" "finite (U \<inter> S)"
immler@69544
   760
  then have "l islimpt S" "l \<in> (U - (U \<inter> S - {l}))" "open (U - (U \<inter> S - {l}))"
immler@69544
   761
    by (auto intro: finite_imp_closed)
immler@69544
   762
  then show False
immler@69544
   763
    by (rule islimptE) auto
immler@69544
   764
next
immler@69544
   765
  fix T
immler@69544
   766
  assume *: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> S)" "l \<in> T" "open T"
immler@69544
   767
  then have "infinite (T \<inter> S - {l})"
immler@69544
   768
    by auto
immler@69544
   769
  then have "\<exists>x. x \<in> (T \<inter> S - {l})"
immler@69544
   770
    unfolding ex_in_conv by (intro notI) simp
immler@69544
   771
  then show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> l"
immler@69544
   772
    by auto
immler@69516
   773
qed
immler@69516
   774
immler@69544
   775
lemma acc_point_range_imp_convergent_subsequence:
immler@69544
   776
  fixes l :: "'a :: first_countable_topology"
immler@69544
   777
  assumes l: "\<forall>U. l\<in>U \<longrightarrow> open U \<longrightarrow> infinite (U \<inter> range f)"
immler@69544
   778
  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
immler@69544
   779
proof -
immler@69544
   780
  from countable_basis_at_decseq[of l]
immler@69544
   781
  obtain A where A:
immler@69544
   782
      "\<And>i. open (A i)"
immler@69544
   783
      "\<And>i. l \<in> A i"
immler@69544
   784
      "\<And>S. open S \<Longrightarrow> l \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
immler@69544
   785
    by blast
immler@69544
   786
  define s where "s n i = (SOME j. i < j \<and> f j \<in> A (Suc n))" for n i
immler@69544
   787
  {
immler@69544
   788
    fix n i
immler@69544
   789
    have "infinite (A (Suc n) \<inter> range f - f`{.. i})"
immler@69544
   790
      using l A by auto
immler@69544
   791
    then have "\<exists>x. x \<in> A (Suc n) \<inter> range f - f`{.. i}"
immler@69544
   792
      unfolding ex_in_conv by (intro notI) simp
immler@69544
   793
    then have "\<exists>j. f j \<in> A (Suc n) \<and> j \<notin> {.. i}"
immler@69544
   794
      by auto
immler@69544
   795
    then have "\<exists>a. i < a \<and> f a \<in> A (Suc n)"
immler@69544
   796
      by (auto simp: not_le)
immler@69544
   797
    then have "i < s n i" "f (s n i) \<in> A (Suc n)"
immler@69544
   798
      unfolding s_def by (auto intro: someI2_ex)
immler@69544
   799
  }
immler@69544
   800
  note s = this
immler@69544
   801
  define r where "r = rec_nat (s 0 0) s"
immler@69544
   802
  have "strict_mono r"
immler@69544
   803
    by (auto simp: r_def s strict_mono_Suc_iff)
immler@69544
   804
  moreover
immler@69544
   805
  have "(\<lambda>n. f (r n)) \<longlonglongrightarrow> l"
immler@69544
   806
  proof (rule topological_tendstoI)
immler@69544
   807
    fix S
immler@69544
   808
    assume "open S" "l \<in> S"
immler@69544
   809
    with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially"
immler@69544
   810
      by auto
immler@69544
   811
    moreover
immler@69544
   812
    {
immler@69544
   813
      fix i
immler@69544
   814
      assume "Suc 0 \<le> i"
immler@69544
   815
      then have "f (r i) \<in> A i"
immler@69544
   816
        by (cases i) (simp_all add: r_def s)
immler@69544
   817
    }
immler@69544
   818
    then have "eventually (\<lambda>i. f (r i) \<in> A i) sequentially"
immler@69544
   819
      by (auto simp: eventually_sequentially)
immler@69544
   820
    ultimately show "eventually (\<lambda>i. f (r i) \<in> S) sequentially"
immler@69544
   821
      by eventually_elim auto
immler@69544
   822
  qed
immler@69544
   823
  ultimately show "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
immler@69544
   824
    by (auto simp: convergent_def comp_def)
immler@69544
   825
qed
immler@69516
   826
immler@69544
   827
lemma islimpt_range_imp_convergent_subsequence:
immler@69544
   828
  fixes l :: "'a :: {t1_space, first_countable_topology}"
immler@69544
   829
  assumes l: "l islimpt (range f)"
immler@69544
   830
  shows "\<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
immler@69544
   831
  using l unfolding islimpt_eq_acc_point
immler@69544
   832
  by (rule acc_point_range_imp_convergent_subsequence)
immler@69516
   833
immler@69544
   834
lemma sequence_unique_limpt:
immler@69544
   835
  fixes f :: "nat \<Rightarrow> 'a::t2_space"
immler@69544
   836
  assumes "(f \<longlongrightarrow> l) sequentially"
immler@69544
   837
    and "l' islimpt (range f)"
immler@69544
   838
  shows "l' = l"
immler@69544
   839
proof (rule ccontr)
immler@69544
   840
  assume "l' \<noteq> l"
immler@69544
   841
  obtain s t where "open s" "open t" "l' \<in> s" "l \<in> t" "s \<inter> t = {}"
immler@69544
   842
    using hausdorff [OF \<open>l' \<noteq> l\<close>] by auto
immler@69544
   843
  have "eventually (\<lambda>n. f n \<in> t) sequentially"
immler@69544
   844
    using assms(1) \<open>open t\<close> \<open>l \<in> t\<close> by (rule topological_tendstoD)
immler@69544
   845
  then obtain N where "\<forall>n\<ge>N. f n \<in> t"
immler@69544
   846
    unfolding eventually_sequentially by auto
immler@69544
   847
immler@69544
   848
  have "UNIV = {..<N} \<union> {N..}"
immler@69544
   849
    by auto
immler@69544
   850
  then have "l' islimpt (f ` ({..<N} \<union> {N..}))"
immler@69544
   851
    using assms(2) by simp
immler@69544
   852
  then have "l' islimpt (f ` {..<N} \<union> f ` {N..})"
immler@69544
   853
    by (simp add: image_Un)
immler@69544
   854
  then have "l' islimpt (f ` {N..})"
immler@69544
   855
    by (simp add: islimpt_Un_finite)
immler@69544
   856
  then obtain y where "y \<in> f ` {N..}" "y \<in> s" "y \<noteq> l'"
immler@69544
   857
    using \<open>l' \<in> s\<close> \<open>open s\<close> by (rule islimptE)
immler@69544
   858
  then obtain n where "N \<le> n" "f n \<in> s" "f n \<noteq> l'"
immler@69544
   859
    by auto
immler@69544
   860
  with \<open>\<forall>n\<ge>N. f n \<in> t\<close> have "f n \<in> s \<inter> t"
immler@69544
   861
    by simp
immler@69544
   862
  with \<open>s \<inter> t = {}\<close> show False
immler@69544
   863
    by simp
immler@69516
   864
qed
immler@69516
   865
immler@69516
   866
immler@69516
   867
subsection \<open>Interior of a Set\<close>
immler@69516
   868
nipkow@69564
   869
definition%important interior :: "('a::topological_space) set \<Rightarrow> 'a set" where
nipkow@69564
   870
"interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
immler@69516
   871
immler@69516
   872
lemma interiorI [intro?]:
immler@69516
   873
  assumes "open T" and "x \<in> T" and "T \<subseteq> S"
immler@69516
   874
  shows "x \<in> interior S"
immler@69516
   875
  using assms unfolding interior_def by fast
immler@69516
   876
immler@69516
   877
lemma interiorE [elim?]:
immler@69516
   878
  assumes "x \<in> interior S"
immler@69516
   879
  obtains T where "open T" and "x \<in> T" and "T \<subseteq> S"
immler@69516
   880
  using assms unfolding interior_def by fast
immler@69516
   881
immler@69516
   882
lemma open_interior [simp, intro]: "open (interior S)"
immler@69516
   883
  by (simp add: interior_def open_Union)
immler@69516
   884
immler@69516
   885
lemma interior_subset: "interior S \<subseteq> S"
immler@69516
   886
  by (auto simp: interior_def)
immler@69516
   887
immler@69516
   888
lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
immler@69516
   889
  by (auto simp: interior_def)
immler@69516
   890
immler@69516
   891
lemma interior_open: "open S \<Longrightarrow> interior S = S"
immler@69516
   892
  by (intro equalityI interior_subset interior_maximal subset_refl)
immler@69516
   893
immler@69516
   894
lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
immler@69516
   895
  by (metis open_interior interior_open)
immler@69516
   896
immler@69516
   897
lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
immler@69516
   898
  by (metis interior_maximal interior_subset subset_trans)
immler@69516
   899
immler@69516
   900
lemma interior_empty [simp]: "interior {} = {}"
immler@69516
   901
  using open_empty by (rule interior_open)
immler@69516
   902
immler@69516
   903
lemma interior_UNIV [simp]: "interior UNIV = UNIV"
immler@69516
   904
  using open_UNIV by (rule interior_open)
immler@69516
   905
immler@69516
   906
lemma interior_interior [simp]: "interior (interior S) = interior S"
immler@69516
   907
  using open_interior by (rule interior_open)
immler@69516
   908
immler@69516
   909
lemma interior_mono: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
immler@69516
   910
  by (auto simp: interior_def)
immler@69516
   911
immler@69516
   912
lemma interior_unique:
immler@69516
   913
  assumes "T \<subseteq> S" and "open T"
immler@69516
   914
  assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T"
immler@69516
   915
  shows "interior S = T"
immler@69516
   916
  by (intro equalityI assms interior_subset open_interior interior_maximal)
immler@69516
   917
immler@69516
   918
lemma interior_singleton [simp]: "interior {a} = {}"
immler@69516
   919
  for a :: "'a::perfect_space"
immler@69516
   920
  apply (rule interior_unique, simp_all)
immler@69516
   921
  using not_open_singleton subset_singletonD
immler@69516
   922
  apply fastforce
immler@69516
   923
  done
immler@69516
   924
immler@69516
   925
lemma interior_Int [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
immler@69516
   926
  by (intro equalityI Int_mono Int_greatest interior_mono Int_lower1
immler@69516
   927
    Int_lower2 interior_maximal interior_subset open_Int open_interior)
immler@69516
   928
immler@69516
   929
lemma eventually_nhds_in_nhd: "x \<in> interior s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
immler@69516
   930
  using interior_subset[of s] by (subst eventually_nhds) blast
immler@69516
   931
immler@69516
   932
lemma interior_limit_point [intro]:
immler@69516
   933
  fixes x :: "'a::perfect_space"
immler@69516
   934
  assumes x: "x \<in> interior S"
immler@69516
   935
  shows "x islimpt S"
immler@69516
   936
  using x islimpt_UNIV [of x]
immler@69516
   937
  unfolding interior_def islimpt_def
immler@69516
   938
  apply (clarsimp, rename_tac T T')
immler@69516
   939
  apply (drule_tac x="T \<inter> T'" in spec)
immler@69516
   940
  apply (auto simp: open_Int)
immler@69516
   941
  done
immler@69516
   942
immler@69516
   943
lemma interior_closed_Un_empty_interior:
immler@69516
   944
  assumes cS: "closed S"
immler@69516
   945
    and iT: "interior T = {}"
immler@69516
   946
  shows "interior (S \<union> T) = interior S"
immler@69516
   947
proof
immler@69516
   948
  show "interior S \<subseteq> interior (S \<union> T)"
immler@69516
   949
    by (rule interior_mono) (rule Un_upper1)
immler@69516
   950
  show "interior (S \<union> T) \<subseteq> interior S"
immler@69516
   951
  proof
immler@69516
   952
    fix x
immler@69516
   953
    assume "x \<in> interior (S \<union> T)"
immler@69516
   954
    then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
immler@69516
   955
    show "x \<in> interior S"
immler@69516
   956
    proof (rule ccontr)
immler@69516
   957
      assume "x \<notin> interior S"
immler@69516
   958
      with \<open>x \<in> R\<close> \<open>open R\<close> obtain y where "y \<in> R - S"
immler@69516
   959
        unfolding interior_def by fast
immler@69516
   960
      from \<open>open R\<close> \<open>closed S\<close> have "open (R - S)"
immler@69516
   961
        by (rule open_Diff)
immler@69516
   962
      from \<open>R \<subseteq> S \<union> T\<close> have "R - S \<subseteq> T"
immler@69516
   963
        by fast
immler@69516
   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
immler@69516
   965
        unfolding interior_def by fast
immler@69516
   966
    qed
immler@69516
   967
  qed
immler@69516
   968
qed
immler@69516
   969
immler@69516
   970
lemma interior_Times: "interior (A \<times> B) = interior A \<times> interior B"
immler@69516
   971
proof (rule interior_unique)
immler@69516
   972
  show "interior A \<times> interior B \<subseteq> A \<times> B"
immler@69516
   973
    by (intro Sigma_mono interior_subset)
immler@69516
   974
  show "open (interior A \<times> interior B)"
immler@69516
   975
    by (intro open_Times open_interior)
immler@69516
   976
  fix T
immler@69516
   977
  assume "T \<subseteq> A \<times> B" and "open T"
immler@69516
   978
  then show "T \<subseteq> interior A \<times> interior B"
immler@69516
   979
  proof safe
immler@69516
   980
    fix x y
immler@69516
   981
    assume "(x, y) \<in> T"
immler@69516
   982
    then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
immler@69516
   983
      using \<open>open T\<close> unfolding open_prod_def by fast
immler@69516
   984
    then have "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
immler@69516
   985
      using \<open>T \<subseteq> A \<times> B\<close> by auto
immler@69516
   986
    then show "x \<in> interior A" and "y \<in> interior B"
immler@69516
   987
      by (auto intro: interiorI)
immler@69516
   988
  qed
immler@69516
   989
qed
immler@69516
   990
immler@69516
   991
lemma interior_Ici:
immler@69516
   992
  fixes x :: "'a :: {dense_linorder,linorder_topology}"
immler@69516
   993
  assumes "b < x"
immler@69516
   994
  shows "interior {x ..} = {x <..}"
immler@69516
   995
proof (rule interior_unique)
immler@69516
   996
  fix T
immler@69516
   997
  assume "T \<subseteq> {x ..}" "open T"
immler@69516
   998
  moreover have "x \<notin> T"
immler@69516
   999
  proof
immler@69516
  1000
    assume "x \<in> T"
immler@69516
  1001
    obtain y where "y < x" "{y <.. x} \<subseteq> T"
immler@69516
  1002
      using open_left[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>b < x\<close>] by auto
immler@69516
  1003
    with dense[OF \<open>y < x\<close>] obtain z where "z \<in> T" "z < x"
immler@69516
  1004
      by (auto simp: subset_eq Ball_def)
immler@69516
  1005
    with \<open>T \<subseteq> {x ..}\<close> show False by auto
immler@69516
  1006
  qed
immler@69516
  1007
  ultimately show "T \<subseteq> {x <..}"
immler@69516
  1008
    by (auto simp: subset_eq less_le)
immler@69516
  1009
qed auto
immler@69516
  1010
immler@69516
  1011
lemma interior_Iic:
immler@69516
  1012
  fixes x :: "'a ::{dense_linorder,linorder_topology}"
immler@69516
  1013
  assumes "x < b"
immler@69516
  1014
  shows "interior {.. x} = {..< x}"
immler@69516
  1015
proof (rule interior_unique)
immler@69516
  1016
  fix T
immler@69516
  1017
  assume "T \<subseteq> {.. x}" "open T"
immler@69516
  1018
  moreover have "x \<notin> T"
immler@69516
  1019
  proof
immler@69516
  1020
    assume "x \<in> T"
immler@69516
  1021
    obtain y where "x < y" "{x ..< y} \<subseteq> T"
immler@69516
  1022
      using open_right[OF \<open>open T\<close> \<open>x \<in> T\<close> \<open>x < b\<close>] by auto
immler@69516
  1023
    with dense[OF \<open>x < y\<close>] obtain z where "z \<in> T" "x < z"
immler@69516
  1024
      by (auto simp: subset_eq Ball_def less_le)
immler@69516
  1025
    with \<open>T \<subseteq> {.. x}\<close> show False by auto
immler@69516
  1026
  qed
immler@69516
  1027
  ultimately show "T \<subseteq> {..< x}"
immler@69516
  1028
    by (auto simp: subset_eq less_le)
immler@69516
  1029
qed auto
immler@69516
  1030
immler@69615
  1031
lemma countable_disjoint_nonempty_interior_subsets:
immler@69615
  1032
  fixes \<F> :: "'a::second_countable_topology set set"
immler@69615
  1033
  assumes pw: "pairwise disjnt \<F>" and int: "\<And>S. \<lbrakk>S \<in> \<F>; interior S = {}\<rbrakk> \<Longrightarrow> S = {}"
immler@69615
  1034
  shows "countable \<F>"
immler@69615
  1035
proof (rule countable_image_inj_on)
immler@69615
  1036
  have "disjoint (interior ` \<F>)"
immler@69615
  1037
    using pw by (simp add: disjoint_image_subset interior_subset)
immler@69615
  1038
  then show "countable (interior ` \<F>)"
immler@69615
  1039
    by (auto intro: countable_disjoint_open_subsets)
immler@69615
  1040
  show "inj_on interior \<F>"
immler@69615
  1041
    using pw apply (clarsimp simp: inj_on_def pairwise_def)
immler@69615
  1042
    apply (metis disjnt_def disjnt_subset1 inf.orderE int interior_subset)
immler@69615
  1043
    done
immler@69615
  1044
qed
immler@69516
  1045
immler@69516
  1046
subsection \<open>Closure of a Set\<close>
immler@69516
  1047
nipkow@69564
  1048
definition%important closure :: "('a::topological_space) set \<Rightarrow> 'a set" where
nipkow@69564
  1049
"closure S = S \<union> {x . x islimpt S}"
immler@69516
  1050
immler@69516
  1051
lemma interior_closure: "interior S = - (closure (- S))"
immler@69516
  1052
  by (auto simp: interior_def closure_def islimpt_def)
immler@69516
  1053
immler@69516
  1054
lemma closure_interior: "closure S = - interior (- S)"
immler@69516
  1055
  by (simp add: interior_closure)
immler@69516
  1056
immler@69516
  1057
lemma closed_closure[simp, intro]: "closed (closure S)"
immler@69516
  1058
  by (simp add: closure_interior closed_Compl)
immler@69516
  1059
immler@69516
  1060
lemma closure_subset: "S \<subseteq> closure S"
immler@69516
  1061
  by (simp add: closure_def)
immler@69516
  1062
immler@69516
  1063
lemma closure_hull: "closure S = closed hull S"
immler@69516
  1064
  by (auto simp: hull_def closure_interior interior_def)
immler@69516
  1065
immler@69516
  1066
lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
immler@69516
  1067
  unfolding closure_hull using closed_Inter by (rule hull_eq)
immler@69516
  1068
immler@69516
  1069
lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
immler@69516
  1070
  by (simp only: closure_eq)
immler@69516
  1071
immler@69516
  1072
lemma closure_closure [simp]: "closure (closure S) = closure S"
immler@69516
  1073
  unfolding closure_hull by (rule hull_hull)
immler@69516
  1074
immler@69516
  1075
lemma closure_mono: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
immler@69516
  1076
  unfolding closure_hull by (rule hull_mono)
immler@69516
  1077
immler@69516
  1078
lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
immler@69516
  1079
  unfolding closure_hull by (rule hull_minimal)
immler@69516
  1080
immler@69516
  1081
lemma closure_unique:
immler@69516
  1082
  assumes "S \<subseteq> T"
immler@69516
  1083
    and "closed T"
immler@69516
  1084
    and "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
immler@69516
  1085
  shows "closure S = T"
immler@69516
  1086
  using assms unfolding closure_hull by (rule hull_unique)
immler@69516
  1087
immler@69516
  1088
lemma closure_empty [simp]: "closure {} = {}"
immler@69516
  1089
  using closed_empty by (rule closure_closed)
immler@69516
  1090
immler@69516
  1091
lemma closure_UNIV [simp]: "closure UNIV = UNIV"
immler@69516
  1092
  using closed_UNIV by (rule closure_closed)
immler@69516
  1093
immler@69516
  1094
lemma closure_Un [simp]: "closure (S \<union> T) = closure S \<union> closure T"
immler@69516
  1095
  by (simp add: closure_interior)
immler@69516
  1096
immler@69516
  1097
lemma closure_eq_empty [iff]: "closure S = {} \<longleftrightarrow> S = {}"
immler@69516
  1098
  using closure_empty closure_subset[of S] by blast
immler@69516
  1099
immler@69516
  1100
lemma closure_subset_eq: "closure S \<subseteq> S \<longleftrightarrow> closed S"
immler@69516
  1101
  using closure_eq[of S] closure_subset[of S] by simp
immler@69516
  1102
immler@69516
  1103
lemma open_Int_closure_eq_empty: "open S \<Longrightarrow> (S \<inter> closure T) = {} \<longleftrightarrow> S \<inter> T = {}"
immler@69516
  1104
  using open_subset_interior[of S "- T"]
immler@69516
  1105
  using interior_subset[of "- T"]
immler@69516
  1106
  by (auto simp: closure_interior)
immler@69516
  1107
immler@69516
  1108
lemma open_Int_closure_subset: "open S \<Longrightarrow> S \<inter> closure T \<subseteq> closure (S \<inter> T)"
immler@69516
  1109
proof
immler@69516
  1110
  fix x
immler@69516
  1111
  assume *: "open S" "x \<in> S \<inter> closure T"
immler@69516
  1112
  have "x islimpt (S \<inter> T)" if **: "x islimpt T"
immler@69516
  1113
  proof (rule islimptI)
immler@69516
  1114
    fix A
immler@69516
  1115
    assume "x \<in> A" "open A"
immler@69516
  1116
    with * have "x \<in> A \<inter> S" "open (A \<inter> S)"
immler@69516
  1117
      by (simp_all add: open_Int)
immler@69516
  1118
    with ** obtain y where "y \<in> T" "y \<in> A \<inter> S" "y \<noteq> x"
immler@69516
  1119
      by (rule islimptE)
immler@69516
  1120
    then have "y \<in> S \<inter> T" "y \<in> A \<and> y \<noteq> x"
immler@69516
  1121
      by simp_all
immler@69516
  1122
    then show "\<exists>y\<in>(S \<inter> T). y \<in> A \<and> y \<noteq> x" ..
immler@69516
  1123
  qed
immler@69516
  1124
  with * show "x \<in> closure (S \<inter> T)"
immler@69516
  1125
    unfolding closure_def by blast
immler@69516
  1126
qed
immler@69516
  1127
immler@69516
  1128
lemma closure_complement: "closure (- S) = - interior S"
immler@69516
  1129
  by (simp add: closure_interior)
immler@69516
  1130
immler@69516
  1131
lemma interior_complement: "interior (- S) = - closure S"
immler@69516
  1132
  by (simp add: closure_interior)
immler@69516
  1133
immler@69516
  1134
lemma interior_diff: "interior(S - T) = interior S - closure T"
immler@69516
  1135
  by (simp add: Diff_eq interior_complement)
immler@69516
  1136
immler@69516
  1137
lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
immler@69516
  1138
proof (rule closure_unique)
immler@69516
  1139
  show "A \<times> B \<subseteq> closure A \<times> closure B"
immler@69516
  1140
    by (intro Sigma_mono closure_subset)
immler@69516
  1141
  show "closed (closure A \<times> closure B)"
immler@69516
  1142
    by (intro closed_Times closed_closure)
immler@69516
  1143
  fix T
immler@69516
  1144
  assume "A \<times> B \<subseteq> T" and "closed T"
immler@69516
  1145
  then show "closure A \<times> closure B \<subseteq> T"
immler@69516
  1146
    apply (simp add: closed_def open_prod_def, clarify)
immler@69516
  1147
    apply (rule ccontr)
immler@69516
  1148
    apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
immler@69516
  1149
    apply (simp add: closure_interior interior_def)
immler@69516
  1150
    apply (drule_tac x=C in spec)
immler@69516
  1151
    apply (drule_tac x=D in spec, auto)
immler@69516
  1152
    done
immler@69516
  1153
qed
immler@69516
  1154
immler@69516
  1155
lemma islimpt_in_closure: "(x islimpt S) = (x\<in>closure(S-{x}))"
immler@69516
  1156
  unfolding closure_def using islimpt_punctured by blast
immler@69516
  1157
immler@69516
  1158
lemma connected_imp_connected_closure: "connected S \<Longrightarrow> connected (closure S)"
immler@69516
  1159
  by (rule connectedI) (meson closure_subset open_Int open_Int_closure_eq_empty subset_trans connectedD)
immler@69516
  1160
immler@69516
  1161
lemma bdd_below_closure:
immler@69516
  1162
  fixes A :: "real set"
immler@69516
  1163
  assumes "bdd_below A"
immler@69516
  1164
  shows "bdd_below (closure A)"
immler@69516
  1165
proof -
immler@69516
  1166
  from assms obtain m where "\<And>x. x \<in> A \<Longrightarrow> m \<le> x"
immler@69516
  1167
    by (auto simp: bdd_below_def)
immler@69516
  1168
  then have "A \<subseteq> {m..}" by auto
immler@69516
  1169
  then have "closure A \<subseteq> {m..}"
immler@69516
  1170
    using closed_real_atLeast by (rule closure_minimal)
immler@69516
  1171
  then show ?thesis
immler@69516
  1172
    by (auto simp: bdd_below_def)
immler@69516
  1173
qed
immler@69516
  1174
immler@69516
  1175
immler@69516
  1176
subsection \<open>Frontier (also known as boundary)\<close>
immler@69516
  1177
nipkow@69564
  1178
definition%important frontier :: "('a::topological_space) set \<Rightarrow> 'a set" where
nipkow@69564
  1179
"frontier S = closure S - interior S"
immler@69516
  1180
immler@69516
  1181
lemma frontier_closed [iff]: "closed (frontier S)"
immler@69516
  1182
  by (simp add: frontier_def closed_Diff)
immler@69516
  1183
immler@69516
  1184
lemma frontier_closures: "frontier S = closure S \<inter> closure (- S)"
immler@69516
  1185
  by (auto simp: frontier_def interior_closure)
immler@69516
  1186
immler@69516
  1187
lemma frontier_Int: "frontier(S \<inter> T) = closure(S \<inter> T) \<inter> (frontier S \<union> frontier T)"
immler@69516
  1188
proof -
immler@69516
  1189
  have "closure (S \<inter> T) \<subseteq> closure S" "closure (S \<inter> T) \<subseteq> closure T"
immler@69516
  1190
    by (simp_all add: closure_mono)
immler@69516
  1191
  then show ?thesis
immler@69516
  1192
    by (auto simp: frontier_closures)
immler@69516
  1193
qed
immler@69516
  1194
immler@69516
  1195
lemma frontier_Int_subset: "frontier(S \<inter> T) \<subseteq> frontier S \<union> frontier T"
immler@69516
  1196
  by (auto simp: frontier_Int)
immler@69516
  1197
immler@69516
  1198
lemma frontier_Int_closed:
immler@69516
  1199
  assumes "closed S" "closed T"
immler@69516
  1200
  shows "frontier(S \<inter> T) = (frontier S \<inter> T) \<union> (S \<inter> frontier T)"
immler@69516
  1201
proof -
immler@69516
  1202
  have "closure (S \<inter> T) = T \<inter> S"
immler@69516
  1203
    using assms by (simp add: Int_commute closed_Int)
immler@69516
  1204
  moreover have "T \<inter> (closure S \<inter> closure (- S)) = frontier S \<inter> T"
immler@69516
  1205
    by (simp add: Int_commute frontier_closures)
immler@69516
  1206
  ultimately show ?thesis
immler@69516
  1207
    by (simp add: Int_Un_distrib Int_assoc Int_left_commute assms frontier_closures)
immler@69516
  1208
qed
immler@69516
  1209
immler@69516
  1210
lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
immler@69516
  1211
  by (metis frontier_def closure_closed Diff_subset)
immler@69516
  1212
immler@69516
  1213
lemma frontier_empty [simp]: "frontier {} = {}"
immler@69516
  1214
  by (simp add: frontier_def)
immler@69516
  1215
immler@69516
  1216
lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
immler@69516
  1217
proof -
immler@69516
  1218
  {
immler@69516
  1219
    assume "frontier S \<subseteq> S"
immler@69516
  1220
    then have "closure S \<subseteq> S"
immler@69516
  1221
      using interior_subset unfolding frontier_def by auto
immler@69516
  1222
    then have "closed S"
immler@69516
  1223
      using closure_subset_eq by auto
immler@69516
  1224
  }
immler@69516
  1225
  then show ?thesis using frontier_subset_closed[of S] ..
immler@69516
  1226
qed
immler@69516
  1227
immler@69516
  1228
lemma frontier_complement [simp]: "frontier (- S) = frontier S"
immler@69516
  1229
  by (auto simp: frontier_def closure_complement interior_complement)
immler@69516
  1230
immler@69516
  1231
lemma frontier_Un_subset: "frontier(S \<union> T) \<subseteq> frontier S \<union> frontier T"
immler@69516
  1232
  by (metis compl_sup frontier_Int_subset frontier_complement)
immler@69516
  1233
immler@69516
  1234
lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
immler@69516
  1235
  using frontier_complement frontier_subset_eq[of "- S"]
immler@69516
  1236
  unfolding open_closed by auto
immler@69516
  1237
immler@69516
  1238
lemma frontier_UNIV [simp]: "frontier UNIV = {}"
immler@69516
  1239
  using frontier_complement frontier_empty by fastforce
immler@69516
  1240
immler@69516
  1241
lemma frontier_interiors: "frontier s = - interior(s) - interior(-s)"
immler@69516
  1242
  by (simp add: Int_commute frontier_def interior_closure)
immler@69516
  1243
immler@69516
  1244
lemma frontier_interior_subset: "frontier(interior S) \<subseteq> frontier S"
immler@69516
  1245
  by (simp add: Diff_mono frontier_interiors interior_mono interior_subset)
immler@69516
  1246
immler@69516
  1247
lemma closure_Un_frontier: "closure S = S \<union> frontier S"
immler@69516
  1248
proof -
immler@69516
  1249
  have "S \<union> interior S = S"
immler@69516
  1250
    using interior_subset by auto
immler@69516
  1251
  then show ?thesis
immler@69516
  1252
    using closure_subset by (auto simp: frontier_def)
immler@69516
  1253
qed
immler@69516
  1254
immler@69516
  1255
immler@69516
  1256
subsection%unimportant \<open>Filters and the ``eventually true'' quantifier\<close>
immler@69516
  1257
immler@69516
  1258
text \<open>Identify Trivial limits, where we can't approach arbitrarily closely.\<close>
immler@69516
  1259
immler@69516
  1260
lemma trivial_limit_within: "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
immler@69516
  1261
proof
immler@69516
  1262
  assume "trivial_limit (at a within S)"
immler@69516
  1263
  then show "\<not> a islimpt S"
immler@69516
  1264
    unfolding trivial_limit_def
immler@69516
  1265
    unfolding eventually_at_topological
immler@69516
  1266
    unfolding islimpt_def
immler@69516
  1267
    apply (clarsimp simp add: set_eq_iff)
immler@69516
  1268
    apply (rename_tac T, rule_tac x=T in exI)
immler@69516
  1269
    apply (clarsimp, drule_tac x=y in bspec, simp_all)
immler@69516
  1270
    done
immler@69516
  1271
next
immler@69516
  1272
  assume "\<not> a islimpt S"
immler@69516
  1273
  then show "trivial_limit (at a within S)"
immler@69516
  1274
    unfolding trivial_limit_def eventually_at_topological islimpt_def
immler@69516
  1275
    by metis
immler@69516
  1276
qed
immler@69516
  1277
immler@69516
  1278
lemma trivial_limit_at_iff: "trivial_limit (at a) \<longleftrightarrow> \<not> a islimpt UNIV"
immler@69516
  1279
  using trivial_limit_within [of a UNIV] by simp
immler@69516
  1280
immler@69516
  1281
lemma trivial_limit_at: "\<not> trivial_limit (at a)"
immler@69516
  1282
  for a :: "'a::perfect_space"
immler@69516
  1283
  by (rule at_neq_bot)
immler@69516
  1284
immler@69516
  1285
lemma not_trivial_limit_within: "\<not> trivial_limit (at x within S) = (x \<in> closure (S - {x}))"
immler@69516
  1286
  using islimpt_in_closure by (metis trivial_limit_within)
immler@69516
  1287
immler@69516
  1288
lemma not_in_closure_trivial_limitI:
immler@69516
  1289
  "x \<notin> closure s \<Longrightarrow> trivial_limit (at x within s)"
immler@69516
  1290
  using not_trivial_limit_within[of x s]
immler@69516
  1291
  by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD)
immler@69516
  1292
immler@69516
  1293
lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)"
immler@69516
  1294
  if "x \<in> closure s \<Longrightarrow> filterlim f l (at x within s)"
immler@69516
  1295
  by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that)
immler@69516
  1296
immler@69516
  1297
lemma at_within_eq_bot_iff: "at c within A = bot \<longleftrightarrow> c \<notin> closure (A - {c})"
immler@69516
  1298
  using not_trivial_limit_within[of c A] by blast
immler@69516
  1299
immler@69516
  1300
text \<open>Some property holds "sufficiently close" to the limit point.\<close>
immler@69516
  1301
immler@69516
  1302
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
immler@69516
  1303
  by simp
immler@69516
  1304
immler@69516
  1305
lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
immler@69516
  1306
  by (simp add: filter_eq_iff)
immler@69516
  1307
immler@69613
  1308
lemma Lim_topological:
immler@69613
  1309
  "(f \<longlongrightarrow> l) net \<longleftrightarrow>
immler@69613
  1310
    trivial_limit net \<or> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
immler@69613
  1311
  unfolding tendsto_def trivial_limit_eq by auto
immler@69613
  1312
immler@69613
  1313
lemma eventually_within_Un:
immler@69613
  1314
  "eventually P (at x within (s \<union> t)) \<longleftrightarrow>
immler@69613
  1315
    eventually P (at x within s) \<and> eventually P (at x within t)"
immler@69613
  1316
  unfolding eventually_at_filter
immler@69613
  1317
  by (auto elim!: eventually_rev_mp)
immler@69613
  1318
immler@69613
  1319
lemma Lim_within_union:
immler@69613
  1320
 "(f \<longlongrightarrow> l) (at x within (s \<union> t)) \<longleftrightarrow>
immler@69613
  1321
  (f \<longlongrightarrow> l) (at x within s) \<and> (f \<longlongrightarrow> l) (at x within t)"
immler@69613
  1322
  unfolding tendsto_def
immler@69613
  1323
  by (auto simp: eventually_within_Un)
immler@69613
  1324
immler@69516
  1325
immler@69516
  1326
subsection \<open>Limits\<close>
immler@69516
  1327
immler@69516
  1328
lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f \<longlongrightarrow> l) net"
immler@69516
  1329
  by (rule topological_tendstoI) (auto elim: eventually_mono)
immler@69516
  1330
immler@69516
  1331
text \<open>The expected monotonicity property.\<close>
immler@69516
  1332
immler@69516
  1333
lemma Lim_Un:
immler@69516
  1334
  assumes "(f \<longlongrightarrow> l) (at x within S)" "(f \<longlongrightarrow> l) (at x within T)"
immler@69516
  1335
  shows "(f \<longlongrightarrow> l) (at x within (S \<union> T))"
immler@69516
  1336
  using assms unfolding at_within_union by (rule filterlim_sup)
immler@69516
  1337
immler@69516
  1338
lemma Lim_Un_univ:
immler@69516
  1339
  "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T) \<Longrightarrow>
immler@69516
  1340
    S \<union> T = UNIV \<Longrightarrow> (f \<longlongrightarrow> l) (at x)"
immler@69516
  1341
  by (metis Lim_Un)
immler@69516
  1342
immler@69516
  1343
text \<open>Interrelations between restricted and unrestricted limits.\<close>
immler@69516
  1344
immler@69516
  1345
lemma Lim_at_imp_Lim_at_within: "(f \<longlongrightarrow> l) (at x) \<Longrightarrow> (f \<longlongrightarrow> l) (at x within S)"
immler@69516
  1346
  by (metis order_refl filterlim_mono subset_UNIV at_le)
immler@69516
  1347
immler@69516
  1348
lemma eventually_within_interior:
immler@69516
  1349
  assumes "x \<in> interior S"
immler@69516
  1350
  shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)"
immler@69516
  1351
  (is "?lhs = ?rhs")
immler@69516
  1352
proof
immler@69516
  1353
  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
immler@69516
  1354
  {
immler@69516
  1355
    assume ?lhs
immler@69516
  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"
immler@69516
  1357
      by (auto simp: eventually_at_topological)
immler@69516
  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"
immler@69516
  1359
      by auto
immler@69516
  1360
    then show ?rhs
immler@69516
  1361
      by (auto simp: eventually_at_topological)
immler@69516
  1362
  next
immler@69516
  1363
    assume ?rhs
immler@69516
  1364
    then show ?lhs
immler@69516
  1365
      by (auto elim: eventually_mono simp: eventually_at_filter)
immler@69516
  1366
  }
immler@69516
  1367
qed
immler@69516
  1368
immler@69516
  1369
lemma at_within_interior: "x \<in> interior S \<Longrightarrow> at x within S = at x"
immler@69516
  1370
  unfolding filter_eq_iff by (intro allI eventually_within_interior)
immler@69516
  1371
immler@69516
  1372
lemma Lim_within_LIMSEQ:
immler@69516
  1373
  fixes a :: "'a::first_countable_topology"
immler@69516
  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"
immler@69516
  1375
  shows "(X \<longlongrightarrow> L) (at a within T)"
immler@69516
  1376
  using assms unfolding tendsto_def [where l=L]
immler@69516
  1377
  by (simp add: sequentially_imp_eventually_within)
immler@69516
  1378
immler@69516
  1379
lemma Lim_right_bound:
immler@69516
  1380
  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder, no_top} \<Rightarrow>
immler@69516
  1381
    'b::{linorder_topology, conditionally_complete_linorder}"
immler@69516
  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"
immler@69516
  1383
    and bnd: "\<And>a. a \<in> I \<Longrightarrow> x < a \<Longrightarrow> K \<le> f a"
immler@69516
  1384
  shows "(f \<longlongrightarrow> Inf (f ` ({x<..} \<inter> I))) (at x within ({x<..} \<inter> I))"
immler@69516
  1385
proof (cases "{x<..} \<inter> I = {}")
immler@69516
  1386
  case True
immler@69516
  1387
  then show ?thesis by simp
immler@69516
  1388
next
immler@69516
  1389
  case False
immler@69516
  1390
  show ?thesis
immler@69516
  1391
  proof (rule order_tendstoI)
immler@69516
  1392
    fix a
immler@69516
  1393
    assume a: "a < Inf (f ` ({x<..} \<inter> I))"
immler@69516
  1394
    {
immler@69516
  1395
      fix y
immler@69516
  1396
      assume "y \<in> {x<..} \<inter> I"
immler@69516
  1397
      with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
immler@69516
  1398
        by (auto intro!: cInf_lower bdd_belowI2)
immler@69516
  1399
      with a have "a < f y"
immler@69516
  1400
        by (blast intro: less_le_trans)
immler@69516
  1401
    }
immler@69516
  1402
    then show "eventually (\<lambda>x. a < f x) (at x within ({x<..} \<inter> I))"
immler@69516
  1403
      by (auto simp: eventually_at_filter intro: exI[of _ 1] zero_less_one)
immler@69516
  1404
  next
immler@69516
  1405
    fix a
immler@69516
  1406
    assume "Inf (f ` ({x<..} \<inter> I)) < a"
immler@69516
  1407
    from cInf_lessD[OF _ this] False obtain y where y: "x < y" "y \<in> I" "f y < a"
immler@69516
  1408
      by auto
immler@69516
  1409
    then have "eventually (\<lambda>x. x \<in> I \<longrightarrow> f x < a) (at_right x)"
immler@69516
  1410
      unfolding eventually_at_right[OF \<open>x < y\<close>] by (metis less_imp_le le_less_trans mono)
immler@69516
  1411
    then show "eventually (\<lambda>x. f x < a) (at x within ({x<..} \<inter> I))"
immler@69516
  1412
      unfolding eventually_at_filter by eventually_elim simp
immler@69516
  1413
  qed
immler@69516
  1414
qed
immler@69516
  1415
immler@69516
  1416
(*could prove directly from islimpt_sequential_inj, but only for metric spaces*)
immler@69516
  1417
lemma islimpt_sequential:
immler@69516
  1418
  fixes x :: "'a::first_countable_topology"
immler@69516
  1419
  shows "x islimpt S \<longleftrightarrow> (\<exists>f. (\<forall>n::nat. f n \<in> S - {x}) \<and> (f \<longlongrightarrow> x) sequentially)"
immler@69516
  1420
    (is "?lhs = ?rhs")
immler@69516
  1421
proof
immler@69516
  1422
  assume ?lhs
immler@69516
  1423
  from countable_basis_at_decseq[of x] obtain A where A:
immler@69516
  1424
      "\<And>i. open (A i)"
immler@69516
  1425
      "\<And>i. x \<in> A i"
immler@69516
  1426
      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
immler@69516
  1427
    by blast
immler@69516
  1428
  define f where "f n = (SOME y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y)" for n
immler@69516
  1429
  {
immler@69516
  1430
    fix n
immler@69516
  1431
    from \<open>?lhs\<close> have "\<exists>y. y \<in> S \<and> y \<in> A n \<and> x \<noteq> y"
immler@69516
  1432
      unfolding islimpt_def using A(1,2)[of n] by auto
immler@69516
  1433
    then have "f n \<in> S \<and> f n \<in> A n \<and> x \<noteq> f n"
immler@69516
  1434
      unfolding f_def by (rule someI_ex)
immler@69516
  1435
    then have "f n \<in> S" "f n \<in> A n" "x \<noteq> f n" by auto
immler@69516
  1436
  }
immler@69516
  1437
  then have "\<forall>n. f n \<in> S - {x}" by auto
immler@69516
  1438
  moreover have "(\<lambda>n. f n) \<longlonglongrightarrow> x"
immler@69516
  1439
  proof (rule topological_tendstoI)
immler@69516
  1440
    fix S
immler@69516
  1441
    assume "open S" "x \<in> S"
immler@69516
  1442
    from A(3)[OF this] \<open>\<And>n. f n \<in> A n\<close>
immler@69516
  1443
    show "eventually (\<lambda>x. f x \<in> S) sequentially"
immler@69516
  1444
      by (auto elim!: eventually_mono)
immler@69516
  1445
  qed
immler@69516
  1446
  ultimately show ?rhs by fast
immler@69516
  1447
next
immler@69516
  1448
  assume ?rhs
immler@69516
  1449
  then obtain f :: "nat \<Rightarrow> 'a" where f: "\<And>n. f n \<in> S - {x}" and lim: "f \<longlonglongrightarrow> x"
immler@69516
  1450
    by auto
immler@69516
  1451
  show ?lhs
immler@69516
  1452
    unfolding islimpt_def
immler@69516
  1453
  proof safe
immler@69516
  1454
    fix T
immler@69516
  1455
    assume "open T" "x \<in> T"
immler@69516
  1456
    from lim[THEN topological_tendstoD, OF this] f
immler@69516
  1457
    show "\<exists>y\<in>S. y \<in> T \<and> y \<noteq> x"
immler@69516
  1458
      unfolding eventually_sequentially by auto
immler@69516
  1459
  qed
immler@69516
  1460
qed
immler@69516
  1461
immler@69516
  1462
text\<open>Deducing things about the limit from the elements.\<close>
immler@69516
  1463
immler@69516
  1464
lemma Lim_in_closed_set:
immler@69516
  1465
  assumes "closed S"
immler@69516
  1466
    and "eventually (\<lambda>x. f(x) \<in> S) net"
immler@69516
  1467
    and "\<not> trivial_limit net" "(f \<longlongrightarrow> l) net"
immler@69516
  1468
  shows "l \<in> S"
immler@69516
  1469
proof (rule ccontr)
immler@69516
  1470
  assume "l \<notin> S"
immler@69516
  1471
  with \<open>closed S\<close> have "open (- S)" "l \<in> - S"
immler@69516
  1472
    by (simp_all add: open_Compl)
immler@69516
  1473
  with assms(4) have "eventually (\<lambda>x. f x \<in> - S) net"
immler@69516
  1474
    by (rule topological_tendstoD)
immler@69516
  1475
  with assms(2) have "eventually (\<lambda>x. False) net"
immler@69516
  1476
    by (rule eventually_elim2) simp
immler@69516
  1477
  with assms(3) show "False"
immler@69516
  1478
    by (simp add: eventually_False)
immler@69516
  1479
qed
immler@69516
  1480
immler@69544
  1481
text\<open>These are special for limits out of the same topological space.\<close>
immler@69516
  1482
immler@69516
  1483
lemma Lim_within_id: "(id \<longlongrightarrow> a) (at a within s)"
immler@69516
  1484
  unfolding id_def by (rule tendsto_ident_at)
immler@69516
  1485
immler@69516
  1486
lemma Lim_at_id: "(id \<longlongrightarrow> a) (at a)"
immler@69516
  1487
  unfolding id_def by (rule tendsto_ident_at)
immler@69516
  1488
immler@69516
  1489
text\<open>It's also sometimes useful to extract the limit point from the filter.\<close>
immler@69516
  1490
immler@69516
  1491
abbreviation netlimit :: "'a::t2_space filter \<Rightarrow> 'a"
immler@69516
  1492
  where "netlimit F \<equiv> Lim F (\<lambda>x. x)"
immler@69516
  1493
immler@69516
  1494
lemma netlimit_within: "\<not> trivial_limit (at a within S) \<Longrightarrow> netlimit (at a within S) = a"
immler@69516
  1495
  by (rule tendsto_Lim) (auto intro: tendsto_intros)
immler@69516
  1496
immler@69516
  1497
lemma netlimit_at [simp]:
immler@69516
  1498
  fixes a :: "'a::{perfect_space,t2_space}"
immler@69516
  1499
  shows "netlimit (at a) = a"
immler@69516
  1500
  using netlimit_within [of a UNIV] by simp
immler@69516
  1501
immler@69516
  1502
lemma lim_within_interior:
immler@69516
  1503
  "x \<in> interior S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within S) \<longleftrightarrow> (f \<longlongrightarrow> l) (at x)"
immler@69516
  1504
  by (metis at_within_interior)
immler@69516
  1505
immler@69516
  1506
lemma netlimit_within_interior:
immler@69516
  1507
  fixes x :: "'a::{t2_space,perfect_space}"
immler@69516
  1508
  assumes "x \<in> interior S"
immler@69516
  1509
  shows "netlimit (at x within S) = x"
immler@69516
  1510
  using assms by (metis at_within_interior netlimit_at)
immler@69516
  1511
immler@69516
  1512
text\<open>Useful lemmas on closure and set of possible sequential limits.\<close>
immler@69516
  1513
immler@69516
  1514
lemma closure_sequential:
immler@69516
  1515
  fixes l :: "'a::first_countable_topology"
immler@69516
  1516
  shows "l \<in> closure S \<longleftrightarrow> (\<exists>x. (\<forall>n. x n \<in> S) \<and> (x \<longlongrightarrow> l) sequentially)"
immler@69516
  1517
  (is "?lhs = ?rhs")
immler@69516
  1518
proof
immler@69516
  1519
  assume "?lhs"
immler@69516
  1520
  moreover
immler@69516
  1521
  {
immler@69516
  1522
    assume "l \<in> S"
immler@69516
  1523
    then have "?rhs" using tendsto_const[of l sequentially] by auto
immler@69516
  1524
  }
immler@69516
  1525
  moreover
immler@69516
  1526
  {
immler@69516
  1527
    assume "l islimpt S"
immler@69516
  1528
    then have "?rhs" unfolding islimpt_sequential by auto
immler@69516
  1529
  }
immler@69516
  1530
  ultimately show "?rhs"
immler@69516
  1531
    unfolding closure_def by auto
immler@69516
  1532
next
immler@69516
  1533
  assume "?rhs"
immler@69516
  1534
  then show "?lhs" unfolding closure_def islimpt_sequential by auto
immler@69516
  1535
qed
immler@69516
  1536
immler@69516
  1537
lemma closed_sequential_limits:
immler@69516
  1538
  fixes S :: "'a::first_countable_topology set"
immler@69516
  1539
  shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x \<longlongrightarrow> l) sequentially \<longrightarrow> l \<in> S)"
immler@69516
  1540
by (metis closure_sequential closure_subset_eq subset_iff)
immler@69516
  1541
immler@69516
  1542
lemma tendsto_If_within_closures:
immler@69516
  1543
  assumes f: "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
immler@69516
  1544
      (f \<longlongrightarrow> l x) (at x within s \<union> (closure s \<inter> closure t))"
immler@69516
  1545
  assumes g: "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
immler@69516
  1546
      (g \<longlongrightarrow> l x) (at x within t \<union> (closure s \<inter> closure t))"
immler@69516
  1547
  assumes "x \<in> s \<union> t"
immler@69516
  1548
  shows "((\<lambda>x. if x \<in> s then f x else g x) \<longlongrightarrow> l x) (at x within s \<union> t)"
immler@69516
  1549
proof -
immler@69516
  1550
  have *: "(s \<union> t) \<inter> {x. x \<in> s} = s" "(s \<union> t) \<inter> {x. x \<notin> s} = t - s"
immler@69516
  1551
    by auto
immler@69516
  1552
  have "(f \<longlongrightarrow> l x) (at x within s)"
immler@69516
  1553
    by (rule filterlim_at_within_closure_implies_filterlim)
immler@69516
  1554
       (use \<open>x \<in> _\<close> in \<open>auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f]\<close>)
immler@69516
  1555
  moreover
immler@69516
  1556
  have "(g \<longlongrightarrow> l x) (at x within t - s)"
immler@69516
  1557
    by (rule filterlim_at_within_closure_implies_filterlim)
immler@69516
  1558
      (use \<open>x \<in> _\<close> in
immler@69516
  1559
        \<open>auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset\<close>)
immler@69516
  1560
  ultimately show ?thesis
immler@69516
  1561
    by (intro filterlim_at_within_If) (simp_all only: *)
immler@69516
  1562
qed
immler@69516
  1563
immler@69516
  1564
immler@69516
  1565
subsection \<open>Compactness\<close>
immler@69516
  1566
nipkow@69738
  1567
lemma brouwer_compactness_lemma:
nipkow@69738
  1568
  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
nipkow@69738
  1569
  assumes "compact s"
nipkow@69738
  1570
    and "continuous_on s f"
nipkow@69738
  1571
    and "\<not> (\<exists>x\<in>s. f x = 0)"
nipkow@69738
  1572
  obtains d where "0 < d" and "\<forall>x\<in>s. d \<le> norm (f x)"
nipkow@69738
  1573
proof (cases "s = {}")
nipkow@69738
  1574
  case True
nipkow@69738
  1575
  show thesis
nipkow@69738
  1576
    by (rule that [of 1]) (auto simp: True)
nipkow@69738
  1577
next
nipkow@69738
  1578
  case False
nipkow@69738
  1579
  have "continuous_on s (norm \<circ> f)"
nipkow@69738
  1580
    by (rule continuous_intros continuous_on_norm assms(2))+
nipkow@69738
  1581
  with False obtain x where x: "x \<in> s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
nipkow@69738
  1582
    using continuous_attains_inf[OF assms(1), of "norm \<circ> f"]
nipkow@69738
  1583
    unfolding o_def
nipkow@69738
  1584
    by auto
nipkow@69738
  1585
  have "(norm \<circ> f) x > 0"
nipkow@69738
  1586
    using assms(3) and x(1)
nipkow@69738
  1587
    by auto
nipkow@69738
  1588
  then show ?thesis
nipkow@69738
  1589
    by (rule that) (insert x(2), auto simp: o_def)
nipkow@69738
  1590
qed
nipkow@69738
  1591
immler@69516
  1592
subsubsection \<open>Bolzano-Weierstrass property\<close>
immler@69516
  1593
nipkow@69529
  1594
proposition Heine_Borel_imp_Bolzano_Weierstrass:
immler@69516
  1595
  assumes "compact s"
immler@69516
  1596
    and "infinite t"
immler@69516
  1597
    and "t \<subseteq> s"
immler@69516
  1598
  shows "\<exists>x \<in> s. x islimpt t"
immler@69516
  1599
proof (rule ccontr)
immler@69516
  1600
  assume "\<not> (\<exists>x \<in> s. x islimpt t)"
immler@69516
  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)"
immler@69516
  1602
    unfolding islimpt_def
immler@69516
  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)"]
immler@69516
  1604
    by auto
immler@69516
  1605
  obtain g where g: "g \<subseteq> {t. \<exists>x. x \<in> s \<and> t = f x}" "finite g" "s \<subseteq> \<Union>g"
nipkow@69529
  1606
    using assms(1)[unfolded compact_eq_Heine_Borel, THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]]
immler@69516
  1607
    using f by auto
immler@69516
  1608
  from g(1,3) have g':"\<forall>x\<in>g. \<exists>xa \<in> s. x = f xa"
immler@69516
  1609
    by auto
immler@69516
  1610
  {
immler@69516
  1611
    fix x y
immler@69516
  1612
    assume "x \<in> t" "y \<in> t" "f x = f y"
immler@69516
  1613
    then have "x \<in> f x"  "y \<in> f x \<longrightarrow> y = x"
immler@69516
  1614
      using f[THEN bspec[where x=x]] and \<open>t \<subseteq> s\<close> by auto
immler@69516
  1615
    then have "x = y"
immler@69516
  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>
immler@69516
  1617
      by auto
immler@69516
  1618
  }
immler@69516
  1619
  then have "inj_on f t"
immler@69516
  1620
    unfolding inj_on_def by simp
immler@69516
  1621
  then have "infinite (f ` t)"
immler@69516
  1622
    using assms(2) using finite_imageD by auto
immler@69516
  1623
  moreover
immler@69516
  1624
  {
immler@69516
  1625
    fix x
immler@69516
  1626
    assume "x \<in> t" "f x \<notin> g"
immler@69516
  1627
    from g(3) assms(3) \<open>x \<in> t\<close> obtain h where "h \<in> g" and "x \<in> h"
immler@69516
  1628
      by auto
immler@69516
  1629
    then obtain y where "y \<in> s" "h = f y"
immler@69516
  1630
      using g'[THEN bspec[where x=h]] by auto
immler@69516
  1631
    then have "y = x"
immler@69516
  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>]
immler@69516
  1633
      by auto
immler@69516
  1634
    then have False
immler@69516
  1635
      using \<open>f x \<notin> g\<close> \<open>h \<in> g\<close> unfolding \<open>h = f y\<close>
immler@69516
  1636
      by auto
immler@69516
  1637
  }
immler@69516
  1638
  then have "f ` t \<subseteq> g" by auto
immler@69516
  1639
  ultimately show False
immler@69516
  1640
    using g(2) using finite_subset by auto
immler@69516
  1641
qed
immler@69516
  1642
immler@69516
  1643
lemma sequence_infinite_lemma:
immler@69516
  1644
  fixes f :: "nat \<Rightarrow> 'a::t1_space"
immler@69516
  1645
  assumes "\<forall>n. f n \<noteq> l"
immler@69516
  1646
    and "(f \<longlongrightarrow> l) sequentially"
immler@69516
  1647
  shows "infinite (range f)"
immler@69516
  1648
proof
immler@69516
  1649
  assume "finite (range f)"
immler@69516
  1650
  then have "closed (range f)"
immler@69516
  1651
    by (rule finite_imp_closed)
immler@69516
  1652
  then have "open (- range f)"
immler@69516
  1653
    by (rule open_Compl)
immler@69516
  1654
  from assms(1) have "l \<in> - range f"
immler@69516
  1655
    by auto
immler@69516
  1656
  from assms(2) have "eventually (\<lambda>n. f n \<in> - range f) sequentially"
immler@69516
  1657
    using \<open>open (- range f)\<close> \<open>l \<in> - range f\<close>
immler@69516
  1658
    by (rule topological_tendstoD)
immler@69516
  1659
  then show False
immler@69516
  1660
    unfolding eventually_sequentially
immler@69516
  1661
    by auto
immler@69516
  1662
qed
immler@69516
  1663
nipkow@69529
  1664
lemma Bolzano_Weierstrass_imp_closed:
immler@69516
  1665
  fixes s :: "'a::{first_countable_topology,t2_space} set"
immler@69516
  1666
  assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
immler@69516
  1667
  shows "closed s"
immler@69516
  1668
proof -
immler@69516
  1669
  {
immler@69516
  1670
    fix x l
immler@69516
  1671
    assume as: "\<forall>n::nat. x n \<in> s" "(x \<longlongrightarrow> l) sequentially"
immler@69516
  1672
    then have "l \<in> s"
immler@69516
  1673
    proof (cases "\<forall>n. x n \<noteq> l")
immler@69516
  1674
      case False
immler@69516
  1675
      then show "l\<in>s" using as(1) by auto
immler@69516
  1676
    next
immler@69516
  1677
      case True note cas = this
immler@69516
  1678
      with as(2) have "infinite (range x)"
immler@69516
  1679
        using sequence_infinite_lemma[of x l] by auto
immler@69516
  1680
      then obtain l' where "l'\<in>s" "l' islimpt (range x)"
immler@69516
  1681
        using assms[THEN spec[where x="range x"]] as(1) by auto
immler@69516
  1682
      then show "l\<in>s" using sequence_unique_limpt[of x l l']
immler@69516
  1683
        using as cas by auto
immler@69516
  1684
    qed
immler@69516
  1685
  }
immler@69516
  1686
  then show ?thesis
immler@69516
  1687
    unfolding closed_sequential_limits by fast
immler@69516
  1688
qed
immler@69516
  1689
immler@69544
  1690
lemma closure_insert:
immler@69544
  1691
  fixes x :: "'a::t1_space"
immler@69544
  1692
  shows "closure (insert x s) = insert x (closure s)"
immler@69544
  1693
  apply (rule closure_unique)
immler@69544
  1694
  apply (rule insert_mono [OF closure_subset])
immler@69544
  1695
  apply (rule closed_insert [OF closed_closure])
immler@69544
  1696
  apply (simp add: closure_minimal)
immler@69544
  1697
  done
immler@69544
  1698
immler@69516
  1699
immler@69516
  1700
text\<open>In particular, some common special cases.\<close>
immler@69516
  1701
immler@69516
  1702
lemma compact_Un [intro]:
immler@69516
  1703
  assumes "compact s"
immler@69516
  1704
    and "compact t"
immler@69516
  1705
  shows " compact (s \<union> t)"
immler@69516
  1706
proof (rule compactI)
immler@69516
  1707
  fix f
immler@69516
  1708
  assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
immler@69516
  1709
  from * \<open>compact s\<close> obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
nipkow@69529
  1710
    unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
immler@69516
  1711
  moreover
immler@69516
  1712
  from * \<open>compact t\<close> obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
nipkow@69529
  1713
    unfolding compact_eq_Heine_Borel by (auto elim!: allE[of _ f])
immler@69516
  1714
  ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
immler@69516
  1715
    by (auto intro!: exI[of _ "s' \<union> t'"])
immler@69516
  1716
qed
immler@69516
  1717
immler@69516
  1718
lemma compact_Union [intro]: "finite S \<Longrightarrow> (\<And>T. T \<in> S \<Longrightarrow> compact T) \<Longrightarrow> compact (\<Union>S)"
immler@69516
  1719
  by (induct set: finite) auto
immler@69516
  1720
immler@69516
  1721
lemma compact_UN [intro]:
immler@69516
  1722
  "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
immler@69516
  1723
  by (rule compact_Union) auto
immler@69516
  1724
immler@69516
  1725
lemma closed_Int_compact [intro]:
immler@69516
  1726
  assumes "closed s"
immler@69516
  1727
    and "compact t"
immler@69516
  1728
  shows "compact (s \<inter> t)"
immler@69516
  1729
  using compact_Int_closed [of t s] assms
immler@69516
  1730
  by (simp add: Int_commute)
immler@69516
  1731
immler@69516
  1732
lemma compact_Int [intro]:
immler@69516
  1733
  fixes s t :: "'a :: t2_space set"
immler@69516
  1734
  assumes "compact s"
immler@69516
  1735
    and "compact t"
immler@69516
  1736
  shows "compact (s \<inter> t)"
immler@69516
  1737
  using assms by (intro compact_Int_closed compact_imp_closed)
immler@69516
  1738
immler@69516
  1739
lemma compact_sing [simp]: "compact {a}"
nipkow@69529
  1740
  unfolding compact_eq_Heine_Borel by auto
immler@69516
  1741
immler@69516
  1742
lemma compact_insert [simp]:
immler@69516
  1743
  assumes "compact s"
immler@69516
  1744
  shows "compact (insert x s)"
immler@69516
  1745
proof -
immler@69516
  1746
  have "compact ({x} \<union> s)"
immler@69516
  1747
    using compact_sing assms by (rule compact_Un)
immler@69516
  1748
  then show ?thesis by simp
immler@69516
  1749
qed
immler@69516
  1750
immler@69516
  1751
lemma finite_imp_compact: "finite s \<Longrightarrow> compact s"
immler@69516
  1752
  by (induct set: finite) simp_all
immler@69516
  1753
immler@69516
  1754
lemma open_delete:
immler@69516
  1755
  fixes s :: "'a::t1_space set"
immler@69516
  1756
  shows "open s \<Longrightarrow> open (s - {x})"
immler@69516
  1757
  by (simp add: open_Diff)
immler@69516
  1758
immler@69516
  1759
immler@69516
  1760
text\<open>Compactness expressed with filters\<close>
immler@69516
  1761
immler@69516
  1762
lemma closure_iff_nhds_not_empty:
immler@69516
  1763
  "x \<in> closure X \<longleftrightarrow> (\<forall>A. \<forall>S\<subseteq>A. open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {})"
immler@69516
  1764
proof safe
immler@69516
  1765
  assume x: "x \<in> closure X"
immler@69516
  1766
  fix S A
immler@69516
  1767
  assume "open S" "x \<in> S" "X \<inter> A = {}" "S \<subseteq> A"
immler@69516
  1768
  then have "x \<notin> closure (-S)"
immler@69516
  1769
    by (auto simp: closure_complement subset_eq[symmetric] intro: interiorI)
immler@69516
  1770
  with x have "x \<in> closure X - closure (-S)"
immler@69516
  1771
    by auto
immler@69516
  1772
  also have "\<dots> \<subseteq> closure (X \<inter> S)"
immler@69516
  1773
    using \<open>open S\<close> open_Int_closure_subset[of S X] by (simp add: closed_Compl ac_simps)
immler@69516
  1774
  finally have "X \<inter> S \<noteq> {}" by auto
immler@69516
  1775
  then show False using \<open>X \<inter> A = {}\<close> \<open>S \<subseteq> A\<close> by auto
immler@69516
  1776
next
immler@69516
  1777
  assume "\<forall>A S. S \<subseteq> A \<longrightarrow> open S \<longrightarrow> x \<in> S \<longrightarrow> X \<inter> A \<noteq> {}"
immler@69516
  1778
  from this[THEN spec, of "- X", THEN spec, of "- closure X"]
immler@69516
  1779
  show "x \<in> closure X"
immler@69516
  1780
    by (simp add: closure_subset open_Compl)
immler@69516
  1781
qed
immler@69516
  1782
immler@69516
  1783
lemma compact_filter:
immler@69516
  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))"
immler@69516
  1785
proof (intro allI iffI impI compact_fip[THEN iffD2] notI)
immler@69516
  1786
  fix F
immler@69516
  1787
  assume "compact U"
immler@69516
  1788
  assume F: "F \<noteq> bot" "eventually (\<lambda>x. x \<in> U) F"
immler@69516
  1789
  then have "U \<noteq> {}"
immler@69516
  1790
    by (auto simp: eventually_False)
immler@69516
  1791
immler@69516
  1792
  define Z where "Z = closure ` {A. eventually (\<lambda>x. x \<in> A) F}"
immler@69516
  1793
  then have "\<forall>z\<in>Z. closed z"
immler@69516
  1794
    by auto
immler@69516
  1795
  moreover
immler@69516
  1796
  have ev_Z: "\<And>z. z \<in> Z \<Longrightarrow> eventually (\<lambda>x. x \<in> z) F"
lp15@69712
  1797
    unfolding Z_def by (auto elim: eventually_mono intro: subsetD[OF closure_subset])
immler@69516
  1798
  have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
immler@69516
  1799
  proof (intro allI impI)
immler@69516
  1800
    fix B assume "finite B" "B \<subseteq> Z"
immler@69516
  1801
    with \<open>finite B\<close> ev_Z F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
immler@69516
  1802
      by (auto simp: eventually_ball_finite_distrib eventually_conj_iff)
immler@69516
  1803
    with F show "U \<inter> \<Inter>B \<noteq> {}"
immler@69516
  1804
      by (intro notI) (simp add: eventually_False)
immler@69516
  1805
  qed
immler@69516
  1806
  ultimately have "U \<inter> \<Inter>Z \<noteq> {}"
immler@69516
  1807
    using \<open>compact U\<close> unfolding compact_fip by blast
immler@69516
  1808
  then obtain x where "x \<in> U" and x: "\<And>z. z \<in> Z \<Longrightarrow> x \<in> z"
immler@69516
  1809
    by auto
immler@69516
  1810
immler@69516
  1811
  have "\<And>P. eventually P (inf (nhds x) F) \<Longrightarrow> P \<noteq> bot"
immler@69516
  1812
    unfolding eventually_inf eventually_nhds
immler@69516
  1813
  proof safe
immler@69516
  1814
    fix P Q R S
immler@69516
  1815
    assume "eventually R F" "open S" "x \<in> S"
immler@69516
  1816
    with open_Int_closure_eq_empty[of S "{x. R x}"] x[of "closure {x. R x}"]
immler@69516
  1817
    have "S \<inter> {x. R x} \<noteq> {}" by (auto simp: Z_def)
immler@69516
  1818
    moreover assume "Ball S Q" "\<forall>x. Q x \<and> R x \<longrightarrow> bot x"
immler@69516
  1819
    ultimately show False by (auto simp: set_eq_iff)
immler@69516
  1820
  qed
immler@69516
  1821
  with \<open>x \<in> U\<close> show "\<exists>x\<in>U. inf (nhds x) F \<noteq> bot"
immler@69516
  1822
    by (metis eventually_bot)
immler@69516
  1823
next
immler@69516
  1824
  fix A
immler@69516
  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 = {}"
immler@69516
  1826
  define F where "F = (INF a\<in>insert U A. principal a)"
immler@69516
  1827
  have "F \<noteq> bot"
immler@69516
  1828
    unfolding F_def
immler@69516
  1829
  proof (rule INF_filter_not_bot)
immler@69516
  1830
    fix X
immler@69516
  1831
    assume X: "X \<subseteq> insert U A" "finite X"
immler@69516
  1832
    with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
immler@69516
  1833
      by auto
immler@69516
  1834
    with X show "(INF a\<in>X. principal a) \<noteq> bot"
immler@69516
  1835
      by (auto simp: INF_principal_finite principal_eq_bot_iff)
immler@69516
  1836
  qed
immler@69516
  1837
  moreover
immler@69516
  1838
  have "F \<le> principal U"
immler@69516
  1839
    unfolding F_def by auto
immler@69516
  1840
  then have "eventually (\<lambda>x. x \<in> U) F"
immler@69516
  1841
    by (auto simp: le_filter_def eventually_principal)
immler@69516
  1842
  moreover
immler@69516
  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)"
immler@69516
  1844
  ultimately obtain x where "x \<in> U" and x: "inf (nhds x) F \<noteq> bot"
immler@69516
  1845
    by auto
immler@69516
  1846
immler@69516
  1847
  { fix V assume "V \<in> A"
immler@69516
  1848
    then have "F \<le> principal V"
immler@69516
  1849
      unfolding F_def by (intro INF_lower2[of V]) auto
immler@69516
  1850
    then have V: "eventually (\<lambda>x. x \<in> V) F"
immler@69516
  1851
      by (auto simp: le_filter_def eventually_principal)
immler@69516
  1852
    have "x \<in> closure V"
immler@69516
  1853
      unfolding closure_iff_nhds_not_empty
immler@69516
  1854
    proof (intro impI allI)
immler@69516
  1855
      fix S A
immler@69516
  1856
      assume "open S" "x \<in> S" "S \<subseteq> A"
immler@69516
  1857
      then have "eventually (\<lambda>x. x \<in> A) (nhds x)"
immler@69516
  1858
        by (auto simp: eventually_nhds)
immler@69516
  1859
      with V have "eventually (\<lambda>x. x \<in> V \<inter> A) (inf (nhds x) F)"
immler@69516
  1860
        by (auto simp: eventually_inf)
immler@69516
  1861
      with x show "V \<inter> A \<noteq> {}"
immler@69516
  1862
        by (auto simp del: Int_iff simp add: trivial_limit_def)
immler@69516
  1863
    qed
immler@69516
  1864
    then have "x \<in> V"
immler@69516
  1865
      using \<open>V \<in> A\<close> A(1) by simp
immler@69516
  1866
  }
immler@69516
  1867
  with \<open>x\<in>U\<close> have "x \<in> U \<inter> \<Inter>A" by auto
immler@69516
  1868
  with \<open>U \<inter> \<Inter>A = {}\<close> show False by auto
immler@69516
  1869
qed
immler@69516
  1870
nipkow@69564
  1871
definition%important countably_compact :: "('a::topological_space) set \<Rightarrow> bool" where
nipkow@69564
  1872
"countably_compact U \<longleftrightarrow>
nipkow@69564
  1873
  (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A
nipkow@69564
  1874
     \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))"
immler@69516
  1875
immler@69516
  1876
lemma countably_compactE:
immler@69516
  1877
  assumes "countably_compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C" "countable C"
immler@69516
  1878
  obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'"
immler@69516
  1879
  using assms unfolding countably_compact_def by metis
immler@69516
  1880
immler@69516
  1881
lemma countably_compactI:
immler@69516
  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')"
immler@69516
  1883
  shows "countably_compact s"
immler@69516
  1884
  using assms unfolding countably_compact_def by metis
immler@69516
  1885
immler@69516
  1886
lemma compact_imp_countably_compact: "compact U \<Longrightarrow> countably_compact U"
nipkow@69529
  1887
  by (auto simp: compact_eq_Heine_Borel countably_compact_def)
immler@69516
  1888
immler@69516
  1889
lemma countably_compact_imp_compact:
immler@69516
  1890
  assumes "countably_compact U"
immler@69516
  1891
    and ccover: "countable B" "\<forall>b\<in>B. open b"
immler@69516
  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"
immler@69516
  1893
  shows "compact U"
immler@69516
  1894
  using \<open>countably_compact U\<close>
nipkow@69529
  1895
  unfolding compact_eq_Heine_Borel countably_compact_def
immler@69516
  1896
proof safe
immler@69516
  1897
  fix A
immler@69516
  1898
  assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
immler@69516
  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)"
immler@69516
  1900
  moreover define C where "C = {b\<in>B. \<exists>a\<in>A. b \<inter> U \<subseteq> a}"
immler@69516
  1901
  ultimately have "countable C" "\<forall>a\<in>C. open a"
immler@69516
  1902
    unfolding C_def using ccover by auto
immler@69516
  1903
  moreover
immler@69516
  1904
  have "\<Union>A \<inter> U \<subseteq> \<Union>C"
immler@69516
  1905
  proof safe
immler@69516
  1906
    fix x a
immler@69516
  1907
    assume "x \<in> U" "x \<in> a" "a \<in> A"
immler@69516
  1908
    with basis[of a x] A obtain b where "b \<in> B" "x \<in> b" "b \<inter> U \<subseteq> a"
immler@69516
  1909
      by blast
immler@69516
  1910
    with \<open>a \<in> A\<close> show "x \<in> \<Union>C"
immler@69516
  1911
      unfolding C_def by auto
immler@69516
  1912
  qed
immler@69516
  1913
  then have "U \<subseteq> \<Union>C" using \<open>U \<subseteq> \<Union>A\<close> by auto
immler@69516
  1914
  ultimately obtain T where T: "T\<subseteq>C" "finite T" "U \<subseteq> \<Union>T"
immler@69516
  1915
    using * by metis
immler@69516
  1916
  then have "\<forall>t\<in>T. \<exists>a\<in>A. t \<inter> U \<subseteq> a"
immler@69516
  1917
    by (auto simp: C_def)
immler@69516
  1918
  then obtain f where "\<forall>t\<in>T. f t \<in> A \<and> t \<inter> U \<subseteq> f t"
immler@69516
  1919
    unfolding bchoice_iff Bex_def ..
immler@69516
  1920
  with T show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
immler@69516
  1921
    unfolding C_def by (intro exI[of _ "f`T"]) fastforce
immler@69516
  1922
qed
immler@69516
  1923
immler@69516
  1924
proposition countably_compact_imp_compact_second_countable:
immler@69516
  1925
  "countably_compact U \<Longrightarrow> compact (U :: 'a :: second_countable_topology set)"
immler@69516
  1926
proof (rule countably_compact_imp_compact)
immler@69516
  1927
  fix T and x :: 'a
immler@69516
  1928
  assume "open T" "x \<in> T"
immler@69516
  1929
  from topological_basisE[OF is_basis this] obtain b where
immler@69516
  1930
    "b \<in> (SOME B. countable B \<and> topological_basis B)" "x \<in> b" "b \<subseteq> T" .
immler@69516
  1931
  then show "\<exists>b\<in>SOME B. countable B \<and> topological_basis B. x \<in> b \<and> b \<inter> U \<subseteq> T"
immler@69516
  1932
    by blast
immler@69516
  1933
qed (insert countable_basis topological_basis_open[OF is_basis], auto)
immler@69516
  1934
immler@69516
  1935
lemma countably_compact_eq_compact:
immler@69516
  1936
  "countably_compact U \<longleftrightarrow> compact (U :: 'a :: second_countable_topology set)"
immler@69516
  1937
  using countably_compact_imp_compact_second_countable compact_imp_countably_compact by blast
immler@69516
  1938
immler@69516
  1939
subsubsection\<open>Sequential compactness\<close>
immler@69516
  1940
nipkow@69564
  1941
definition%important seq_compact :: "'a::topological_space set \<Rightarrow> bool" where
nipkow@69564
  1942
"seq_compact S \<longleftrightarrow>
nipkow@69564
  1943
  (\<forall>f. (\<forall>n. f n \<in> S)
nipkow@69564
  1944
    \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
immler@69516
  1945
immler@69516
  1946
lemma seq_compactI:
immler@69516
  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"
immler@69516
  1948
  shows "seq_compact S"
immler@69516
  1949
  unfolding seq_compact_def using assms by fast
immler@69516
  1950
immler@69516
  1951
lemma seq_compactE:
immler@69516
  1952
  assumes "seq_compact S" "\<forall>n. f n \<in> S"
immler@69516
  1953
  obtains l r where "l \<in> S" "strict_mono (r :: nat \<Rightarrow> nat)" "((f \<circ> r) \<longlongrightarrow> l) sequentially"
immler@69516
  1954
  using assms unfolding seq_compact_def by fast
immler@69516
  1955
immler@69516
  1956
lemma closed_sequentially: (* TODO: move upwards *)
immler@69516
  1957
  assumes "closed s" and "\<forall>n. f n \<in> s" and "f \<longlonglongrightarrow> l"
immler@69516
  1958
  shows "l \<in> s"
immler@69516
  1959
proof (rule ccontr)
immler@69516
  1960
  assume "l \<notin> s"
immler@69516
  1961
  with \<open>closed s\<close> and \<open>f \<longlonglongrightarrow> l\<close> have "eventually (\<lambda>n. f n \<in> - s) sequentially"
immler@69516
  1962
    by (fast intro: topological_tendstoD)
immler@69516
  1963
  with \<open>\<forall>n. f n \<in> s\<close> show "False"
immler@69516
  1964
    by simp
immler@69516
  1965
qed
immler@69516
  1966
immler@69516
  1967
lemma seq_compact_Int_closed:
immler@69516
  1968
  assumes "seq_compact s" and "closed t"
immler@69516
  1969
  shows "seq_compact (s \<inter> t)"
immler@69516
  1970
proof (rule seq_compactI)
immler@69516
  1971
  fix f assume "\<forall>n::nat. f n \<in> s \<inter> t"
immler@69516
  1972
  hence "\<forall>n. f n \<in> s" and "\<forall>n. f n \<in> t"
immler@69516
  1973
    by simp_all
immler@69516
  1974
  from \<open>seq_compact s\<close> and \<open>\<forall>n. f n \<in> s\<close>
immler@69516
  1975
  obtain l r where "l \<in> s" and r: "strict_mono r" and l: "(f \<circ> r) \<longlonglongrightarrow> l"
immler@69516
  1976
    by (rule seq_compactE)
immler@69516
  1977
  from \<open>\<forall>n. f n \<in> t\<close> have "\<forall>n. (f \<circ> r) n \<in> t"
immler@69516
  1978
    by simp
immler@69516
  1979
  from \<open>closed t\<close> and this and l have "l \<in> t"
immler@69516
  1980
    by (rule closed_sequentially)
immler@69516
  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"
immler@69516
  1982
    by fast
immler@69516
  1983
qed
immler@69516
  1984
immler@69516
  1985
lemma seq_compact_closed_subset:
immler@69516
  1986
  assumes "closed s" and "s \<subseteq> t" and "seq_compact t"
immler@69516
  1987
  shows "seq_compact s"
immler@69516
  1988
  using assms seq_compact_Int_closed [of t s] by (simp add: Int_absorb1)
immler@69516
  1989
immler@69516
  1990
lemma seq_compact_imp_countably_compact:
immler@69516
  1991
  fixes U :: "'a :: first_countable_topology set"
immler@69516
  1992
  assumes "seq_compact U"
immler@69516
  1993
  shows "countably_compact U"
immler@69516
  1994
proof (safe intro!: countably_compactI)
immler@69516
  1995
  fix A
immler@69516
  1996
  assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
immler@69516
  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"
immler@69516
  1998
    using \<open>seq_compact U\<close> by (fastforce simp: seq_compact_def subset_eq)
immler@69516
  1999
  show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
immler@69516
  2000
  proof cases
immler@69516
  2001
    assume "finite A"
immler@69516
  2002
    with A show ?thesis by auto
immler@69516
  2003
  next
immler@69516
  2004
    assume "infinite A"
immler@69516
  2005
    then have "A \<noteq> {}" by auto
immler@69516
  2006
    show ?thesis
immler@69516
  2007
    proof (rule ccontr)
immler@69516
  2008
      assume "\<not> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T)"
immler@69516
  2009
      then have "\<forall>T. \<exists>x. T \<subseteq> A \<and> finite T \<longrightarrow> (x \<in> U - \<Union>T)"
immler@69516
  2010
        by auto
immler@69516
  2011
      then obtain X' where T: "\<And>T. T \<subseteq> A \<Longrightarrow> finite T \<Longrightarrow> X' T \<in> U - \<Union>T"
immler@69516
  2012
        by metis
immler@69516
  2013
      define X where "X n = X' (from_nat_into A ` {.. n})" for n
immler@69516
  2014
      have X: "\<And>n. X n \<in> U - (\<Union>i\<le>n. from_nat_into A i)"
immler@69516
  2015
        using \<open>A \<noteq> {}\<close> unfolding X_def by (intro T) (auto intro: from_nat_into)
immler@69516
  2016
      then have "range X \<subseteq> U"
immler@69516
  2017
        by auto
immler@69516
  2018
      with subseq[of X] obtain r x where "x \<in> U" and r: "strict_mono r" "(X \<circ> r) \<longlonglongrightarrow> x"
immler@69516
  2019
        by auto
immler@69516
  2020
      from \<open>x\<in>U\<close> \<open>U \<subseteq> \<Union>A\<close> from_nat_into_surj[OF \<open>countable A\<close>]
immler@69516
  2021
      obtain n where "x \<in> from_nat_into A n" by auto
immler@69516
  2022
      with r(2) A(1) from_nat_into[OF \<open>A \<noteq> {}\<close>, of n]
immler@69516
  2023
      have "eventually (\<lambda>i. X (r i) \<in> from_nat_into A n) sequentially"
immler@69516
  2024
        unfolding tendsto_def by (auto simp: comp_def)
immler@69516
  2025
      then obtain N where "\<And>i. N \<le> i \<Longrightarrow> X (r i) \<in> from_nat_into A n"
immler@69516
  2026
        by (auto simp: eventually_sequentially)
immler@69516
  2027
      moreover from X have "\<And>i. n \<le> r i \<Longrightarrow> X (r i) \<notin> from_nat_into A n"
immler@69516
  2028
        by auto
immler@69516
  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"
immler@69516
  2030
        by (auto intro!: exI[of _ "max n N"])
immler@69516
  2031
      ultimately show False
immler@69516
  2032
        by auto
immler@69516
  2033
    qed
immler@69516
  2034
  qed
immler@69516
  2035
qed
immler@69516
  2036
immler@69516
  2037
lemma compact_imp_seq_compact:
immler@69516
  2038
  fixes U :: "'a :: first_countable_topology set"
immler@69516
  2039
  assumes "compact U"
immler@69516
  2040
  shows "seq_compact U"
immler@69516
  2041
  unfolding seq_compact_def
immler@69516
  2042
proof safe
immler@69516
  2043
  fix X :: "nat \<Rightarrow> 'a"
immler@69516
  2044
  assume "\<forall>n. X n \<in> U"
immler@69516
  2045
  then have "eventually (\<lambda>x. x \<in> U) (filtermap X sequentially)"
immler@69516
  2046
    by (auto simp: eventually_filtermap)
immler@69516
  2047
  moreover
immler@69516
  2048
  have "filtermap X sequentially \<noteq> bot"
immler@69516
  2049
    by (simp add: trivial_limit_def eventually_filtermap)
immler@69516
  2050
  ultimately
immler@69516
  2051
  obtain x where "x \<in> U" and x: "inf (nhds x) (filtermap X sequentially) \<noteq> bot" (is "?F \<noteq> _")
immler@69516
  2052
    using \<open>compact U\<close> by (auto simp: compact_filter)
immler@69516
  2053
immler@69516
  2054
  from countable_basis_at_decseq[of x]
immler@69516
  2055
  obtain A where A:
immler@69516
  2056
      "\<And>i. open (A i)"
immler@69516
  2057
      "\<And>i. x \<in> A i"
immler@69516
  2058
      "\<And>S. open S \<Longrightarrow> x \<in> S \<Longrightarrow> eventually (\<lambda>i. A i \<subseteq> S) sequentially"
immler@69516
  2059
    by blast
immler@69516
  2060
  define s where "s n i = (SOME j. i < j \<and> X j \<in> A (Suc n))" for n i
immler@69516
  2061
  {
immler@69516
  2062
    fix n i
immler@69516
  2063
    have "\<exists>a. i < a \<and> X a \<in> A (Suc n)"
immler@69516
  2064
    proof (rule ccontr)
immler@69516
  2065
      assume "\<not> (\<exists>a>i. X a \<in> A (Suc n))"
immler@69516
  2066
      then have "\<And>a. Suc i \<le> a \<Longrightarrow> X a \<notin> A (Suc n)"
immler@69516
  2067
        by auto
immler@69516
  2068
      then have "eventually (\<lambda>x. x \<notin> A (Suc n)) (filtermap X sequentially)"
immler@69516
  2069
        by (auto simp: eventually_filtermap eventually_sequentially)
immler@69516
  2070
      moreover have "eventually (\<lambda>x. x \<in> A (Suc n)) (nhds x)"
immler@69516
  2071
        using A(1,2)[of "Suc n"] by (auto simp: eventually_nhds)
immler@69516
  2072
      ultimately have "eventually (\<lambda>x. False) ?F"
immler@69516
  2073
        by (auto simp: eventually_inf)
immler@69516
  2074
      with x show False
immler@69516
  2075
        by (simp add: eventually_False)
immler@69516
  2076
    qed
immler@69516
  2077
    then have "i < s n i" "X (s n i) \<in> A (Suc n)"
immler@69516
  2078
      unfolding s_def by (auto intro: someI2_ex)
immler@69516
  2079
  }
immler@69516
  2080
  note s = this
immler@69516
  2081
  define r where "r = rec_nat (s 0 0) s"
immler@69516
  2082
  have "strict_mono r"
immler@69516
  2083
    by (auto simp: r_def s strict_mono_Suc_iff)
immler@69516
  2084
  moreover
immler@69516
  2085
  have "(\<lambda>n. X (r n)) \<longlonglongrightarrow> x"
immler@69516
  2086
  proof (rule topological_tendstoI)
immler@69516
  2087
    fix S
immler@69516
  2088
    assume "open S" "x \<in> S"
immler@69516
  2089
    with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially"
immler@69516
  2090
      by auto
immler@69516
  2091
    moreover
immler@69516
  2092
    {
immler@69516
  2093
      fix i
immler@69516
  2094
      assume "Suc 0 \<le> i"
immler@69516
  2095
      then have "X (r i) \<in> A i"
immler@69516
  2096
        by (cases i) (simp_all add: r_def s)
immler@69516
  2097
    }
immler@69516
  2098
    then have "eventually (\<lambda>i. X (r i) \<in> A i) sequentially"
immler@69516
  2099
      by (auto simp: eventually_sequentially)
immler@69516
  2100
    ultimately show "eventually (\<lambda>i. X (r i) \<in> S) sequentially"
immler@69516
  2101
      by eventually_elim auto
immler@69516
  2102
  qed
immler@69516
  2103
  ultimately show "\<exists>x \<in> U. \<exists>r. strict_mono r \<and> (X \<circ> r) \<longlonglongrightarrow> x"
immler@69516
  2104
    using \<open>x \<in> U\<close> by (auto simp: convergent_def comp_def)
immler@69516
  2105
qed
immler@69516
  2106
immler@69516
  2107
lemma countably_compact_imp_acc_point:
immler@69516
  2108
  assumes "countably_compact s"
immler@69516
  2109
    and "countable t"
immler@69516
  2110
    and "infinite t"
immler@69516
  2111
    and "t \<subseteq> s"
immler@69516
  2112
  shows "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t)"
immler@69516
  2113
proof (rule ccontr)
immler@69516
  2114
  define C where "C = (\<lambda>F. interior (F \<union> (- t))) ` {F. finite F \<and> F \<subseteq> t }"
immler@69516
  2115
  note \<open>countably_compact s\<close>
immler@69516
  2116
  moreover have "\<forall>t\<in>C. open t"
immler@69516
  2117
    by (auto simp: C_def)
immler@69516
  2118
  moreover
immler@69516
  2119
  assume "\<not> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t))"
immler@69516
  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
immler@69516
  2121
  have "s \<subseteq> \<Union>C"
immler@69516
  2122
    using \<open>t \<subseteq> s\<close>
immler@69516
  2123
    unfolding C_def
immler@69516
  2124
    apply (safe dest!: s)
immler@69516
  2125
    apply (rule_tac a="U \<inter> t" in UN_I)
immler@69516
  2126
    apply (auto intro!: interiorI simp add: finite_subset)
immler@69516
  2127
    done
immler@69516
  2128
  moreover
immler@69516
  2129
  from \<open>countable t\<close> have "countable C"
immler@69516
  2130
    unfolding C_def by (auto intro: countable_Collect_finite_subset)
immler@69516
  2131
  ultimately
immler@69516
  2132
  obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> \<Union>D"
immler@69516
  2133
    by (rule countably_compactE)
immler@69516
  2134
  then obtain E where E: "E \<subseteq> {F. finite F \<and> F \<subseteq> t }" "finite E"
immler@69516
  2135
    and s: "s \<subseteq> (\<Union>F\<in>E. interior (F \<union> (- t)))"
immler@69516
  2136
    by (metis (lifting) finite_subset_image C_def)
immler@69516
  2137
  from s \<open>t \<subseteq> s\<close> have "t \<subseteq> \<Union>E"
immler@69516
  2138
    using interior_subset by blast
immler@69516
  2139
  moreover have "finite (\<Union>E)"
immler@69516
  2140
    using E by auto
immler@69516
  2141
  ultimately show False using \<open>infinite t\<close>
immler@69516
  2142
    by (auto simp: finite_subset)
immler@69516
  2143
qed
immler@69516
  2144
immler@69516
  2145
lemma countable_acc_point_imp_seq_compact:
immler@69516
  2146
  fixes s :: "'a::first_countable_topology set"
immler@69516
  2147
  assumes "\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s \<longrightarrow>
immler@69516
  2148
    (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t))"
immler@69516
  2149
  shows "seq_compact s"
immler@69516
  2150
proof -
immler@69516
  2151
  {
immler@69516
  2152
    fix f :: "nat \<Rightarrow> 'a"
immler@69516
  2153
    assume f: "\<forall>n. f n \<in> s"
immler@69516
  2154
    have "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
immler@69516
  2155
    proof (cases "finite (range f)")
immler@69516
  2156
      case True
immler@69516
  2157
      obtain l where "infinite {n. f n = f l}"
immler@69516
  2158
        using pigeonhole_infinite[OF _ True] by auto
immler@69516
  2159
      then obtain r :: "nat \<Rightarrow> nat" where "strict_mono  r" and fr: "\<forall>n. f (r n) = f l"
immler@69516
  2160
        using infinite_enumerate by blast
immler@69516
  2161
      then have "strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> f l"
immler@69516
  2162
        by (simp add: fr o_def)
immler@69516
  2163
      with f show "\<exists>l\<in>s. \<exists>r. strict_mono  r \<and> (f \<circ> r) \<longlonglongrightarrow> l"
immler@69516
  2164
        by auto
immler@69516
  2165
    next
immler@69516
  2166
      case False
immler@69516
  2167
      with f assms have "\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)"
immler@69516
  2168
        by auto
immler@69516
  2169
      then obtain l where "l \<in> s" "\<forall>U. l\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> range f)" ..
immler@69516
  2170
      from this(2) have "\<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
immler@69516
  2171
        using acc_point_range_imp_convergent_subsequence[of l f] by auto
immler@69516
  2172
      with \<open>l \<in> s\<close> show "\<exists>l\<in>s. \<exists>r. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially" ..
immler@69516
  2173
    qed
immler@69516
  2174
  }
immler@69516
  2175
  then show ?thesis
immler@69516
  2176
    unfolding seq_compact_def by auto
immler@69516
  2177
qed
immler@69516
  2178
immler@69516
  2179
lemma seq_compact_eq_countably_compact:
immler@69516
  2180
  fixes U :: "'a :: first_countable_topology set"
immler@69516
  2181
  shows "seq_compact U \<longleftrightarrow> countably_compact U"
immler@69516
  2182
  using
immler@69516
  2183
    countable_acc_point_imp_seq_compact
immler@69516
  2184
    countably_compact_imp_acc_point
immler@69516
  2185
    seq_compact_imp_countably_compact
immler@69516
  2186
  by metis
immler@69516
  2187
immler@69516
  2188
lemma seq_compact_eq_acc_point:
immler@69516
  2189
  fixes s :: "'a :: first_countable_topology set"
immler@69516
  2190
  shows "seq_compact s \<longleftrightarrow>
immler@69516
  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)))"
immler@69516
  2192
  using
immler@69516
  2193
    countable_acc_point_imp_seq_compact[of s]
immler@69516
  2194
    countably_compact_imp_acc_point[of s]
immler@69516
  2195
    seq_compact_imp_countably_compact[of s]
immler@69516
  2196
  by metis
immler@69516
  2197
immler@69516
  2198
lemma seq_compact_eq_compact:
immler@69516
  2199
  fixes U :: "'a :: second_countable_topology set"
immler@69516
  2200
  shows "seq_compact U \<longleftrightarrow> compact U"
immler@69516
  2201
  using seq_compact_eq_countably_compact countably_compact_eq_compact by blast
immler@69516
  2202
nipkow@69529
  2203
proposition Bolzano_Weierstrass_imp_seq_compact:
immler@69516
  2204
  fixes s :: "'a::{t1_space, first_countable_topology} set"
immler@69516
  2205
  shows "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t) \<Longrightarrow> seq_compact s"
immler@69516
  2206
  by (rule countable_acc_point_imp_seq_compact) (metis islimpt_eq_acc_point)
immler@69516
  2207