RichterHilbertAxiomGeometry/Topology.ml

   1 (*                (c) Copyright, Bill Richter 2013                           *)
   2 (*          Distributed under the same license as HOL Light                  *)
   3 (*                                                                           *)
   4 (* An ongoing readable.ml port of Multivariate/topology.ml with 3 features:  *)
   5 (* 1) A topological space will be an ordered pair α = (X, L), where L is the *)
   6 (* the set of open sets on X.  topology.ml defines a topological space to be *)
   7 (* just L, and the topspace X is defined as UNIONS L.                        *)
   8 (* 2) Result about Connectiveness, limit points, interior and closure  are   *)
   9 (* first proved for general topological spaces and then specialized to       *)
  10 (* Euclidean space.                                                          *)
  11 (* 3)All general topology theorems using subtopology α u have antecedent     *)
  12 (* u ⊂ topspace α.                                                           *)
  13 (* The math character ━ is used for DIFF.                                    *)
  14 (* This file, together with from_topology.ml, shows that all of              *)
  15 (* Multivariate/topology.ml is either ported/modified here, or else run on   *)
  16 (* top of this file.                                                         *)
  17 (* Thanks to Vince Aravantinos for improving the proofs of OPEN_BALL,        *)
  18 (* CONNECTED_OPEN_IN_EQ, CONNECTED_CLOSED_IN_EQ and INTERIOR_EQ.             *)
  19
  20 needs "RichterHilbertAxiomGeometry/readable.ml";;
  21 needs "Multivariate/determinants.ml";;
  22
  23 ParseAsInfix("∉",(11, "right"));;
  24
  25 let NOTIN = NewDefinition `;
  26   ∀a l. a ∉ l ⇔ ¬(a ∈ l)`;;
  27
  28 let DIFF_UNION = theorem `;
  29   ∀u s t.  u ━ (s ∪ t) = (u ━ s) ∩ (u ━ t)
  30   by set`;;
  31
  32 let DIFF_INTER = theorem `;
  33   ∀u s t.  u ━ (s ∩ t) = (u ━ s) ∪ (u ━ t)
  34   by set`;;
  35
  36 let DIFF_REFL = theorem `;
  37   ∀u t.  t ⊂ u ⇒ u ━ (u ━ t) = t
  38   by set`;;
  39
  40 let DIFF_SUBSET = theorem `;
  41   ∀u s t.  s ⊂ t  ⇒  s ━ u ⊂ t ━ u
  42   by set`;;
  43
  44 let DOUBLE_DIFF_UNION = theorem `;
  45   ∀A s t. A ━ s ━ t = A ━ (s ∪ t)
  46   by set`;;
  47
  48 let SUBSET_COMPLEMENT = theorem `;
  49   ∀s t A.  s ⊂ A  ⇒  (s ⊂ A ━ t ⇔ s ∩ t = ∅)
  50   by set`;;
  51
  52 let COMPLEMENT_DISJOINT = theorem `;
  53   ∀A s t.  s ⊂ A  ⇒  (s ⊂ t ⇔ s ∩ (A ━ t) = ∅)
  54   by set`;;
  55
  56 let COMPLEMENT_DUALITY = theorem `;
  57   ∀A s t. s ⊂ A ∧ t ⊂ A  ⇒  (s = t ⇔ A ━ s = A ━ t)
  58   by set`;;
  59
  60 let COMPLEMENT_DUALITY_UNION = theorem `;
  61   ∀A s t.  s ⊂ A ∧ t ⊂ A ∧ u ⊂ A  ⇒  (s = t ∪ u ⇔ A ━ s = (A ━ t) ∩ (A ━ u))
  62   by set`;;
  63
  64 let SUBSET_DUALITY = theorem `;
  65   ∀s t u.  t ⊂ u  ⇒  s ━ u ⊂ s ━ t
  66   by set`;;
  67
  68 let COMPLEMENT_INTER_DIFF = theorem `;
  69   ∀A s t. s ⊂ A  ⇒  s ━ t = s ∩ (A ━ t)
  70   by set`;;
  71
  72 let INTERS_SUBSET = theorem `;
  73   ∀f t. ¬(f = ∅) ∧ (∀s. s ∈ f ⇒ s ⊂ t)  ⇒  INTERS f ⊂ t
  74   by set`;;
  75
  76 let IN_SET_FUNCTION_PREDICATE = theorem `;
  77   ∀x f P. x ∈ {f y | P y}  ⇔  ∃y. x = f y ∧ P y
  78   by set`;;
  79
  80 let INTER_TENSOR = theorem `;
  81   ∀s s' t t'.  s ⊂ s' ∧ t ⊂ t'  ⇒  s ∩ t ⊂ s' ∩ t'
  82   by set`;;
  83
  84 let UNION_TENSOR = theorem `;
  85   ∀s s' t t'.  s ⊂ s' ∧ t ⊂ t'  ⇒  s ∪ t ⊂ s' ∪ t'
  86   by set`;;
  87
  88 let ExistsTensorInter = theorem `;
  89   ∀F G H.  (∀x y. F x ∧ G y  ⇒ H (x ∩ y))  ⇒
  90     (∃x. F x) ∧ (∃y. G y) ⇒ (∃z. H z)
  91   by fol`;;
  92
  93 let istopology = NewDefinition `;
  94   istopology (X, L)  ⇔
  95   (∀U. U ∈ L  ⇒  U ⊂ X)  ∧  ∅ ∈ L  ∧  X ∈ L  ∧
  96   (∀s t. s ∈ L ∧ t ∈ L  ⇒ s ∩ t ∈ L)  ∧ ∀k. k ⊂ L  ⇒  UNIONS k ∈ L`;;
  97
  98 let UnderlyingSpace = NewDefinition `;
  99   UnderlyingSpace α = FST α`;;
 100
 101 let OpenSets = NewDefinition `;
 102   OpenSets α = SND α`;;
 103
 104 let ExistsTopology = theorem `;
 105   ∀X. ∃α. istopology α  ∧  UnderlyingSpace α = X
 106
 107   proof
 108     intro_TAC ∀X;
 109     consider L such that L = {U | U ⊂ X}     [Lexists] by fol;
 110     exists_TAC (X, L);
 111     rewrite istopology IN_ELIM_THM Lexists UnderlyingSpace;
 112     set;
 113   qed;
 114 `;;
 115
 116 let topology_tybij_th = theorem `;
 117   ∃t. istopology t
 118   by fol ExistsTopology`;;
 119
 120 let topology_tybij =
 121   new_type_definition "topology" ("mk_topology","dest_topology")
 122   topology_tybij_th;;
 123
 124 let ISTOPOLOGYdest_topology = theorem `;
 125   ∀α. istopology (dest_topology α)
 126   by fol topology_tybij`;;
 127
 128 let OpenIn = NewDefinition `;
 129   ∀α. open_in α = OpenSets (dest_topology α)`;;
 130
 131 let topspace = NewDefinition `;
 132   ∀α. topspace α = UnderlyingSpace (dest_topology  α)`;;
 133
 134 let TopologyPAIR = theorem `;
 135   ∀α.  dest_topology α = (topspace α, open_in α)
 136   by rewrite PAIR_EQ OpenIn topspace UnderlyingSpace OpenSets`;;
 137
 138 let Topology_Eq = theorem `;
 139   ∀α β.  topspace α =  topspace β  ∧  (∀U. open_in α U ⇔ open_in β U)
 140     ⇔ α = β
 141
 142   proof
 143     intro_TAC ∀α β;
 144     eq_tac     [Right] by fol;
 145     intro_TAC H1 H2;
 146     dest_topology α = dest_topology β     [] by simplify TopologyPAIR PAIR_EQ H1 H2 FUN_EQ_THM;
 147     fol - topology_tybij;
 148   qed;
 149 `;;
 150
 151 let OpenInCLAUSES = theorem `;
 152   ∀α X. topspace α = X  ⇒
 153     (∀U. open_in α U  ⇒  U ⊂ X)  ∧  open_in α ∅  ∧  open_in α X  ∧
 154     (∀s t. open_in α s ∧ open_in α t  ⇒ open_in α (s ∩ t))  ∧
 155     ∀k. (∀s. s ∈ k ⇒ open_in α s)  ⇒  open_in α (UNIONS k)
 156
 157   proof
 158     intro_TAC ∀α X, H1;
 159     consider L such that L = open_in α     [Ldef] by fol;
 160     istopology (X, L)     [] by fol H1 Ldef TopologyPAIR PAIR_EQ ISTOPOLOGYdest_topology;
 161     fol Ldef - istopology IN SUBSET;
 162   qed;
 163 `;;
 164
 165 let OPEN_IN_SUBSET = theorem `;
 166   ∀α s.  open_in α s  ⇒  s ⊂ topspace α
 167   by fol OpenInCLAUSES`;;
 168
 169 let OPEN_IN_EMPTY = theorem `;
 170   ∀α. open_in α ∅
 171   by fol OpenInCLAUSES`;;
 172
 173 let OPEN_IN_INTER = theorem `;
 174   ∀α s t. open_in α s ∧ open_in α t  ⇒  open_in α (s ∩ t)
 175   by fol OpenInCLAUSES`;;
 176
 177 let OPEN_IN_UNIONS = theorem `;
 178   ∀α k. (∀s. s ∈ k ⇒ open_in α s)  ⇒  open_in α (UNIONS k)
 179   by fol OpenInCLAUSES`;;
 180
 181 let OpenInTopspace = theorem `;
 182   ∀α.  open_in α (topspace α)
 183   by fol OpenInCLAUSES`;;
 184
 185 let OPEN_IN_UNION = theorem `;
 186   ∀α s t. open_in α s ∧ open_in α t  ⇒  open_in α (s ∪ t)
 187
 188   proof
 189     intro_TAC ∀α s t, H;
 190     ∀x. x ∈ {s, t} ⇔ x = s ∨ x = t     [] by fol IN_INSERT NOT_IN_EMPTY;
 191     fol - UNIONS_2 H OPEN_IN_UNIONS;
 192   qed;
 193 `;;
 194
 195 let OPEN_IN_TOPSPACE = theorem `;
 196   ∀α. open_in α (topspace α)
 197   by fol OpenInCLAUSES`;;
 198
 199 let OPEN_IN_INTERS = theorem `;
 200   ∀α s. FINITE s ∧ ¬(s = ∅) ∧ (∀t. t ∈ s  ⇒  open_in α t)
 201     ⇒ open_in α (INTERS s)
 202
 203   proof
 204     intro_TAC ∀α;
 205     rewrite IMP_CONJ;
 206     MATCH_MP_TAC FINITE_INDUCT;
 207     rewrite INTERS_INSERT NOT_INSERT_EMPTY FORALL_IN_INSERT;
 208     intro_TAC ∀x s, H1, xWorks sWorks;
 209     assume ¬(s = ∅)     [Nonempty] by simplify INTERS_0 INTER_UNIV xWorks;
 210     fol xWorks Nonempty H1 sWorks OPEN_IN_INTER;
 211   qed;
 212 `;;
 213
 214 let OPEN_IN_SUBOPEN = theorem `;
 215   ∀α s.  open_in α s ⇔ ∀x. x ∈ s ⇒ ∃t. open_in α t ∧ x ∈ t ∧ t ⊂ s
 216
 217   proof
 218     intro_TAC ∀α s;
 219     eq_tac     [Left] by set;
 220     intro_TAC ALLtExist;
 221     consider f such that
 222     ∀x. x ∈ s  ⇒  open_in α (f x) ∧ x ∈ f x ∧ f x ⊂ s     [fExists] by fol ALLtExist SKOLEM_THM_GEN;
 223     s = UNIONS (IMAGE f s)     [] by set -;
 224     fol - fExists FORALL_IN_IMAGE OPEN_IN_UNIONS;
 225   qed;
 226 `;;
 227
 228 let closed_in = NewDefinition `;
 229   ∀α s.  closed_in α s  ⇔
 230       s ⊂ topspace α ∧ open_in α (topspace α ━ s)`;;
 231
 232 let CLOSED_IN_SUBSET = theorem `;
 233   ∀α s. closed_in α s   ⇒  s ⊂ topspace α
 234   by fol closed_in`;;
 235
 236 let CLOSED_IN_EMPTY = theorem `;
 237   ∀α. closed_in α ∅
 238   by fol closed_in EMPTY_SUBSET DIFF_EMPTY OPEN_IN_TOPSPACE`;;
 239
 240 let CLOSED_IN_TOPSPACE = theorem `;
 241   ∀α. closed_in α (topspace α)
 242   by fol closed_in SUBSET_REFL DIFF_EQ_EMPTY OPEN_IN_EMPTY`;;
 243
 244 let CLOSED_IN_UNION = theorem `;
 245   ∀α s t. closed_in α s ∧ closed_in α t  ⇒  closed_in α (s ∪ t)
 246
 247   proof
 248     intro_TAC ∀α s t, Hst;
 249     fol Hst closed_in DIFF_UNION UNION_SUBSET OPEN_IN_INTER;
 250   qed;
 251 `;;
 252
 253 let CLOSED_IN_INTERS = theorem `;
 254   ∀α k.  ¬(k = ∅) ∧ (∀s. s ∈ k ⇒ closed_in α s)  ⇒  closed_in α (INTERS k)
 255
 256   proof
 257     intro_TAC ∀α k, H1 H2;
 258     consider X such that X = topspace α     [Xdef] by fol;
 259     simplify GSYM Xdef closed_in DIFF_INTERS SIMPLE_IMAGE;
 260     fol H1 H2 Xdef INTERS_SUBSET closed_in FORALL_IN_IMAGE OPEN_IN_UNIONS;
 261   qed;
 262 `;;
 263
 264 let CLOSED_IN_FORALL_IN = theorem `;
 265   ∀α P Q.  ¬(P = ∅) ∧ (∀a. P a ⇒ closed_in α {x | Q a x})  ⇒
 266     closed_in α {x | ∀a. P a ⇒ Q a x}
 267
 268   proof
 269     intro_TAC ∀α P Q, Pnonempty H1;
 270     consider f such that f = {{x | Q a x} | P a}     [fDef] by fol;
 271     ¬(f = ∅)     [fNonempty] by set fDef Pnonempty;
 272     (∀a. P a ⇒ closed_in α {x | Q a x})  ⇔  (∀s. s ∈ f ⇒ closed_in α s)     [] by simplify fDef FORALL_IN_GSPEC;
 273     closed_in α (INTERS f)     [] by fol fNonempty H1 - CLOSED_IN_INTERS;
 274     MP_TAC -;
 275     {x | ∀a. P a ⇒ x ∈ {x | Q a x}} = {x | ∀a. P a ⇒ Q a x}     [] by set;
 276     simplify fDef INTERS_GSPEC -;
 277   qed;
 278 `;;
 279
 280 let CLOSED_IN_INTER = theorem `;
 281   ∀α s t. closed_in α s ∧ closed_in α t ⇒ closed_in α (s ∩ t)
 282
 283   proof
 284     intro_TAC ∀α s t, Hs Ht;
 285     rewrite GSYM INTERS_2;
 286     MATCH_MP_TAC CLOSED_IN_INTERS;
 287     set Hs Ht;
 288   qed;
 289 `;;
 290
 291 let OPEN_IN_CLOSED_IN_EQ = theorem `;
 292   ∀α s. open_in α s  ⇔  s ⊂ topspace α ∧ closed_in α (topspace α ━ s)
 293
 294   proof
 295     intro_TAC ∀α s;
 296     simplify closed_in SUBSET_DIFF OPEN_IN_SUBSET;
 297     fol SET_RULE [X ━ (X ━ s) = X ∩ s  ∧  (s ⊂ X ⇒ X ∩ s = s)] OPEN_IN_SUBSET;
 298   qed;
 299 `;;
 300
 301 let OPEN_IN_CLOSED_IN = theorem `;
 302   ∀s. s ⊂ topspace α
 303     ⇒ (open_in α s ⇔ closed_in α (topspace α ━ s))
 304   by fol OPEN_IN_CLOSED_IN_EQ`;;
 305
 306 let OPEN_IN_DIFF = theorem `;
 307   ∀α s t.  open_in α s ∧ closed_in α t  ⇒  open_in α (s ━ t)
 308
 309   proof
 310     intro_TAC ∀α s t, H1 H2;
 311     consider X such that X = topspace α     [Xdef] by fol;
 312     fol COMPLEMENT_INTER_DIFF OPEN_IN_SUBSET - H1 H2 closed_in OPEN_IN_INTER;
 313   qed;
 314 `;;
 315
 316 let CLOSED_IN_DIFF = theorem `;
 317   ∀α s t.  closed_in α s ∧ open_in α t  ⇒  closed_in α (s ━ t)
 318
 319   proof
 320     intro_TAC ∀α s t, H1 H2;
 321     consider X such that X = topspace α     [Xdef] by fol;
 322     fol COMPLEMENT_INTER_DIFF H1 - OPEN_IN_SUBSET SUBSET_DIFF DIFF_REFL H2 closed_in CLOSED_IN_INTER;
 323   qed;
 324 `;;
 325
 326 let CLOSED_IN_UNIONS = theorem `;
 327   ∀α s.  FINITE s ∧ (∀t. t ∈ s ⇒ closed_in α t)
 328     ⇒ closed_in α (UNIONS s)
 329
 330   proof
 331     intro_TAC ∀α;
 332     rewrite IMP_CONJ;
 333     MATCH_MP_TAC FINITE_INDUCT;
 334     fol UNIONS_INSERT UNIONS_0 CLOSED_IN_EMPTY IN_INSERT CLOSED_IN_UNION;
 335   qed;
 336 `;;
 337
 338 let subtopology = NewDefinition `;
 339   ∀α u.  subtopology α u = mk_topology (u, {s ∩ u | open_in α s})`;;
 340
 341 let IstopologySubtopology = theorem `;
 342   ∀α u:A->bool. u ⊂ topspace α  ⇒  istopology (u, {s ∩ u | open_in α s})
 343
 344   proof
 345     intro_TAC ∀α u, H1;
 346     ∅ = ∅ ∩ u ∧ open_in α ∅     [emptysetOpen] by fol INTER_EMPTY OPEN_IN_EMPTY;
 347     u = topspace α ∩ u ∧ open_in α (topspace α)     [uOpen] by fol OPEN_IN_TOPSPACE H1 INTER_COMM SUBSET_INTER_ABSORPTION;
 348     ∀s' s. open_in α s' ∧ open_in α s  ⇒  open_in α (s' ∩ s)  ∧
 349     (s' ∩ u) ∩ (s ∩ u) = (s' ∩ s) ∩ u     [interOpen]
 350     proof
 351       intro_TAC ∀s' s, H1 H2;
 352       set MESON [H1; H2; OPEN_IN_INTER] [open_in α (s' ∩ s)];
 353     qed;
 354     ∀k. k ⊂ {s | open_in α s}  ⇒  open_in α (UNIONS k)  ∧
 355     UNIONS (IMAGE (λs. s ∩ u) k) = (UNIONS k) ∩ u     [unionsOpen]
 356     proof
 357       intro_TAC ∀k, kProp;
 358       open_in α (UNIONS k)     [] by fol kProp SUBSET IN_ELIM_THM OPEN_IN_UNIONS;
 359       simplify - UNIONS_IMAGE UNIONS_GSPEC INTER_UNIONS;
 360     qed;
 361     {s ∩ u | open_in α s} = IMAGE (λs. s ∩ u) {s | open_in α s}     [] by set;
 362     simplify istopology IN_SET_FUNCTION_PREDICATE LEFT_IMP_EXISTS_THM INTER_SUBSET - FORALL_SUBSET_IMAGE;
 363     fol  emptysetOpen uOpen interOpen unionsOpen;
 364   qed;
 365 `;;
 366
 367 let OpenInSubtopology = theorem `;
 368   ∀α u s. u ⊂ topspace α ⇒
 369     (open_in (subtopology α u) s  ⇔  ∃t. open_in α t ∧ s = t ∩ u)
 370
 371   proof
 372     intro_TAC ∀α u s, H1;
 373     open_in (subtopology α u) = OpenSets (u,{s ∩ u | open_in α s})     [] by fol subtopology H1 IstopologySubtopology topology_tybij OpenIn;
 374     rewrite - OpenSets PAIR_EQ SND EXTENSION IN_ELIM_THM;
 375   qed;
 376 `;;
 377
 378 let TopspaceSubtopology = theorem `;
 379   ∀α u. u ⊂ topspace α  ⇒  topspace (subtopology α u) = u
 380
 381   proof
 382     intro_TAC ∀α u , H1;
 383     topspace (subtopology α u) = UnderlyingSpace (u,{s ∩ u | open_in α s})     [] by fol subtopology H1 IstopologySubtopology topology_tybij topspace;
 384     rewrite - UnderlyingSpace PAIR_EQ FST;
 385     fol  INTER_COMM H1 SUBSET_INTER_ABSORPTION;
 386   qed;
 387 `;;
 388
 389 let OpenInRefl = theorem `;
 390   ∀α s.  s ⊂ topspace α  ⇒  open_in (subtopology α s) s
 391   by fol TopspaceSubtopology OPEN_IN_TOPSPACE`;;
 392
 393 let ClosedInRefl = theorem `;
 394   ∀α s.  s ⊂ topspace α  ⇒  closed_in (subtopology α s) s
 395   by fol TopspaceSubtopology CLOSED_IN_TOPSPACE`;;
 396
 397 let ClosedInSubtopology = theorem `;
 398   ∀α u C.  u ⊂ topspace α  ⇒
 399     (closed_in (subtopology α u) C  ⇔  ∃D. closed_in α D ∧ C = D ∩ u)
 400
 401   proof
 402     intro_TAC ∀α u C, H1;
 403     consider X such that
 404     X = topspace α ∧ u ⊂ X     [Xdef] by fol H1;
 405     closed_in (subtopology α u) C  ⇔
 406     ∃t. C ⊂ u ∧ t ⊂ X ∧ open_in α t ∧ u ━ C = t ∩ u     [] by fol closed_in H1 Xdef OpenInSubtopology OPEN_IN_SUBSET TopspaceSubtopology;
 407     closed_in (subtopology α u) C  ⇔
 408     ∃D. C ⊂ u ∧ D ⊂ X ∧ open_in α (X ━ D) ∧ u ━ C = (X ━ D) ∩ u     []
 409     proof
 410       rewrite -;
 411       eq_tac     [Left]
 412       proof
 413         STRIP_TAC;     exists_TAC X ━ t;
 414         ASM_SIMP_TAC H1 OPEN_IN_SUBSET DIFF_REFL SUBSET_DIFF;
 415       qed;
 416       STRIP_TAC;     exists_TAC X ━ D;
 417       ASM_SIMP_TAC SUBSET_DIFF;
 418     qed;
 419     simplify - GSYM Xdef H1 closed_in;
 420     ∀D C. C ⊂ u ∧ u ━ C = (X ━ D) ∩ u  ⇔  C = D ∩ u     [] by set Xdef DIFF_REFL INTER_SUBSET;
 421     fol -;
 422   qed;
 423 `;;
 424
 425 let OPEN_IN_SUBTOPOLOGY_EMPTY = theorem `;
 426   ∀α s. open_in (subtopology α ∅) s  ⇔  s = ∅
 427
 428   proof
 429     simplify EMPTY_SUBSET OpenInSubtopology INTER_EMPTY;
 430     fol  OPEN_IN_EMPTY;
 431   qed;
 432 `;;
 433
 434 let CLOSED_IN_SUBTOPOLOGY_EMPTY = theorem `;
 435   ∀α s. closed_in (subtopology α ∅) s  ⇔  s = ∅
 436
 437   proof
 438     simplify EMPTY_SUBSET ClosedInSubtopology INTER_EMPTY;
 439     fol  CLOSED_IN_EMPTY;
 440   qed;
 441 `;;
 442
 443 let SUBTOPOLOGY_TOPSPACE = theorem `;
 444   ∀α. subtopology α (topspace α) = α
 445
 446   proof
 447     intro_TAC ∀α;
 448     topspace (subtopology α (topspace α)) = topspace α     [topXsub] by simplify SUBSET_REFL TopspaceSubtopology;
 449     simplify topXsub GSYM Topology_Eq;
 450     fol MESON [SUBSET_REFL] [topspace α ⊂ topspace α] OpenInSubtopology OPEN_IN_SUBSET SUBSET_INTER_ABSORPTION;
 451   qed;
 452 `;;
 453
 454 let OpenInImpSubset = theorem `;
 455   ∀α s t.  s ⊂ topspace α  ⇒
 456     open_in (subtopology α s) t  ⇒  t ⊂ s
 457   by fol OpenInSubtopology INTER_SUBSET`;;
 458
 459 let ClosedInImpSubset = theorem `;
 460   ∀α s t.  s ⊂ topspace α  ⇒
 461     closed_in (subtopology α s) t  ⇒  t ⊂ s
 462   by fol ClosedInSubtopology INTER_SUBSET`;;
 463
 464 let OpenInSubtopologyUnion = theorem `;
 465   ∀α s t u.  t ⊂ topspace α  ∧  u ⊂ topspace α  ⇒
 466     open_in (subtopology α t) s  ∧  open_in (subtopology α u) s
 467     ⇒  open_in (subtopology α (t ∪ u)) s
 468
 469   proof
 470     intro_TAC ∀α s t u, Ht Hu;
 471     simplify Ht Hu Ht Hu UNION_SUBSET OpenInSubtopology;
 472     intro_TAC sOpenSub_t sOpenSub_u;
 473     consider a b such that
 474     open_in α a  ∧  s = a ∩ t  ∧
 475     open_in α b  ∧  s = b ∩ u     [abExist] by fol sOpenSub_t sOpenSub_u;
 476     exists_TAC a ∩ b;
 477     set MESON [abExist; OPEN_IN_INTER] [open_in α (a ∩ b)] abExist;
 478   qed;
 479 `;;
 480
 481 let ClosedInSubtopologyUnion = theorem `;
 482   ∀α s t u.  t ⊂ topspace α  ∧  u ⊂ topspace α  ⇒
 483     closed_in (subtopology α t) s  ∧  closed_in (subtopology α u) s
 484     ⇒  closed_in (subtopology α (t ∪ u)) s
 485
 486   proof
 487     intro_TAC ∀α s t u, Ht Hu;
 488     simplify Ht Hu Ht Hu UNION_SUBSET ClosedInSubtopology;
 489     intro_TAC sClosedSub_t sClosedSub_u;
 490     consider a b such that
 491     closed_in α a  ∧  s = a ∩ t  ∧
 492     closed_in α b  ∧  s = b ∩ u     [abExist] by fol sClosedSub_t sClosedSub_u;
 493     exists_TAC a ∩ b;
 494     set MESON [abExist; CLOSED_IN_INTER] [closed_in α (a ∩ b)] abExist;
 495   qed;
 496 `;;
 497
 498 let OpenInSubtopologyInterOpen = theorem `;
 499   ∀α s t u.  u ⊂ topspace α  ⇒
 500     open_in (subtopology α u) s  ∧  open_in α t
 501     ⇒ open_in (subtopology α u) (s ∩ t)
 502
 503   proof
 504     intro_TAC ∀α s t u, H1, sOpenSub_t tOpen;
 505     consider a b such that
 506     open_in α a  ∧  s = a ∩ u  ∧  b = a ∩ t     [aExists] by fol sOpenSub_t H1 OpenInSubtopology;
 507     fol - tOpen OPEN_IN_INTER INTER_ACI H1 OpenInSubtopology;
 508   qed;
 509 `;;
 510
 511 let OpenInOpenInter = theorem `;
 512   ∀α u s.  u ⊂ topspace α  ⇒ open_in α s
 513     ⇒  open_in (subtopology α u) (u ∩ s)
 514   by fol INTER_COMM OpenInSubtopology`;;
 515
 516 let OpenOpenInTrans = theorem `;
 517   ∀α s t.  open_in α s ∧ open_in α t ∧ t ⊂ s
 518     ⇒ open_in (subtopology α s) t
 519   by fol OPEN_IN_SUBSET SUBSET_INTER_ABSORPTION OpenInSubtopology`;;
 520
 521 let ClosedClosedInTrans = theorem `;
 522   ∀α s t.  closed_in α s ∧ closed_in α t ∧ t ⊂ s
 523     ⇒ closed_in (subtopology α s) t
 524   by fol CLOSED_IN_SUBSET SUBSET_INTER_ABSORPTION ClosedInSubtopology`;;
 525
 526 let OpenSubset = theorem `;
 527   ∀α s t.  t ⊂ topspace α  ⇒
 528     s ⊂ t  ∧  open_in α s ⇒ open_in (subtopology α t) s
 529   by fol OpenInSubtopology SUBSET_INTER_ABSORPTION`;;
 530
 531 let ClosedSubsetEq = theorem `;
 532   ∀α u s.  u ⊂ topspace α  ⇒
 533     closed_in α s  ⇒  (closed_in (subtopology α u) s  ⇔  s ⊂ u)
 534   by fol ClosedInSubtopology INTER_SUBSET SUBSET_INTER_ABSORPTION`;;
 535
 536 let ClosedInInterClosed = theorem `;
 537   ∀α s t u.  u ⊂ topspace α  ⇒
 538         closed_in (subtopology α u) s ∧ closed_in α t
 539         ⇒ closed_in (subtopology α u) (s ∩ t)
 540
 541   proof
 542     intro_TAC ∀α s t u, H1, sClosedSub_t tClosed;
 543     consider a b such that
 544     closed_in α a  ∧  s = a ∩ u  ∧  b = a ∩ t     [aExists] by fol sClosedSub_t H1 ClosedInSubtopology;
 545     fol - tClosed CLOSED_IN_INTER INTER_ACI H1 ClosedInSubtopology;
 546   qed;
 547 `;;
 548
 549 let ClosedInClosedInter = theorem `;
 550   ∀α u s.  u ⊂ topspace α  ⇒
 551     closed_in α s  ⇒  closed_in (subtopology α u) (u ∩ s)
 552   by fol INTER_COMM ClosedInSubtopology`;;
 553
 554 let ClosedSubset = theorem `;
 555   ∀α s t.  t ⊂ topspace α  ⇒
 556     s ⊂ t  ∧  closed_in α s  ⇒  closed_in (subtopology α t) s
 557   by fol ClosedInSubtopology SUBSET_INTER_ABSORPTION`;;
 558
 559 let OpenInSubsetTrans = theorem `;
 560   ∀α s t u.  u ⊂ topspace α  ∧  t ⊂ topspace α  ⇒
 561     open_in (subtopology α u) s  ∧  s ⊂ t  ∧  t ⊂ u
 562     ⇒ open_in (subtopology α t) s
 563
 564   proof
 565     intro_TAC ∀α s t u, uSubset tSubset;
 566     simplify uSubset tSubset OpenInSubtopology;
 567     intro_TAC sOpen_u s_t t_u;
 568     consider a such that
 569     open_in α a  ∧  s = a ∩ u     [aExists] by fol uSubset sOpen_u OpenInSubtopology;
 570     set aExists s_t t_u;
 571   qed;
 572 `;;
 573
 574 let ClosedInSubsetTrans = theorem `;
 575   ∀α s t u.  u ⊂ topspace α  ∧  t ⊂ topspace α  ⇒
 576         closed_in (subtopology α u) s  ∧  s ⊂ t  ∧  t ⊂ u
 577         ⇒ closed_in (subtopology α t) s
 578
 579   proof
 580     intro_TAC ∀α s t u, uSubset tSubset;
 581     simplify uSubset tSubset ClosedInSubtopology;
 582     intro_TAC sClosed_u s_t t_u;
 583     consider a such that
 584     closed_in α a  ∧  s = a ∩ u     [aExists] by fol uSubset sClosed_u ClosedInSubtopology;
 585     set aExists s_t t_u;
 586   qed;
 587 `;;
 588
 589 let OpenInTrans = theorem `;
 590   ∀α s t u.  t ⊂ topspace α  ∧  u ⊂ topspace α  ⇒
 591     open_in (subtopology α t) s   ∧  open_in (subtopology α u) t
 592     ⇒ open_in (subtopology α u) s
 593
 594   proof
 595     intro_TAC ∀α s t u, H1 H2;
 596     simplify H1 H2 OpenInSubtopology;
 597     fol H1 H2 OpenInSubtopology OPEN_IN_INTER INTER_ASSOC;
 598   qed;
 599 `;;
 600
 601 let OpenInTransEq = theorem `;
 602   ∀α s t.  t ⊂ topspace α  ∧  s ⊂ topspace α  ⇒
 603     ((∀u. open_in (subtopology α t) u  ⇒  open_in (subtopology α s) t)
 604     ⇔ open_in (subtopology α s) t)
 605   by fol OpenInTrans OpenInRefl`;;
 606
 607 let OpenInOpenTrans = theorem `;
 608   ∀α u s.  u ⊂ topspace α  ⇒
 609     open_in (subtopology α u) s ∧ open_in α u  ⇒  open_in α s
 610   by fol OpenInSubtopology OPEN_IN_INTER`;;
 611
 612 let OpenInSubtopologyTrans = theorem `;
 613   ∀α s t u.  t ⊂ topspace α  ∧  u ⊂ topspace α  ⇒
 614     open_in (subtopology α t) s  ∧  open_in (subtopology α u) t
 615     ⇒ open_in (subtopology α u) s
 616
 617   proof
 618     simplify OpenInSubtopology;
 619     fol  OPEN_IN_INTER INTER_ASSOC;
 620   qed;
 621 `;;
 622
 623 let SubtopologyOpenInSubopen = theorem `;
 624   ∀α u s.  u ⊂ topspace α ⇒
 625     (open_in (subtopology α u) s  ⇔
 626     s ⊂ u  ∧  ∀x. x ∈ s ⇒ ∃t. open_in α t  ∧  x ∈ t  ∧  t ∩ u ⊂ s)
 627
 628   proof
 629     intro_TAC ∀α u s, H1;
 630     rewriteL OPEN_IN_SUBOPEN;
 631     simplify H1 OpenInSubtopology;
 632     eq_tac     [Right] by fol SUBSET IN_INTER;
 633     intro_TAC H2;
 634     conj_tac     [Left]
 635     proof     simplify SUBSET;     fol H2 IN_INTER;     qed;
 636     intro_TAC ∀x, xs;
 637     consider t such that
 638     open_in α t ∧ x ∈ t ∩ u ∧ t ∩ u ⊂ s     [tExists] by fol H2 xs;
 639     fol  - IN_INTER;
 640   qed;
 641 `;;
 642
 643 let ClosedInSubtopologyTrans = theorem `;
 644   ∀α s t u.  t ⊂ topspace α  ∧  u ⊂ topspace α  ⇒
 645     closed_in (subtopology α t) s  ∧  closed_in (subtopology α u) t
 646     ⇒ closed_in (subtopology α u) s
 647
 648   proof
 649     simplify ClosedInSubtopology;
 650     fol  CLOSED_IN_INTER INTER_ASSOC;
 651   qed;
 652 `;;
 653
 654 let ClosedInSubtopologyTransEq = theorem `;
 655   ∀α s t.  t ⊂ topspace α  ∧  s ⊂ topspace α  ⇒
 656     ((∀u. closed_in (subtopology α t) u  ⇒  closed_in (subtopology α s) t)
 657     ⇔ closed_in (subtopology α s) t)
 658
 659   proof
 660     intro_TAC ∀α s t, H1 H2;
 661     fol H1 H2 ClosedInSubtopologyTrans CLOSED_IN_TOPSPACE;
 662   qed;
 663 `;;
 664
 665 let ClosedInClosedTrans = theorem `;
 666   ∀α s t.  u ⊂ topspace α  ⇒
 667     closed_in (subtopology α u) s ∧ closed_in α u ⇒ closed_in α s
 668   by fol ClosedInSubtopology CLOSED_IN_INTER`;;
 669
 670 let OpenInSubtopologyInterSubset = theorem `;
 671   ∀α s u v.  u ⊂ topspace α  ∧  v ⊂ topspace α  ⇒
 672     open_in (subtopology α u) (u ∩ s)  ∧  v ⊂ u
 673     ⇒ open_in (subtopology α v) (v ∩ s)
 674
 675   proof
 676     simplify OpenInSubtopology;
 677     set;
 678   qed;
 679 `;;
 680
 681 let OpenInOpenEq = theorem `;
 682   ∀α s t.  s ⊂ topspace α  ⇒
 683     open_in α s  ⇒  (open_in (subtopology α s) t  ⇔  open_in α t ∧ t ⊂ s)
 684   by fol OpenOpenInTrans OPEN_IN_SUBSET TopspaceSubtopology OpenInOpenTrans`;;
 685
 686 let ClosedInClosedEq = theorem `;
 687   ∀α s t.  s ⊂ topspace α  ⇒  closed_in α s  ⇒
 688     (closed_in (subtopology α s) t  ⇔  closed_in α t ∧ t ⊂ s)
 689   by fol ClosedClosedInTrans CLOSED_IN_SUBSET TopspaceSubtopology ClosedInClosedTrans`;;
 690
 691 let OpenImpliesSubtopologyInterOpen = theorem `;
 692   ∀α u s.  u ⊂ topspace α  ⇒
 693     open_in α s  ⇒  open_in (subtopology α u) (u ∩ s)
 694     by fol OpenInSubtopology INTER_COMM`;;
 695
 696 let OPEN_IN_EXISTS_IN = theorem `;
 697   ∀α P Q.  (∀a. P a ⇒ open_in α {x | Q a x})  ⇒
 698     open_in α {x | ∃a. P a ∧ Q a x}
 699
 700   proof
 701     intro_TAC ∀α P Q, H1;
 702     consider f such that f = {{x | Q a x} | P a}     [fDef] by fol;
 703     (∀a. P a ⇒ open_in α {x | Q a x})  ⇔  (∀s. s ∈ f ⇒ open_in α s)     [] by simplify fDef FORALL_IN_GSPEC;
 704     MP_TAC MESON [H1; -; OPEN_IN_UNIONS] [open_in α  (UNIONS f)];
 705     simplify fDef UNIONS_GSPEC;
 706     set;
 707   qed;
 708 `;;
 709
 710 let Connected_DEF = NewDefinition `;
 711   ∀α. Connected α ⇔
 712     ¬(∃e1 e2. open_in α e1  ∧  open_in α e2  ∧  topspace α = e1 ∪ e2  ∧
 713     e1 ∩ e2 = ∅  ∧  ¬(e1 = ∅)  ∧  ¬(e2 = ∅))`;;
 714
 715 let ConnectedClosedHelp = theorem `;
 716   ∀α e1 e2. topspace α = e1 ∪ e2  ∧  e1 ∩ e2 = ∅  ⇒
 717     (closed_in α e1  ∧  closed_in α e2  ⇔  open_in α e1  ∧  open_in α e2)
 718
 719   proof
 720     intro_TAC ∀α e1 e2, H1 H2;
 721     e1 = topspace α ━ e2  ∧  e2 = topspace α ━ e1     [e12Complements] by set H1 H2;
 722     fol H1 SUBSET_UNION e12Complements OPEN_IN_CLOSED_IN_EQ;
 723   qed;
 724 `;;
 725
 726 let ConnectedClosed = theorem `;
 727   ∀α. Connected α  ⇔
 728     ¬(∃e1 e2. closed_in α e1  ∧  closed_in α e2  ∧
 729     topspace α = e1 ∪ e2  ∧  e1 ∩ e2 = ∅  ∧  ¬(e1 = ∅) ∧ ¬(e2 = ∅))
 730
 731   proof
 732     rewrite Connected_DEF;
 733     fol ConnectedClosedHelp;
 734   qed;
 735 `;;
 736
 737 let ConnectedOpenIn = theorem `;
 738   ∀α s.  s ⊂ topspace α  ⇒
 739     (Connected (subtopology α s)  ⇔  ¬(∃e1 e2.
 740     open_in (subtopology α s) e1  ∧  open_in (subtopology α s) e2  ∧
 741     s ⊂ e1 ∪ e2  ∧  e1 ∩ e2 = ∅  ∧  ¬(e1 = ∅)  ∧  ¬(e2 = ∅)))
 742
 743   proof
 744     simplify Connected_DEF TopspaceSubtopology;
 745     fol SUBSET_REFL OpenInImpSubset UNION_SUBSET SUBSET_ANTISYM;
 746   qed;
 747 `;;
 748
 749 let ConnectedClosedIn = theorem `;
 750   ∀α s.  s ⊂ topspace α  ⇒
 751     (Connected (subtopology α s)  ⇔  ¬(∃e1 e2.
 752     closed_in (subtopology α s) e1  ∧  closed_in (subtopology α s) e2  ∧
 753     s ⊂ e1 ∪ e2  ∧  e1 ∩ e2 = ∅  ∧  ¬(e1 = ∅)  ∧  ¬(e2 = ∅)))
 754
 755   proof
 756     simplify ConnectedClosed TopspaceSubtopology;
 757     fol SUBSET_REFL ClosedInImpSubset UNION_SUBSET SUBSET_ANTISYM;
 758   qed;
 759 `;;
 760
 761 let ConnectedSubtopology = theorem `;
 762   ∀α s. s ⊂ topspace α  ⇒
 763     (Connected (subtopology α s)  ⇔
 764     ¬(∃e1 e2. open_in α e1  ∧  open_in α e2  ∧  s ⊂ e1 ∪ e2  ∧
 765     e1 ∩ e2 ∩ s = ∅  ∧  ¬(e1 ∩ s = ∅)  ∧  ¬(e2 ∩ s = ∅)))
 766
 767   proof
 768     intro_TAC ∀α s, H1;
 769     simplify H1 Connected_DEF OpenInSubtopology TopspaceSubtopology;
 770     AP_TERM_TAC;
 771     eq_tac     [Left]
 772     proof
 773     intro_TAC H2;
 774     consider t1 t2 such that
 775     open_in α t1  ∧  open_in α t2  ∧  s = (t1 ∩ s) ∪ (t2 ∩ s)  ∧
 776     (t1 ∩ s) ∩ (t2 ∩ s) = ∅  ∧  ¬(t1 ∩ s = ∅)  ∧  ¬(t2 ∩ s = ∅)     [t12Exist] by fol H2;
 777     s ⊂ t1 ∪ t2  ∧  t1 ∩ t2 ∩ s = ∅     [] by set t12Exist;
 778     fol t12Exist -;
 779     qed;
 780     rewrite LEFT_IMP_EXISTS_THM;
 781     intro_TAC ∀e1 e2, e12Exist;
 782     exists_TAC e1 ∩ s;
 783     exists_TAC e2 ∩ s;
 784     set e12Exist;
 785   qed;
 786 `;;
 787
 788 let ConnectedSubtopology_ALT = theorem `;
 789   ∀α s. s ⊂ topspace α  ⇒
 790     (Connected (subtopology α s)  ⇔
 791     ∀e1 e2. open_in α e1  ∧  open_in α e2  ∧
 792     s ⊂ e1 ∪ e2  ∧  e1 ∩ e2 ∩ s = ∅
 793     ⇒ e1 ∩ s = ∅  ∨  e2 ∩ s = ∅)
 794
 795   proof     simplify ConnectedSubtopology;     fol;     qed;
 796 `;;
 797
 798 let ConnectedClosedSubtopology = theorem `;
 799   ∀α s. s ⊂ topspace α  ⇒
 800     (Connected (subtopology α s)  ⇔
 801     ¬(∃e1 e2. closed_in α e1  ∧  closed_in α e2  ∧  s ⊂ e1 ∪ e2  ∧
 802     e1 ∩ e2 ∩ s = ∅  ∧  ¬(e1 ∩ s = ∅)  ∧  ¬(e2 ∩ s = ∅)))
 803
 804   proof
 805     intro_TAC ∀α s, H1;
 806     simplify H1 ConnectedSubtopology;
 807     AP_TERM_TAC;
 808     eq_tac     [Left]
 809     proof
 810       rewrite LEFT_IMP_EXISTS_THM;
 811       intro_TAC ∀e1 e2, e12Exist;
 812       exists_TAC topspace α ━ e2;
 813       exists_TAC topspace α ━ e1;
 814       simplify OPEN_IN_SUBSET H1 SUBSET_DIFF DIFF_REFL closed_in e12Exist;
 815       set H1 e12Exist;
 816     qed;
 817     rewrite LEFT_IMP_EXISTS_THM;
 818     intro_TAC ∀e1 e2, e12Exist;
 819     exists_TAC topspace α ━ e2;
 820     exists_TAC topspace α ━ e1;
 821     e1 ⊂ topspace α  ∧  e2 ⊂ topspace α     [e12Top] by fol closed_in e12Exist;
 822     simplify DIFF_REFL SUBSET_DIFF e12Top OPEN_IN_CLOSED_IN;
 823     set H1 e12Exist;
 824   qed;
 825 `;;
 826
 827 let ConnectedClosedSubtopology_ALT = theorem `;
 828   ∀α s. s ⊂ topspace α  ⇒
 829     (Connected (subtopology α s)  ⇔
 830     ∀e1 e2. closed_in α e1  ∧  closed_in α e2  ∧
 831     s ⊂ e1 ∪ e2  ∧  e1 ∩ e2 ∩ s = ∅
 832      ⇒ e1 ∩ s = ∅  ∨  e2 ∩ s = ∅)
 833
 834   proof     simplify ConnectedClosedSubtopology;     fol;     qed;
 835 `;;
 836
 837 let ConnectedClopen = theorem `;
 838   ∀α. Connected α  ⇔
 839     ∀t. open_in α t ∧ closed_in α t  ⇒  t = ∅ ∨ t = topspace α
 840
 841   proof
 842     intro_TAC ∀α;
 843     simplify Connected_DEF closed_in TAUT [(¬a ⇔ b) ⇔ (a ⇔ ¬b)] NOT_FORALL_THM NOT_IMP DE_MORGAN_THM;
 844     eq_tac     [Left]
 845     proof
 846       rewrite LEFT_IMP_EXISTS_THM;     intro_TAC ∀e1 e2, H1 H2 H3 H4 H5 H6;
 847       exists_TAC e1;
 848       e1 ⊂ topspace α  ∧  e2 = topspace α ━ e1  ∧  ¬(e1 = topspace alpha)     [] by set H3 H4 H6;
 849       fol H1 - H2 H5;
 850     qed;
 851     rewrite LEFT_IMP_EXISTS_THM;     intro_TAC ∀t, H1;
 852     exists_TAC t;     exists_TAC topspace α ━ t;
 853     set H1;
 854   qed;
 855 `;;
 856
 857 let ConnectedClosedSet = theorem `;
 858   ∀α s. s ⊂ topspace α  ⇒  closed_in α s  ⇒
 859     (Connected (subtopology α s)  ⇔  ¬(∃e1 e2.
 860     closed_in α e1  ∧  closed_in α e2  ∧
 861     ¬(e1 = ∅)  ∧  ¬(e2 = ∅)  ∧  e1 ∪ e2 = s  ∧  e1 ∩ e2 = ∅))
 862
 863   proof
 864     intro_TAC ∀α s, H1, H2;
 865     simplify H1 ConnectedClosedSubtopology;
 866     AP_TERM_TAC;
 867     eq_tac     [Left]
 868     proof
 869       rewrite LEFT_IMP_EXISTS_THM;     intro_TAC ∀e1 e2, H3 H4 H5 H6 H7 H8;
 870       exists_TAC e1 ∩ s;     exists_TAC e2 ∩ s;
 871       simplify H2 H3 H4 H7 H8 CLOSED_IN_INTER;
 872       set H5 H6;
 873     qed;
 874     rewrite LEFT_IMP_EXISTS_THM;     intro_TAC ∀e1 e2, H3 H4 H5 H6 H7 H8;
 875     exists_TAC e1;     exists_TAC e2;
 876     set H3 H4 H7 H8 H5 H6;
 877   qed;
 878 `;;
 879
 880 let ConnectedOpenSet = theorem `;
 881   ∀α s.  open_in α s  ⇒
 882     (Connected (subtopology α s) ⇔
 883     ¬(∃e1 e2.  open_in α e1  ∧  open_in α e2  ∧
 884     ¬(e1 = ∅)  ∧  ¬(e2 = ∅)  ∧  e1 ∪ e2 = s  ∧  e1 ∩ e2 = ∅))
 885
 886   proof
 887     intro_TAC ∀α s, H1;
 888     simplify H1 OPEN_IN_SUBSET ConnectedSubtopology;
 889     AP_TERM_TAC;
 890     eq_tac     [Left]
 891     proof
 892       rewrite LEFT_IMP_EXISTS_THM;     intro_TAC ∀e1 e2, H3 H4 H5 H6 H7 H8;
 893       exists_TAC e1 ∩ s;     exists_TAC e2 ∩ s;
 894       e1 ⊂ topspace α  ∧  e2 ⊂ topspace α     [e12Subsets] by fol H3 H4 OPEN_IN_SUBSET;
 895       simplify H1 H3 H4 OPEN_IN_INTER H7 H8;
 896       set e12Subsets H5 H6;
 897     qed;
 898     rewrite LEFT_IMP_EXISTS_THM;     intro_TAC ∀e1 e2, H3 H4 H5 H6 H7 H8;
 899     exists_TAC e1;     exists_TAC e2;
 900     set H3 H4 H7 H8 H5 H6;
 901   qed;
 902 `;;
 903
 904 let ConnectedEmpty = theorem `;
 905   ∀α. Connected (subtopology α ∅)
 906
 907   proof
 908     simplify Connected_DEF INTER_EMPTY EMPTY_SUBSET TopspaceSubtopology;
 909     fol UNION_SUBSET SUBSET_EMPTY;
 910   qed;
 911 `;;
 912
 913 let ConnectedSing = theorem `;
 914   ∀α a. a ∈ topspace α  ⇒  Connected (subtopology α {a})
 915
 916   proof
 917     simplify Connected_DEF SING_SUBSET TopspaceSubtopology;
 918     set;
 919   qed;
 920 `;;
 921
 922 let ConnectedUnions = theorem `;
 923   ∀α P. (∀s. s ∈ P ⇒ s ⊂ topspace α)  ⇒
 924     (∀s. s ∈ P ⇒ Connected (subtopology α s)) ∧ ¬(INTERS P = ∅)
 925         ⇒ Connected (subtopology α (UNIONS P))
 926
 927   proof
 928     intro_TAC ∀α P, H1;
 929     simplify H1 ConnectedSubtopology UNIONS_SUBSET NOT_EXISTS_THM;
 930     intro_TAC allConnected PnotDisjoint, ∀[d/e1] [e/e2];
 931     consider a such that
 932     ∀t. t ∈ P ⇒ a ∈ t     [aInterP] by fol PnotDisjoint MEMBER_NOT_EMPTY IN_INTERS;
 933     ONCE_REWRITE_TAC TAUT [∀p. ¬p ⇔ p ⇒ F];
 934     intro_TAC dOpen eOpen Pde deDisjoint dNonempty eNonempty;
 935     a ∈ d ∨ a ∈ e     [adORae] by set aInterP Pde dNonempty;
 936     consider s x t y such that
 937     s ∈ P  ∧  x ∈ d ∩ s  ∧
 938     t ∈ P  ∧  y ∈ e ∩ t     [xdsANDyet] by set dNonempty eNonempty;
 939     d ∩ e ∩ s = ∅  ∧  d ∩ e ∩ t = ∅     [] by set - deDisjoint;
 940     (d ∩ s = ∅  ∨  e ∩ s = ∅)  ∧
 941     (d ∩ t = ∅  ∨  e ∩ t = ∅)     [] by fol xdsANDyet allConnected dOpen eOpen Pde -;
 942     set adORae xdsANDyet aInterP -;
 943   qed;
 944 `;;
 945
 946 let ConnectedUnion = theorem `;
 947   ∀α s t.  s ⊂ topspace α  ∧  t ⊂ topspace α  ∧  ¬(s ∩ t = ∅)  ∧
 948     Connected (subtopology α s) ∧ Connected (subtopology α t)
 949     ⇒ Connected (subtopology α (s ∪ t))
 950
 951   proof
 952     rewrite GSYM UNIONS_2 GSYM INTERS_2;
 953     intro_TAC ∀α s t, H1 H2 H3 H4 H5;
 954     ∀u. u ∈ {s, t}  ⇒  u ⊂ topspace α     [stEuclidean] by set H1 H2;
 955     ∀u. u ∈ {s, t}  ⇒  Connected (subtopology α u)     [] by set H4 H5;
 956     fol stEuclidean - H3 ConnectedUnions;
 957   qed;
 958 `;;
 959
 960 let ConnectedDiffOpenFromClosed = theorem `;
 961   ∀α s t u.  u ⊂ topspace α  ⇒
 962     s ⊂ t  ∧  t ⊂ u ∧ open_in α s  ∧  closed_in α t  ∧
 963     Connected (subtopology α u)  ∧  Connected (subtopology α (t ━ s))
 964     ⇒ Connected (subtopology α (u ━ s))
 965
 966   proof
 967     ONCE_REWRITE_TAC TAUT
 968     [∀a b c d e f g. (a ∧ b ∧ c ∧ d ∧ e ∧ f ⇒ g)  ⇔
 969     (a ∧ b ∧ c ∧ d ⇒ ¬g ⇒ f ⇒ ¬e)];
 970     intro_TAC ∀α s t u, uSubset, st tu sOpen tClosed;
 971     t ━ s ⊂ topspace α  ∧  u ━ s ⊂ topspace α     [] by fol uSubset sOpen OPEN_IN_SUBSET tClosed closed_in SUBSET_DIFF SUBSET_TRANS;
 972     simplify uSubset - ConnectedSubtopology;
 973     rewrite LEFT_IMP_EXISTS_THM;
 974     intro_TAC ∀[v/e1] [w/e2];
 975     intro_TAC vOpen wOpen u_sDisconnected vwDisjoint vNonempty wNonempty;
 976     rewrite NOT_EXISTS_THM;
 977     intro_TAC t_sConnected;
 978     t ━ s ⊂ v ∪ w  ∧  v ∩ w ∩ (t ━ s) = ∅     [] by set tu u_sDisconnected vwDisjoint;
 979     v ∩ (t ━ s) = ∅  ∨  w ∩ (t ━ s) = ∅     [] by fol t_sConnected vOpen wOpen -;
 980     case_split vEmpty | wEmpty by fol -;
 981     suppose v ∩ (t ━ s) = ∅;
 982       exists_TAC w ∪ s;     exists_TAC v ━ t;
 983       simplify vOpen wOpen sOpen tClosed OPEN_IN_UNION OPEN_IN_DIFF;
 984       set st tu u_sDisconnected vEmpty vwDisjoint wNonempty vNonempty;
 985     end;
 986     suppose w ∩ (t ━ s) = ∅;
 987       exists_TAC v ∪ s;     exists_TAC w ━ t;
 988       simplify vOpen wOpen sOpen tClosed OPEN_IN_UNION OPEN_IN_DIFF;
 989       set st tu u_sDisconnected wEmpty vwDisjoint wNonempty vNonempty;
 990     end;
 991   qed;
 992 `;;
 993
 994 let ConnectedDisjointUnionsOpenUniquePart1 = theorem `;
 995   ∀α f f' s t a.  pairwise DISJOINT f ∧ pairwise DISJOINT f' ∧
 996     (∀s. s ∈ f  ⇒  open_in α s ∧ Connected (subtopology α s) ∧ ¬(s = ∅)) ∧
 997     (∀s. s ∈ f'  ⇒  open_in α s ∧ Connected (subtopology α s) ∧ ¬(s = ∅)) ∧
 998     UNIONS f = UNIONS f' ∧ s ∈ f ∧ t ∈ f' ∧ a ∈ s ∧ a ∈ t
 999      ⇒ s ⊂ t
1000
1001   proof
1002     intro_TAC ∀α f f' s t a, pDISJf pDISJf' fConn f'Conn Uf_Uf' sf tf' a_s a_t;
1003     ∀s.  s ∈ f ⇒ s ⊂ topspace α     [fTop] by fol fConn OPEN_IN_SUBSET;
1004     ∀s.  s ∈ f' ⇒ s ⊂ topspace α     [f'Top] by fol f'Conn OPEN_IN_SUBSET;
1005     rewrite SUBSET;
1006     X_genl_TAC b;     intro_TAC bs;
1007     assume ¬(b ∈ t)     [Contradiction] by fol;
1008     ∃e1 e2.  open_in α e1 ∧ open_in α e2 ∧ e1 ∩ e2 ∩ s = ∅ ∧
1009      s ⊂ e1 ∪ e2 ∧ ¬(e1 ∩ s = ∅) ∧ ¬(e2 ∩ s = ∅)     []
1010      proof
1011        exists_TAC t;     exists_TAC UNIONS (f' DELETE t);
1012        simplify tf' f'Conn IN_DELETE OPEN_IN_UNIONS;
1013        conj_tac     [Right] by set sf Uf_Uf' a_s a_t sf bs Contradiction;
1014        MATCH_MP_TAC SET_RULE [∀s t u. t ∩ u = ∅ ⇒ t ∩ u ∩ s = ∅];
1015        rewrite INTER_UNIONS EMPTY_UNIONS FORALL_IN_GSPEC;
1016        rewrite IN_DELETE GSYM DISJOINT;
1017        fol pDISJf' tf' pairwise;
1018      qed;
1019      fol - sf fTop fConn ConnectedSubtopology;
1020   qed;
1021 `;;
1022
1023 let ConnectedDisjointUnionsOpenUnique = theorem `;
1024   ∀α f f'.  pairwise DISJOINT f ∧ pairwise DISJOINT f' ∧
1025     (∀s. s ∈ f  ⇒  open_in α s ∧ Connected (subtopology α s) ∧ ¬(s = ∅)) ∧
1026     (∀s. s ∈ f'  ⇒  open_in α s ∧ Connected (subtopology α s) ∧ ¬(s = ∅)) ∧
1027     UNIONS f = UNIONS f'
1028     ⇒ f = f'
1029
1030   proof
1031     MATCH_MP_TAC MESON [SUBSET_ANTISYM]
1032     [(∀α s t. P α s t ⇒ P α t s) ∧ (∀α s t. P α s t ⇒ s ⊂ t)
1033     ⇒ (∀α s t. P α s t ⇒ s = t)];
1034     conj_tac     [Left] by fol;
1035     intro_TAC ∀α f f', pDISJf pDISJf' fConn f'Conn Uf_Uf';
1036     rewrite SUBSET;     X_genl_TAC s;     intro_TAC sf;
1037     consider t a such that
1038     t ∈ f' ∧ a ∈ s ∧ a ∈ t     [taExist] by set sf fConn Uf_Uf';
1039     MP_TAC ISPECL [α; f; f'; s; t] ConnectedDisjointUnionsOpenUniquePart1;
1040     MP_TAC ISPECL [α; f'; f; t; s] ConnectedDisjointUnionsOpenUniquePart1;
1041     fol pDISJf pDISJf' fConn f'Conn Uf_Uf' sf taExist SUBSET_ANTISYM taExist;
1042   qed;
1043 `;;
1044
1045 let ConnectedFromClosedUnionAndInter = theorem `;
1046   ∀α s t.  s ∪ t ⊂ topspace α ∧ closed_in α s ∧ closed_in α t ∧
1047     Connected (subtopology α (s ∪ t)) ∧ Connected (subtopology α (s ∩ t))
1048     ⇒ Connected (subtopology α s) ∧ Connected (subtopology α t)
1049
1050   proof
1051     MATCH_MP_TAC MESON [] [(∀α s t. P α s t ⇒ P α t s) ∧
1052     (∀α s t. P α s t ⇒ Q α s) ⇒ ∀α s t. P α s t ⇒ Q α s ∧ Q α t];
1053     conj_tac     [Left] by fol UNION_COMM INTER_COMM;
1054     ONCE_REWRITE_TAC TAUT
1055     [∀a b c d e f.  a ∧ b ∧ c ∧ d ∧ e ⇒ f  ⇔  a ∧ b ∧ c ∧ e ∧ ¬f ⇒ ¬d];
1056     intro_TAC ∀α s t, stUnionTop sClosed tClosed stInterConn  NOTsConn;
1057     s ⊂ topspace α ∧ t ⊂ topspace α ∧ s ∩ t ⊂ topspace α     [stTop] by fol stUnionTop UNION_SUBSET INTER_SUBSET SUBSET_TRANS;
1058     simplify stUnionTop ConnectedClosedSubtopology;
1059     consider u v such that closed_in α u ∧ closed_in α v ∧
1060     ¬(u = ∅) ∧ ¬(v = ∅) ∧ u ∪ v = s ∧ u ∩ v = ∅     [sDisConn]
1061     proof
1062       MP_TAC ISPECL [α; s] ConnectedClosedSet;
1063       simplify stTop sClosed NOTsConn;
1064     qed;
1065     s ∩ t ⊂ u ∪ v  ∧  u ∩ v ∩ (s ∩ t) = ∅     [stuvProps] by set sDisConn;
1066     u ∩ (s ∩ t) = ∅  ∨  v ∩ (s ∩ t) = ∅     [] by fol stTop stInterConn sDisConn - ConnectedClosedSubtopology_ALT;
1067     case_split vstEmpty | ustEmpty by fol -;
1068     suppose v ∩ (s ∩ t) = ∅;
1069       exists_TAC t ∪ u;     exists_TAC v;
1070       simplify tClosed sDisConn CLOSED_IN_UNION;
1071       set stuvProps sDisConn vstEmpty;
1072     end;
1073     suppose u ∩ (s ∩ t) = ∅;
1074       exists_TAC t ∪ v;     exists_TAC u;
1075       simplify tClosed sDisConn CLOSED_IN_UNION;
1076       set stuvProps sDisConn ustEmpty;
1077     end;
1078   qed;
1079 `;;
1080
1081 let ConnectedFromOpenUnionAndInter = theorem `;
1082   ∀α s t.  s ∪ t ⊂ topspace α ∧ open_in α s ∧ open_in α t ∧
1083     Connected (subtopology α (s ∪ t)) ∧ Connected (subtopology α (s ∩ t))
1084     ⇒ Connected (subtopology α s) ∧ Connected (subtopology α t)
1085
1086   proof
1087     MATCH_MP_TAC MESON [] [(∀α s t. P α s t ⇒ P α t s) ∧
1088     (∀α s t. P α s t ⇒ Q α s) ⇒ ∀α s t. P α s t ⇒ Q α s ∧ Q α t];
1089     conj_tac     [Left] by fol UNION_COMM INTER_COMM;
1090     ONCE_REWRITE_TAC TAUT
1091     [∀a b c d e f.  a ∧ b ∧ c ∧ d ∧ e ⇒ f  ⇔  a ∧ b ∧ c ∧ e ∧ ¬f ⇒ ¬d];
1092     intro_TAC ∀α s t, stUnionTop sOpen tOpen stInterConn  NOTsConn;
1093     s ⊂ topspace α ∧ t ⊂ topspace α ∧ s ∩ t ⊂ topspace α     [stTop] by fol stUnionTop UNION_SUBSET INTER_SUBSET SUBSET_TRANS;
1094     simplify stUnionTop ConnectedSubtopology;
1095     consider u v such that open_in α u ∧ open_in α v ∧
1096     ¬(u = ∅) ∧ ¬(v = ∅) ∧ u ∪ v = s ∧ u ∩ v = ∅     [sDisConn]
1097     proof
1098       MP_TAC ISPECL [α; s] ConnectedOpenSet;
1099       simplify stTop sOpen NOTsConn;
1100     qed;
1101     s ∩ t ⊂ u ∪ v  ∧  u ∩ v ∩ (s ∩ t) = ∅     [stuvProps] by set sDisConn;
1102     u ∩ (s ∩ t) = ∅  ∨  v ∩ (s ∩ t) = ∅     [] by fol stTop stInterConn sDisConn - ConnectedSubtopology_ALT;
1103     case_split vstEmpty | ustEmpty by fol -;
1104     suppose v ∩ (s ∩ t) = ∅;
1105       exists_TAC t ∪ u;     exists_TAC v;
1106       simplify tOpen sDisConn OPEN_IN_UNION;
1107       set stuvProps sDisConn vstEmpty;
1108     end;
1109     suppose u ∩ (s ∩ t) = ∅;
1110       exists_TAC t ∪ v;     exists_TAC u;
1111       simplify tOpen sDisConn OPEN_IN_UNION;
1112       set stuvProps sDisConn ustEmpty;
1113     end;
1114   qed;
1115 `;;
1116
1117 let ConnectedInduction = theorem `;
1118   ∀α P Q s.  s ⊂ topspace α  ⇒  Connected (subtopology α s) ∧
1119     (∀t a. open_in (subtopology α s) t ∧ a ∈ t  ⇒  ∃z. z ∈ t ∧ P z) ∧
1120     (∀a. a ∈ s  ⇒  ∃t. open_in (subtopology α s) t ∧ a ∈ t ∧
1121     ∀x y. x ∈ t ∧ y ∈ t ∧ P x ∧ P y ∧ Q x ⇒ Q y)
1122     ⇒ ∀a b. a ∈ s ∧ b ∈ s ∧ P a ∧ P b ∧ Q a ⇒ Q b
1123
1124   proof
1125     intro_TAC ∀α P Q s, sTop, sConn atOpenImplies_ztPz asImplies_atOpen_xytPxPyQxasImpliesQy, ∀a b, aINs bINs Pa Pb Qa;
1126     assume ¬Q b     [NotQb] by fol;
1127     ¬Connected (subtopology α s)     []
1128     proof
1129       simplify sTop ConnectedOpenIn;
1130       exists_TAC
1131       {b | ∃t. open_in (subtopology α s) t ∧ b ∈ t ∧ ∀x. x ∈ t ∧ P x ⇒ Q x};
1132       exists_TAC
1133       {b | ∃t. open_in (subtopology α s) t ∧ b ∈ t ∧ ∀x. x ∈ t ∧ P x ⇒ ¬(Q x)};
1134       conj_tac     [Left]
1135       proof
1136         ONCE_REWRITE_TAC OPEN_IN_SUBOPEN;
1137         X_genl_TAC c;
1138         rewrite IN_ELIM_THM;
1139         MATCH_MP_TAC MONO_EXISTS;
1140         set atOpenImplies_ztPz;
1141       qed;
1142       conj_tac     [Left]
1143       proof
1144         ONCE_REWRITE_TAC OPEN_IN_SUBOPEN;
1145         X_genl_TAC c;
1146         rewrite IN_ELIM_THM;
1147         MATCH_MP_TAC MONO_EXISTS;
1148         set atOpenImplies_ztPz;
1149       qed;
1150       conj_tac     [Left]
1151       proof
1152         rewrite SUBSET IN_ELIM_THM IN_UNION;
1153         X_genl_TAC c;     intro_TAC cs;
1154         MP_TAC SPECL [c] asImplies_atOpen_xytPxPyQxasImpliesQy;
1155         set cs;
1156       qed;
1157       conj_tac     [Right] by set aINs bINs Qa NotQb asImplies_atOpen_xytPxPyQxasImpliesQy Pa Pb;
1158       rewrite EXTENSION IN_INTER NOT_IN_EMPTY IN_ELIM_THM;
1159       X_genl_TAC c;
1160       ONCE_REWRITE_TAC TAUT [∀p. ¬p  ⇔  p ⇒ F];
1161       intro_TAC Qx NotQx;
1162       consider t such that
1163       open_in (subtopology α s) t ∧ c ∈ t ∧ (∀x. x ∈ t ∧ P x ⇒ Q x)     [tExists] by fol Qx;
1164       consider u such that
1165       open_in (subtopology α s) u ∧ c ∈ u ∧ (∀x. x ∈ u ∧ P x ⇒ ¬Q x)     [uExists] by fol NotQx;
1166       MP_TAC SPECL [t ∩ u; c] atOpenImplies_ztPz;
1167       simplify tExists uExists OPEN_IN_INTER;
1168       set tExists uExists;
1169     qed;
1170     fol sConn -;
1171   qed;
1172 `;;
1173
1174 let ConnectedEquivalenceRelationGen = theorem `;
1175   ∀α P R s.  s ⊂ topspace α  ⇒  Connected (subtopology α s) ∧
1176         (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
1177         (∀t a. open_in (subtopology α s) t ∧ a ∈ t
1178                ⇒ ∃z. z ∈ t ∧ P z) ∧
1179         (∀a. a ∈ s
1180              ⇒ ∃t. open_in (subtopology α s) t ∧ a ∈ t ∧
1181                      ∀x y. x ∈ t ∧ y ∈ t ∧ P x ∧ P y ⇒ R x y)
1182         ⇒ ∀a b. a ∈ s ∧ b ∈ s ∧ P a ∧ P b ⇒ R a b
1183
1184   proof
1185     intro_TAC ∀α P R s, sTop, sConn Rtrans atOpenImplies_ztPz asImplies_atOpen_xytPxPyImpliesRxy, ∀a b, aINs bINs Pa Pb;
1186     ∀a.  a ∈ s ∧ P a  ⇒  ∀b c. b ∈ s ∧ c ∈ s ∧ P b ∧ P c ∧ R a b ⇒ R a c     []
1187     proof
1188       intro_TAC ∀[p/a], pINs Pp;
1189       MP_TAC ISPECL [α; P; λx. R p x; s] ConnectedInduction;
1190       rewrite sTop sConn atOpenImplies_ztPz;
1191       fol asImplies_atOpen_xytPxPyImpliesRxy Rtrans;
1192     qed;
1193     fol aINs Pa bINs Pb asImplies_atOpen_xytPxPyImpliesRxy -;
1194   qed;
1195 `;;
1196
1197 let ConnectedInductionSimple = theorem `;
1198   ∀α P s.  s ⊂ topspace α  ⇒
1199         Connected (subtopology α s) ∧
1200         (∀a. a ∈ s
1201              ⇒ ∃t. open_in (subtopology α s) t ∧ a ∈ t ∧
1202                      ∀x y. x ∈ t ∧ y ∈ t ∧ P x ⇒ P y)
1203         ⇒ ∀a b. a ∈ s ∧ b ∈ s ∧ P a ⇒ P b
1204
1205   proof
1206     intro_TAC ∀α P s, sTop;
1207     MP_TAC ISPECL [α; (λx. T ∨ x ∈ s); P; s] ConnectedInduction;
1208     fol sTop;
1209   qed;
1210 `;;
1211
1212 let ConnectedEquivalenceRelation = theorem `;
1213   ∀α R s.  s ⊂ topspace α  ⇒  Connected (subtopology α s)∧
1214     (∀x y. R x y ⇒ R y x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
1215     (∀a. a ∈ s ⇒
1216     ∃t. open_in (subtopology α s) t ∧ a ∈ t ∧ ∀x. x ∈ t ⇒ R a x)
1217     ⇒ ∀a b. a ∈ s ∧ b ∈ s ⇒ R a b
1218
1219   proof
1220     intro_TAC ∀α R s, sTop, sConn Rcomm Rtrans asImplies_atOpen_xtImpliesRax;
1221     ∀a. a ∈ s ⇒ ∀b c. b ∈ s ∧ c ∈ s ∧ R a b ⇒ R a c     []
1222     proof
1223       intro_TAC ∀[p/a], pINs;
1224       MP_TAC ISPECL [α; λx. R p x; s] ConnectedInductionSimple;
1225        rewrite sTop sConn;
1226       fol asImplies_atOpen_xtImpliesRax Rcomm Rtrans;
1227     qed;
1228     fol asImplies_atOpen_xtImpliesRax -;
1229   qed;
1230 `;;
1231
1232 let LimitPointOf = NewDefinition `;
1233   ∀α s. LimitPointOf α s  =  {x | s ⊂ topspace α ∧ x ∈ topspace α ∧
1234     ∀t. x ∈ t ∧ open_in α t  ⇒  ∃y. ¬(y = x) ∧ y ∈ s ∧ y ∈ t}`;;
1235
1236 let IN_LimitPointOf = theorem `;
1237   ∀α s x.  s ⊂ topspace α  ⇒
1238     (x ∈ LimitPointOf α s  ⇔  x ∈ topspace α ∧
1239     ∀t. x ∈ t ∧ open_in α t  ⇒  ∃y. ¬(y = x) ∧ y ∈ s ∧ y ∈ t)
1240   by simplify IN_ELIM_THM LimitPointOf`;;
1241
1242 let NotLimitPointOf = theorem `;
1243   ∀α s x.  s ⊂ topspace α ∧ x ∈ topspace α  ⇒
1244     (x ∉ LimitPointOf α s  ⇔
1245     ∃t. x ∈ t  ∧  open_in α t  ∧  s ∩ (t ━ {x}) = ∅)
1246
1247   proof
1248     ONCE_REWRITE_TAC TAUT [∀a b. (a ⇔ b)  ⇔  (¬a  ⇔ ¬b)];
1249     simplify ∉ NOT_EXISTS_THM IN_LimitPointOf
1250     TAUT [∀a b. ¬(a ∧ b ∧ c)  ⇔  a ∧ b ⇒ ¬c] GSYM MEMBER_NOT_EMPTY IN_INTER  IN_DIFF IN_SING;
1251      fol;
1252   qed;
1253 `;;
1254
1255 let LimptSubset = theorem `;
1256   ∀α s t.  t ⊂ topspace α  ⇒
1257     s ⊂ t  ⇒  LimitPointOf α s ⊂ LimitPointOf α t
1258
1259   proof
1260     intro_TAC ∀α s t, tTop, st;
1261     s ⊂ topspace α     [sTop] by fol tTop st SUBSET_TRANS;
1262     simplify tTop sTop IN_LimitPointOf SUBSET;
1263     fol st SUBSET;
1264   qed;
1265 `;;
1266
1267 let ClosedLimpt = theorem `;
1268   ∀α s.  s ⊂ topspace α  ⇒
1269     (closed_in α s  ⇔  LimitPointOf α s ⊂ s)
1270
1271   proof
1272     intro_TAC ∀α s, H1;
1273     simplify H1 closed_in;
1274     ONCE_REWRITE_TAC OPEN_IN_SUBOPEN;
1275     simplify H1 IN_LimitPointOf SUBSET IN_DIFF;
1276     AP_TERM_TAC;
1277     ABS_TAC;
1278     fol OPEN_IN_SUBSET SUBSET;
1279   qed;
1280 `;;
1281
1282 let LimptEmpty = theorem `;
1283   ∀α x.  x ∈ topspace α  ⇒  x ∉ LimitPointOf α ∅
1284   by fol EMPTY_SUBSET IN_LimitPointOf OPEN_IN_TOPSPACE NOT_IN_EMPTY ∉`;;
1285
1286 let NoLimitPointImpClosed = theorem `;
1287   ∀α s.  s ⊂ topspace α  ⇒  (∀x. x ∉ LimitPointOf α s)  ⇒  closed_in α s
1288   by fol ClosedLimpt SUBSET ∉`;;
1289
1290 let LimitPointUnion = theorem `;
1291   ∀α s t.  s ∪ t ⊂ topspace α  ⇒
1292     LimitPointOf α (s ∪ t)  =  LimitPointOf α s  ∪  LimitPointOf α t
1293
1294   proof
1295     intro_TAC ∀α s t, H1;
1296     s ⊂ topspace α ∧ t ⊂ topspace α     [stTop] by fol H1 UNION_SUBSET;
1297     rewrite EXTENSION IN_UNION;
1298     intro_TAC ∀x;
1299     assume x ∈ topspace α     [xTop] by fol H1 stTop IN_LimitPointOf;
1300     ONCE_REWRITE_TAC TAUT [∀a b. (a ⇔ b)  ⇔  (¬a  ⇔ ¬b)];
1301     simplify GSYM NOTIN DE_MORGAN_THM H1 stTop NotLimitPointOf xTop;
1302     eq_tac     [Left] by set;
1303     MATCH_MP_TAC ExistsTensorInter;
1304     simplify IN_INTER OPEN_IN_INTER;
1305     set;
1306   qed;
1307 `;;
1308
1309 let Interior_DEF = NewDefinition `;
1310   ∀α s.  Interior α s =
1311     {x | s ⊂ topspace α  ∧  ∃t. open_in α t ∧ x ∈ t ∧ t ⊂ s}`;;
1312
1313 let Interior_THM = theorem `;
1314   ∀α s.  s ⊂ topspace α  ⇒  Interior α s =
1315     {x | s ⊂ topspace α  ∧  ∃t. open_in α t ∧ x ∈ t ∧ t ⊂ s}
1316   by fol Interior_DEF`;;
1317
1318 let IN_Interior = theorem `;
1319   ∀α s x.  s ⊂ topspace α  ⇒
1320     (x ∈ Interior α s  ⇔  ∃t. open_in α t ∧ x ∈ t ∧ t ⊂ s)
1321   by simplify Interior_THM IN_ELIM_THM`;;
1322
1323 let InteriorEq = theorem `;
1324   ∀α s.  s ⊂ topspace α  ⇒
1325     (open_in α s  ⇔  s = Interior α s)
1326
1327   proof
1328     intro_TAC ∀α s, H1;
1329     rewriteL OPEN_IN_SUBOPEN;
1330     simplify EXTENSION H1 IN_Interior;
1331     set;
1332   qed;
1333 `;;
1334
1335 let InteriorOpen = theorem `;
1336   ∀α s.  open_in α s  ⇒  Interior α s = s
1337   by fol OPEN_IN_SUBSET InteriorEq`;;
1338
1339 let InteriorEmpty = theorem `;
1340   ∀α. Interior α ∅ = ∅
1341   by fol OPEN_IN_EMPTY EMPTY_SUBSET InteriorOpen`;;
1342
1343 let InteriorUniv = theorem `;
1344   ∀α. Interior α (topspace α) = topspace α
1345   by simplify OpenInTopspace InteriorOpen`;;
1346
1347 let OpenInterior = theorem `;
1348   ∀α s.  s ⊂ topspace α  ⇒  open_in α (Interior α s)
1349
1350   proof
1351     ONCE_REWRITE_TAC OPEN_IN_SUBOPEN;
1352     fol IN_Interior SUBSET;
1353   qed;
1354 `;;
1355
1356 let InteriorInterior = theorem `;
1357   ∀α s.  s ⊂ topspace α  ⇒
1358     Interior α  (Interior α s) = Interior α s
1359   by fol OpenInterior InteriorOpen`;;
1360
1361 let InteriorSubset = theorem `;
1362   ∀α s.  s ⊂ topspace α  ⇒  Interior α s ⊂ s
1363
1364   proof
1365     intro_TAC ∀α s, H1;
1366     simplify SUBSET Interior_DEF IN_ELIM_THM;
1367     fol H1 SUBSET;
1368   qed;
1369 `;;
1370
1371 let InteriorTopspace = theorem `;
1372   ∀α s.  s ⊂ topspace α  ⇒  Interior α s ⊂ topspace α
1373   by fol SUBSET_TRANS InteriorSubset`;;
1374
1375 let SubsetInterior = theorem `;
1376   ∀α s t.  t ⊂ topspace α  ⇒  s ⊂ t  ⇒
1377     Interior α s ⊂ Interior α t
1378   by fol SUBSET_TRANS SUBSET IN_Interior SUBSET`;;
1379
1380 let InteriorMaximal = theorem `;
1381   ∀α s t.  s ⊂ topspace α  ⇒
1382     t ⊂ s ∧ open_in α t  ⇒  t ⊂ Interior α s
1383   by fol SUBSET IN_Interior SUBSET`;;
1384
1385 let InteriorMaximalEq = theorem `;
1386   ∀s t.  t ⊂ topspace α  ⇒
1387     open_in α s  ⇒  (s ⊂ Interior α t  ⇔  s ⊂ t)
1388   by fol InteriorMaximal SUBSET_TRANS InteriorSubset`;;
1389
1390 let InteriorUnique = theorem `;
1391   ∀α s t.  s ⊂ topspace α  ⇒
1392     t ⊂ s  ∧  open_in α t ∧  (∀t'. t' ⊂ s ∧ open_in α t' ⇒ t' ⊂ t)
1393     ⇒ Interior α s = t
1394   by fol SUBSET_ANTISYM InteriorSubset OpenInterior InteriorMaximal`;;
1395
1396 let OpenSubsetInterior = theorem `;
1397   ∀α s t.  t ⊂ topspace α  ⇒
1398     open_in α s  ⇒  (s ⊂ Interior α t  ⇔  s ⊂ t)
1399   by fol InteriorMaximal InteriorSubset SUBSET_TRANS`;;
1400
1401 let InteriorInter = theorem `;
1402   ∀α s t.  s ⊂ topspace α  ∧  t ⊂ topspace α  ⇒
1403     Interior α (s ∩ t) = Interior α s ∩ Interior α t
1404
1405   proof
1406     intro_TAC ∀α s t, sTop tTop;
1407     rewrite GSYM SUBSET_ANTISYM_EQ SUBSET_INTER;
1408     conj_tac     [Left] by fol sTop tTop SubsetInterior INTER_SUBSET;
1409     s ∩ t ⊂ topspace α     [] by fol sTop INTER_SUBSET SUBSET_TRANS;
1410     fol - sTop tTop OpenInterior OPEN_IN_INTER InteriorSubset InteriorMaximal INTER_TENSOR;
1411   qed;
1412 `;;
1413
1414 let InteriorFiniteInters = theorem `;
1415   ∀α s.  FINITE s ⇒ ¬(s = ∅) ⇒ (∀t. t ∈ s ⇒ t ⊂ topspace α) ⇒
1416     Interior α (INTERS s) = INTERS (IMAGE (Interior α) s)
1417
1418   proof
1419     intro_TAC ∀α;
1420     MATCH_MP_TAC FINITE_INDUCT;
1421     rewrite INTERS_INSERT IMAGE_CLAUSES IN_INSERT;
1422     intro_TAC ∀x s, sCase, xsNonempty, sSetOfSubsets;
1423     assume ¬(s = ∅)     [sNonempty] by simplify INTERS_0 INTER_UNIV IMAGE_CLAUSES;
1424     simplify INTERS_SUBSET  sSetOfSubsets InteriorInter sNonempty sSetOfSubsets sCase;
1425   qed;
1426 `;;
1427
1428 let InteriorIntersSubset = theorem `;
1429   ∀α f.  ¬(f = ∅) ∧ (∀t. t ∈ f ⇒ t ⊂ topspace α) ⇒
1430     Interior α (INTERS f)  ⊂  INTERS (IMAGE (Interior α) f)
1431
1432   proof
1433     intro_TAC ∀α f, H1 H2;
1434     INTERS f ⊂ topspace α     [] by set H1 H2;
1435     simplify SUBSET IN_INTERS FORALL_IN_IMAGE - H2 IN_Interior;
1436     fol;
1437   qed;
1438 `;;
1439
1440 let UnionInteriorSubset = theorem `;
1441   ∀α s t.  s ⊂ topspace α  ∧  t ⊂ topspace α  ⇒
1442     Interior α s ∪ Interior α t  ⊂  Interior α (s ∪ t)
1443
1444   proof
1445     intro_TAC ∀α s t, sTop tTop;
1446     s ∪ t ⊂ topspace α     [] by fol sTop tTop UNION_SUBSET;
1447     fol sTop tTop - OpenInterior OPEN_IN_UNION InteriorMaximal UNION_TENSOR InteriorSubset;
1448   qed;
1449 `;;
1450
1451 let InteriorEqEmpty = theorem `;
1452   ∀α s.  s ⊂ topspace α  ⇒
1453     (Interior α s = ∅  ⇔  ∀t. open_in α t ∧ t ⊂ s  ⇒  t = ∅)
1454   by fol InteriorMaximal SUBSET_EMPTY OpenInterior SUBSET_REFL InteriorSubset`;;
1455
1456 let InteriorEqEmptyAlt = theorem `;
1457   ∀α s.  s ⊂ topspace α  ⇒
1458     (Interior α s = ∅  ⇔  ∀t. open_in α t ∧ ¬(t = ∅) ⇒ ¬(t ━ s = ∅))
1459
1460   proof
1461     simplify InteriorEqEmpty;
1462     set;
1463   qed;
1464 `;;
1465
1466 let InteriorUnionsOpenSubsets = theorem `;
1467   ∀α s.  s ⊂ topspace α  ⇒  UNIONS {t | open_in α t ∧ t ⊂ s} = Interior α s
1468
1469   proof
1470     intro_TAC ∀α s, H1;
1471     consider t such that
1472     t = UNIONS {f | open_in α f ∧ f ⊂ s}     [tDef] by fol;
1473     t ⊂ s  ∧  ∀f. f ⊂ s ∧ open_in α f ⇒ f ⊂ t     [] by set tDef;
1474     simplify H1 tDef - OPEN_IN_UNIONS IN_ELIM_THM InteriorUnique;
1475   qed;
1476 `;;
1477
1478 let InteriorClosedUnionEmptyInterior = theorem `;
1479   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1480     closed_in α s ∧ Interior α t = ∅  ⇒
1481     Interior α (s ∪ t) = Interior α s
1482
1483   proof
1484     intro_TAC ∀α s t, H1 H2, H3 H4;
1485     s ∪ t ⊂ topspace α     [stTop] by fol H1 H2 UNION_SUBSET;
1486     Interior α (s ∪ t) ⊂ s     []
1487     proof
1488       simplify SUBSET stTop IN_Interior LEFT_IMP_EXISTS_THM;
1489       X_genl_TAC y O;     intro_TAC openO yO Os_t;
1490       consider O' such that O' = (topspace α ━ s) ∩ O     [O'def] by fol -;
1491       O' ⊂ t     [O't] by set O'def Os_t;
1492       assume y ∉ s     [yNOTs] by fol ∉;
1493       y ∈ topspace α ━ s     [] by fol openO OPEN_IN_SUBSET yO SUBSET yNOTs IN_DIFF ∉;
1494       y ∈ O'  ∧  open_in α O'     [] by fol O'def - yO IN_INTER H3 closed_in openO OPEN_IN_INTER;
1495       fol O'def - O't H2 IN_Interior SUBSET MEMBER_NOT_EMPTY H4;
1496     qed;
1497     fol SUBSET_ANTISYM H1 stTop OpenInterior - InteriorMaximal SUBSET_UNION SubsetInterior;
1498   qed;
1499 `;;
1500
1501 let InteriorUnionEqEmpty = theorem `;
1502   ∀α s t.  s ∪ t ⊂ topspace α  ⇒
1503     closed_in α s ∨ closed_in α t
1504     ⇒ (Interior α (s ∪ t) = ∅  ⇔  Interior α s = ∅ ∧ Interior α t = ∅)
1505
1506   proof
1507     intro_TAC ∀α s t, H1, H2;
1508     s ⊂ topspace α ∧ t ⊂ topspace α     [] by fol H1 UNION_SUBSET;
1509     eq_tac     [Left] by fol - H1 SUBSET_UNION SubsetInterior SUBSET_EMPTY;
1510     fol UNION_COMM - H2 InteriorClosedUnionEmptyInterior;
1511   qed;
1512 `;;
1513
1514 let Closure_DEF = NewDefinition `;
1515   ∀α s.  Closure α s  =  s ∪ LimitPointOf α s`;;
1516
1517 let Closure_THM = theorem `;
1518   ∀α s.  s ⊂ topspace α  ⇒  Closure α s  =  s ∪ LimitPointOf α s
1519   by fol Closure_DEF`;;
1520
1521 let IN_Closure = theorem `;
1522   ∀α s x.  s ⊂ topspace α  ⇒
1523     (x ∈ Closure α s  ⇔  x ∈ topspace α ∧
1524     ∀t. x ∈ t ∧ open_in α t  ⇒  ∃y. y ∈ s ∧ y ∈ t)
1525
1526   proof
1527     intro_TAC ∀α s x, H1;
1528     simplify H1 Closure_THM IN_UNION IN_LimitPointOf;
1529     fol H1 SUBSET;
1530   qed;
1531 `;;
1532
1533 let ClosureSubset = theorem `;
1534   ∀α s.  s ⊂ topspace α  ⇒  s ⊂ Closure α s
1535   by fol SUBSET IN_Closure`;;
1536
1537 let ClosureTopspace = theorem `;
1538   ∀α s.  s ⊂ topspace α  ⇒  Closure α s ⊂ topspace α
1539   by fol SUBSET IN_Closure`;;
1540
1541 let ClosureInterior = theorem `;
1542   ∀α s.  s ⊂ topspace α  ⇒
1543     Closure α s  =  topspace α ━ (Interior α (topspace α ━ s))
1544
1545   proof
1546     intro_TAC ∀α s, H1;
1547     simplify H1 EXTENSION IN_Closure IN_DIFF IN_Interior SUBSET;
1548     fol OPEN_IN_SUBSET SUBSET;
1549   qed;
1550 `;;
1551
1552 let InteriorClosure = theorem `;
1553   ∀α s.  s ⊂ topspace α  ⇒
1554     Interior α s = topspace α ━ (Closure α (topspace α ━ s))
1555   by fol SUBSET_DIFF InteriorTopspace DIFF_REFL ClosureInterior`;;
1556
1557 let ClosedClosure = theorem `;
1558   ∀α s.  s ⊂ topspace α  ⇒  closed_in α (Closure α s)
1559   by fol closed_in ClosureInterior DIFF_REFL SUBSET_DIFF InteriorTopspace OpenInterior`;;
1560
1561 let SubsetClosure = theorem `;
1562   ∀α s t.  t ⊂ topspace α  ⇒  s ⊂ t  ⇒  Closure α s ⊂ Closure α t
1563
1564   proof
1565     intro_TAC ∀α s t, tSubset, st;
1566     s ⊂ topspace α     [] by fol tSubset st SUBSET_TRANS;
1567     simplify tSubset - Closure_THM st LimptSubset UNION_TENSOR;
1568   qed;
1569 `;;
1570
1571 let ClosureHull = theorem `;
1572   ∀α s.  s ⊂ topspace α  ⇒  Closure α s = (closed_in α) hull s
1573
1574   proof
1575     intro_TAC ∀α s, H1;
1576     MATCH_MP_TAC GSYM HULL_UNIQUE;
1577     simplify H1 ClosureSubset ClosedClosure Closure_THM UNION_SUBSET;
1578     fol LimptSubset CLOSED_IN_SUBSET ClosedLimpt SUBSET_TRANS;
1579   qed;
1580 `;;
1581
1582 let ClosureEq = theorem `;
1583   ∀α s.  s ⊂ topspace α  ⇒  (Closure α s = s  ⇔  closed_in α s)
1584   by fol ClosedClosure ClosedLimpt Closure_THM SUBSET_UNION_ABSORPTION UNION_COMM`;;
1585
1586 let ClosureClosed = theorem `;
1587   ∀α s.  closed_in α s  ⇒  Closure α s = s
1588   by fol closed_in ClosureEq`;;
1589
1590 let ClosureClosure = theorem `;
1591   ∀α s.  s ⊂ topspace α  ⇒  Closure α (Closure α s) = Closure α s
1592   by fol ClosureTopspace ClosureHull HULL_HULL`;;
1593
1594 let ClosureUnion = theorem `;
1595   ∀α s t.  s ∪ t ⊂ topspace α
1596     ⇒ Closure α (s ∪ t)  =  Closure α s ∪ Closure α t
1597
1598   proof
1599     intro_TAC ∀α s t, H1;
1600     s ⊂ topspace α ∧ t ⊂ topspace α     [stTop] by fol H1 UNION_SUBSET;
1601     simplify H1 stTop Closure_THM LimitPointUnion;
1602     set;
1603   qed;
1604 `;;
1605
1606 let ClosureInterSubset = theorem `;
1607   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1608     Closure α (s ∩ t)  ⊂  Closure α s ∩ Closure α t
1609   by fol SUBSET_INTER INTER_SUBSET SubsetClosure`;;
1610
1611 let ClosureIntersSubset = theorem `;
1612   ∀α f.  (∀s. s ∈ f ⇒ s ⊂ topspace α)  ⇒
1613     Closure α (INTERS f)  ⊂  INTERS (IMAGE (Closure α) f)
1614
1615   proof
1616     intro_TAC ∀α f, H1;
1617     rewrite SET_RULE [s ⊂ INTERS f ⇔ ∀t. t ∈ f ⇒ s ⊂ t] FORALL_IN_IMAGE;
1618     X_genl_TAC s;
1619     intro_TAC sf;
1620     s ⊂ topspace α  ∧  INTERS f ⊂ s  ∧  INTERS f ⊂ topspace α     [] by set H1 sf;
1621     fol SubsetClosure -;
1622   qed;
1623 `;;
1624
1625 let ClosureMinimal = theorem `;
1626   ∀α s t.  s ⊂ t ∧ closed_in α t  ⇒  Closure α s ⊂ t
1627   by fol closed_in SubsetClosure ClosureClosed`;;
1628
1629 let ClosureMinimalEq = theorem `;
1630   ∀α s t.  s ⊂ topspace α  ⇒
1631     closed_in α t  ⇒  (Closure α s ⊂ t ⇔ s ⊂ t)
1632   by fol closed_in SUBSET_TRANS ClosureSubset ClosureMinimal`;;
1633
1634 let ClosureUnique = theorem `;
1635   ∀α s t.  s ⊂ t ∧ closed_in α t ∧ (∀u. s ⊂ u ∧ closed_in α u  ⇒  t ⊂ u)
1636     ⇒ Closure α s = t
1637   by fol closed_in SUBSET_ANTISYM_EQ ClosureMinimal SUBSET_TRANS ClosureSubset ClosedClosure`;;
1638
1639 let ClosureUniv = theorem `;
1640   ∀α.  Closure α (topspace α) =  topspace α
1641   by simplify SUBSET_REFL CLOSED_IN_TOPSPACE ClosureEq`;;
1642
1643 let ClosureEmpty = theorem `;
1644   Closure α ∅ = ∅
1645   by fol EMPTY_SUBSET CLOSED_IN_EMPTY ClosureClosed`;;
1646
1647 let ClosureUnions = theorem `;
1648   ∀α f.  FINITE f  ⇒  (∀ t. t ∈ f ⇒ t ⊂ topspace α)  ⇒
1649     Closure α (UNIONS f) = UNIONS {Closure α t | t ∈ f}
1650
1651   proof
1652     intro_TAC ∀α;
1653     MATCH_MP_TAC FINITE_INDUCT;
1654     rewrite UNIONS_0 SET_RULE [{f x | x ∈ ∅} = ∅] ClosureEmpty UNIONS_INSERT
1655     SET_RULE [{f x | x ∈ a INSERT t} = (f a) INSERT {f x | x ∈ t}] IN_INSERT;
1656     fol UNION_SUBSET UNIONS_SUBSET IN_UNIONS ClosureUnion;
1657   qed;
1658 `;;
1659
1660 let ClosureEqEmpty = theorem `;
1661   ∀α s.  s ⊂ topspace α  ⇒  (Closure α s = ∅  ⇔  s = ∅)
1662   by fol ClosureEmpty ClosureSubset SUBSET_EMPTY`;;
1663
1664 let ClosureSubsetEq = theorem `;
1665   ∀α s.  s ⊂ topspace α  ⇒  (Closure α s ⊂ s  ⇔  closed_in α s)
1666   by fol ClosureEq ClosureSubset SUBSET_ANTISYM`;;
1667
1668 let OpenInterClosureEqEmpty = theorem `;
1669   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1670     open_in α s  ⇒  (s ∩ Closure α t = ∅  ⇔  s ∩ t = ∅)
1671
1672   proof
1673     intro_TAC ∀α s t, H1 H2, H3;
1674     eq_tac     [Left] by fol H2 ClosureSubset INTER_TENSOR SUBSET_REFL SUBSET_EMPTY;
1675     intro_TAC stDisjoint;
1676     s ⊂ Interior α (topspace α ━ t)     [] by fol H2 SUBSET_DIFF H3 H1 H2 stDisjoint SUBSET_COMPLEMENT OpenSubsetInterior;
1677     fol H1 H2 InteriorTopspace - COMPLEMENT_DISJOINT H2 ClosureInterior;
1678   qed;
1679 `;;
1680
1681 let OpenInterClosureSubset = theorem `;
1682   ∀α s t.  t ⊂ topspace α  ⇒
1683     open_in α s  ⇒  s ∩ Closure α t ⊂ Closure α (s ∩ t)
1684
1685   proof
1686     intro_TAC ∀α s t, tTop, sOpen;
1687     s ⊂ topspace α     [sTop] by fol OPEN_IN_SUBSET sOpen;
1688     s ∩ t ⊂ topspace α     [stTop] by fol sTop sTop INTER_SUBSET SUBSET_TRANS;
1689     simplify tTop - Closure_THM UNION_OVER_INTER SUBSET_UNION SUBSET_UNION;
1690     s ∩ LimitPointOf α t  ⊂  LimitPointOf α (s ∩ t)     []
1691     proof
1692       simplify SUBSET IN_INTER tTop stTop IN_LimitPointOf;
1693       X_genl_TAC x;     intro_TAC xs xTop xLIMt;
1694       X_genl_TAC O;     intro_TAC xO Oopen;
1695       x ∈ O ∩ s  ∧  open_in α (O ∩ s)     [xOsOpen] by fol xs xO IN_INTER Oopen sOpen OPEN_IN_INTER;
1696       fol xOsOpen xLIMt IN_INTER;
1697     qed;
1698     simplify - UNION_TENSOR SUBSET_REFL;
1699   qed;
1700 `;;
1701
1702 let ClosureOpenInterSuperset = theorem `;
1703   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1704     open_in α s ∧ s ⊂ Closure α t  ⇒  Closure α (s ∩ t) = Closure α s
1705
1706   proof
1707     intro_TAC ∀α s t, sTop tTop, sOpen sSUBtC;
1708     s ∩ t ⊂ topspace α     [stTop] by fol INTER_SUBSET sTop SUBSET_TRANS;
1709     MATCH_MP_TAC SUBSET_ANTISYM;
1710     conj_tac     [Left] by fol sTop INTER_SUBSET SubsetClosure;
1711     s  ⊂  Closure α (s ∩ t)     [] by fol tTop sOpen OpenInterClosureSubset SUBSET_REFL sSUBtC SUBSET_INTER SUBSET_TRANS;
1712     fol stTop - ClosedClosure ClosureMinimal;
1713   qed;
1714 `;;
1715
1716 let ClosureComplement = theorem `;
1717   ∀α s.  s ⊂ topspace α  ⇒
1718     Closure α (topspace α ━ s) = topspace α ━ Interior α s
1719   by fol InteriorClosure SUBSET_DIFF ClosureTopspace DIFF_REFL`;;
1720
1721 let InteriorComplement = theorem `;
1722   ∀α s.  s ⊂ topspace α  ⇒
1723     Interior α (topspace α ━ s) = topspace α ━ Closure α s
1724   by fol SUBSET_DIFF InteriorTopspace DIFF_REFL ClosureInterior DIFF_REFL`;;
1725
1726 let ClosureInteriorComplement = theorem `;
1727   ∀α s.  s ⊂ topspace α  ⇒
1728     topspace α ━ Closure α (Interior α s)
1729     = Interior α (Closure α (topspace α ━ s))
1730   by fol InteriorTopspace InteriorComplement ClosureComplement`;;
1731
1732 let InteriorClosureComplement = theorem `;
1733   ∀α s.  s ⊂ topspace α  ⇒
1734     topspace α ━ Interior α (Closure α s)
1735     = Closure α (Interior α (topspace α ━ s))
1736   by fol ClosureTopspace SUBSET_TRANS InteriorComplement ClosureComplement`;;
1737
1738 let ConnectedIntermediateClosure = theorem `;
1739   ∀α s t.  s ⊂ topspace α  ⇒
1740     Connected (subtopology α s) ∧  s ⊂ t  ∧  t ⊂ Closure α s
1741     ⇒ Connected (subtopology α t)
1742
1743   proof
1744     intro_TAC ∀α s t, sTop, sCon st tCs;
1745     t ⊂ topspace α     [tTop] by fol tCs sTop ClosureTopspace SUBSET_TRANS;
1746     simplify tTop ConnectedSubtopology_ALT;
1747     X_genl_TAC u v;
1748     intro_TAC uOpen vOpen t_uv uvtEmpty;
1749     u ⊂ topspace α  ∧  v ⊂ topspace α     [uvTop] by fol uOpen vOpen OPEN_IN_SUBSET;
1750     u ∩ s = ∅  ∨  v ∩ s = ∅     [] by fol sTop uvTop uOpen vOpen st t_uv uvtEmpty SUBSET_TRANS SUBSET_REFL INTER_TENSOR SUBSET_EMPTY sCon ConnectedSubtopology_ALT;
1751     s ⊂ topspace α ━ u  ∨  s ⊂ topspace α ━ v     [] by fol - sTop uvTop INTER_COMM SUBSET_COMPLEMENT;
1752     t ⊂ topspace α ━ u  ∨  t ⊂ topspace α ━ v     [] by fol SUBSET_DIFF - uvTop uOpen vOpen OPEN_IN_CLOSED_IN ClosureMinimal tCs SUBSET_TRANS;
1753     fol tTop uvTop - SUBSET_COMPLEMENT INTER_COMM;
1754   qed;
1755 `;;
1756
1757 let ConnectedClosure = theorem `;
1758   ∀α s.  s ⊂ topspace α  ⇒  Connected (subtopology α s) ⇒
1759     Connected (subtopology α (Closure α s))
1760   by fol ClosureTopspace ClosureSubset SUBSET_REFL ConnectedIntermediateClosure`;;
1761
1762 let ConnectedUnionStrong = theorem `;
1763   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1764     Connected (subtopology α s)  ∧  Connected (subtopology α t)  ∧
1765     ¬(Closure α s ∩ t = ∅)
1766     ⇒ Connected (subtopology α (s ∪ t))
1767
1768   proof
1769     intro_TAC ∀α s t, sTop tTop, H2 H3 H4;
1770     consider p s' such that
1771     p ∈ Closure α s  ∧  p ∈ t  ∧  s' = p ╪ s     [pCst] by fol H4 MEMBER_NOT_EMPTY IN_INTER;
1772     s ⊂ s'  ∧  s' ⊂ Closure α s     [s_ps_Cs] by fol IN_INSERT SUBSET pCst sTop ClosureSubset INSERT_SUBSET;
1773     Connected (subtopology α (s'))     [s'Con] by fol sTop H2 s_ps_Cs ConnectedIntermediateClosure;
1774     s ∪ t = s' ∪ t  ∧  ¬(s' ∩ t = ∅)     [] by fol pCst INSERT_UNION IN_INSERT IN_INTER MEMBER_NOT_EMPTY;
1775     fol s_ps_Cs sTop ClosureTopspace SUBSET_TRANS tTop - s'Con H3 ConnectedUnion;
1776   qed;
1777 `;;
1778
1779 let InteriorDiff = theorem `;
1780   ∀α s t.   s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1781     Interior α (s ━ t) = Interior α s ━ Closure α t
1782   by fol ClosureTopspace InteriorTopspace COMPLEMENT_INTER_DIFF InteriorComplement SUBSET_DIFF InteriorInter`;;
1783
1784 let ClosedInLimpt = theorem `;
1785   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1786     (closed_in (subtopology α t) s  ⇔
1787     s ⊂ t  ∧  LimitPointOf α s ∩ t ⊂ s)
1788
1789   proof
1790     intro_TAC ∀α s t, H1 H2;
1791     simplify H2 ClosedInSubtopology;
1792     eq_tac     [Right]
1793     proof
1794       intro_TAC sSUBt LIMstSUBs;
1795       exists_TAC Closure α s;
1796       simplify H1 ClosedClosure Closure_THM INTER_COMM UNION_OVER_INTER;
1797       set sSUBt LIMstSUBs;
1798     qed;
1799     rewrite LEFT_IMP_EXISTS_THM;     X_genl_TAC D;     intro_TAC Dexists;
1800     LimitPointOf α (D ∩ t) ⊂ D     [] by fol Dexists CLOSED_IN_SUBSET INTER_SUBSET LimptSubset ClosedLimpt SUBSET_TRANS;
1801     fol Dexists INTER_SUBSET - SUBSET_REFL INTER_TENSOR;
1802   qed;
1803 `;;
1804
1805 let ClosedInLimpt_ALT = theorem `;
1806   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1807     (closed_in (subtopology α t) s  ⇔
1808     s ⊂ t  ∧  ∀x. x ∈ LimitPointOf α s ∧ x ∈ t ⇒ x ∈ s)
1809   by simplify SUBSET IN_INTER ClosedInLimpt`;;
1810
1811 let ClosedInInterClosure = theorem `;
1812   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1813     (closed_in (subtopology α s) t  ⇔  s ∩ Closure α t = t)
1814
1815   proof     simplify Closure_THM ClosedInLimpt;     set;     qed;
1816 `;;
1817
1818 let InteriorClosureIdemp = theorem `;
1819   ∀α s.  s ⊂ topspace α  ⇒
1820     Interior α (Closure α (Interior α (Closure α s)))
1821     = Interior α (Closure α s)
1822
1823   proof
1824     intro_TAC ∀α s, H1;
1825     consider IC CIC such that
1826     IC = Interior α (Closure α s)  ∧  CIC = Closure α IC     [CICdef] by fol;
1827     Closure α s ⊂ topspace α     [Ctop] by fol H1 ClosureTopspace;
1828     IC ⊂ topspace α     [ICtop] by fol CICdef - H1 InteriorTopspace;
1829     CIC ⊂ topspace α     [CICtop] by fol CICdef - ClosureTopspace;
1830     IC ⊂ CIC     [ICsubCIC] by fol CICdef ICtop ClosureSubset;
1831     ∀u. u ⊂ CIC ∧ open_in α u ⇒ u ⊂ IC     [] by fol CICdef Ctop InteriorSubset SubsetClosure H1 ClosureClosure SUBSET_TRANS OpenSubsetInterior;
1832     fol CICdef CICtop ICsubCIC Ctop OpenInterior - InteriorUnique;
1833   qed;
1834 `;;
1835
1836 let InteriorClosureIdemp = theorem `;
1837   ∀α s.  s ⊂ topspace α  ⇒
1838     Interior α (Closure α (Interior α (Closure α s)))
1839     = Interior α (Closure α s)
1840
1841   proof
1842     intro_TAC ∀α s, H1;
1843     Closure α s ⊂ topspace α     [Ctop] by fol H1 ClosureTopspace;
1844     consider IC CIC such that
1845     IC = Interior α (Closure α s)  ∧  CIC = Closure α IC     [ICdefs] by fol;
1846     IC ⊂ topspace α     [] by fol - Ctop H1 InteriorTopspace;
1847     CIC ⊂ topspace α  ∧  IC ⊂ CIC  ∧  ∀u. u ⊂ CIC ∧ open_in α u ⇒ u ⊂ IC     [] by fol ICdefs Ctop - ClosureTopspace ClosureSubset InteriorSubset SubsetClosure H1 ClosureClosure SUBSET_TRANS OpenSubsetInterior;
1848     fol ICdefs - Ctop OpenInterior InteriorUnique;
1849   qed;
1850 `;;
1851
1852 let ClosureInteriorIdemp = theorem `;
1853   ∀α s.  s ⊂ topspace α  ⇒
1854     Closure α (Interior α (Closure α (Interior α s)))
1855     = Closure α (Interior α s)
1856
1857   proof
1858     intro_TAC ∀α s, H1;
1859     consider t such that t = topspace α ━ s     [tDef] by fol;
1860     t ⊂ topspace α  ∧  s = topspace α ━ t     [tProps] by fol - H1 SUBSET_DIFF DIFF_REFL;
1861     Interior α (Closure α t) ⊂ topspace α     [] by fol - ClosureTopspace InteriorTopspace;
1862     simplify tProps - GSYM InteriorClosureComplement InteriorClosureIdemp;
1863   qed;
1864 `;;
1865
1866 let InteriorClosureDiffSpaceEmpty = theorem `;
1867   ∀α s.  s ⊂ topspace α  ⇒  Interior α (Closure α s ━ s) = ∅
1868
1869   proof
1870     intro_TAC ∀α s, H1;
1871     Closure α s ━ s ⊂ topspace α     [Cs_sTop] by fol H1 ClosureTopspace SUBSET_DIFF SUBSET_TRANS;
1872     assume ¬(Interior α (Closure α s ━ s) = ∅)     [Contradiction] by fol;
1873     consider x such that
1874     x ∈ (Interior α (Closure α s ━ s))     [xExists] by fol - MEMBER_NOT_EMPTY;
1875     consider t such that
1876     open_in α t ∧ x ∈ t ∧ t ⊂ (s ∪ LimitPointOf α s) ━ s     [tProps] by fol - Cs_sTop IN_Interior Closure_DEF;
1877     t ⊂ LimitPointOf α s ∧ s ∩ (t ━ {x}) = ∅     [tSubLIMs] by set -;
1878     x ∈ LimitPointOf α s ∧ x ∉ s     [xLims] by fol tProps - SUBSET IN_DIFF ∉;
1879     fol H1 xLims IN_LimitPointOf tProps tSubLIMs NotLimitPointOf ∉;
1880   qed;
1881 `;;
1882
1883 let NowhereDenseUnion = theorem `;
1884   ∀α s t.  s ∪ t ⊂ topspace α  ⇒
1885     (Interior α (Closure α (s ∪ t)) = ∅  ⇔
1886     Interior α (Closure α s) = ∅  ∧  Interior α (Closure α t) = ∅)
1887
1888   proof
1889     intro_TAC ∀α s t, H1;
1890     s ⊂ topspace α ∧ t ⊂ topspace α     [] by fol H1 UNION_SUBSET;
1891     simplify H1 - ClosureUnion ClosureTopspace UNION_SUBSET ClosedClosure InteriorUnionEqEmpty;
1892   qed;
1893 `;;
1894
1895 let NowhereDense = theorem `;
1896   ∀α s.  s ⊂ topspace α  ⇒
1897     (Interior α (Closure α s) = ∅ ⇔
1898     ∀t. open_in α t ∧ ¬(t = ∅)  ⇒
1899     ∃u. open_in α u ∧ ¬(u = ∅) ∧ u ⊂ t ∧ u ∩ s = ∅)
1900
1901   proof
1902     intro_TAC ∀α s, H1;
1903     simplify H1 ClosureTopspace InteriorEqEmptyAlt;
1904     eq_tac     [Left]
1905     proof
1906       intro_TAC H2;
1907       X_genl_TAC t;
1908       intro_TAC tOpen tNonempty;
1909       exists_TAC t ━ Closure α s;
1910       fol tOpen H1 ClosedClosure OPEN_IN_DIFF tOpen tNonempty H2 SUBSET_DIFF H1 ClosureSubset
1911       SET_RULE [∀s t A.  s ⊂ t  ⇒  (A ━ t) ∩ s = ∅];
1912     qed;
1913     intro_TAC H2;
1914     X_genl_TAC t;
1915     intro_TAC tOpen tNonempty;
1916     consider u such that
1917     open_in α u ∧ ¬(u = ∅) ∧ u ⊂ t ∧ u ∩ s = ∅     [uExists] by simplify tOpen tNonempty H2;
1918     MP_TAC ISPECL [α; u; s] OpenInterClosureEqEmpty;
1919     simplify uExists OPEN_IN_SUBSET H1;
1920     set uExists;
1921   qed;
1922 `;;
1923
1924 let InteriorClosureInterOpen = theorem `;
1925   ∀α s t.  open_in α s ∧ open_in α t  ⇒
1926     Interior α (Closure α (s ∩ t)) =
1927     Interior α (Closure α s) ∩ Interior α (Closure α t)
1928
1929   proof
1930     intro_TAC ∀α s t, sOpen tOpen;
1931     s ⊂ topspace α     [sTop] by fol sOpen OPEN_IN_SUBSET;
1932     t ⊂ topspace α     [tTop] by fol tOpen OPEN_IN_SUBSET;
1933     rewrite SET_RULE [∀s t u. u = s ∩ t  ⇔  s ∩ t ⊂ u ∧ u ⊂ s ∧ u ⊂ t];
1934     simplify sTop tTop INTER_SUBSET SubsetClosure ClosureTopspace SubsetInterior;
1935     s ∩ t ⊂ topspace α     [stTop] by fol INTER_SUBSET sTop SUBSET_TRANS;
1936     Closure α s ⊂ topspace α  ∧  Closure α t ⊂ topspace α     [CsCtTop] by fol sTop tTop ClosureTopspace;
1937     Closure α s ∩ Closure α t ⊂ topspace α     [CsIntCtTop] by fol - INTER_SUBSET SUBSET_TRANS;
1938     Closure α s ━ s ∪ Closure α t ━ t  ⊂  topspace α     [Cs_sUNIONCt_tTop] by fol CsCtTop SUBSET_DIFF UNION_SUBSET SUBSET_TRANS;
1939     simplify CsCtTop GSYM InteriorInter;
1940     Interior α (Closure α s ∩ Closure α t) ⊂ Closure α (s ∩ t)     []
1941     proof
1942       simplify CsIntCtTop InteriorTopspace ISPECL [topspace α] COMPLEMENT_DISJOINT stTop ClosureTopspace GSYM ClosureComplement GSYM InteriorComplement CsIntCtTop SUBSET_DIFF GSYM InteriorInter;
1943       closed_in α (Closure α s ━ s) ∧ closed_in α (Closure α t ━ t)     [] by fol sTop tTop ClosedClosure sOpen tOpen CLOSED_IN_DIFF;
1944       Interior α (Closure α s ━ s ∪ Closure α t ━ t) = ∅     [IntEmpty] by fol Cs_sUNIONCt_tTop - sTop tTop InteriorClosureDiffSpaceEmpty InteriorUnionEqEmpty;
1945       Closure α s ∩ Closure α t ∩ (topspace α ━ (s ∩ t))  ⊂
1946       Closure α s ━ s ∪ Closure α t ━ t     [] by set;
1947       fol Cs_sUNIONCt_tTop - SubsetInterior IntEmpty INTER_ACI SUBSET_EMPTY;
1948     qed;
1949     fol stTop ClosureTopspace - CsIntCtTop OpenInterior InteriorMaximal;
1950   qed;
1951 `;;
1952
1953 let ClosureInteriorUnionClosed = theorem `;
1954   ∀α s t.   closed_in α s ∧ closed_in α t ⇒
1955     Closure α (Interior α (s ∪ t))  =
1956     Closure α (Interior α s) ∪ Closure α (Interior α t)
1957
1958   proof
1959     rewrite closed_in;
1960     intro_TAC ∀α s t, sClosed tClosed;
1961     simplify sClosed tClosed ClosureTopspace UNION_SUBSET InteriorTopspace ISPECL [topspace α] COMPLEMENT_DUALITY_UNION;
1962     simplify sClosed tClosed UNION_SUBSET ClosureTopspace InteriorTopspace ClosureInteriorComplement DIFF_UNION SUBSET_DIFF InteriorClosureInterOpen;
1963   qed;
1964 `;;
1965
1966 let RegularOpenInter = theorem `;
1967   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1968     Interior α (Closure α s) = s ∧ Interior α (Closure α t) = t
1969     ⇒ Interior α (Closure α (s ∩ t)) = s ∩ t
1970   by fol ClosureTopspace OpenInterior InteriorClosureInterOpen`;;
1971
1972 let RegularClosedUnion = theorem `;
1973   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1974     Closure α (Interior α s) = s  ∧  Closure α (Interior α t) = t
1975     ⇒ Closure α (Interior α (s ∪ t)) = s ∪ t
1976   by fol InteriorTopspace ClosureInteriorUnionClosed ClosedClosure`;;
1977
1978 let DiffClosureSubset = theorem `;
1979   ∀α s t.  s ⊂ topspace α ∧ t ⊂ topspace α  ⇒
1980     Closure α s ━ Closure α t ⊂ Closure α (s ━ t)
1981
1982   proof
1983     intro_TAC ∀α s t, sTop tTop;
1984     Closure α s ━ Closure α t ⊂ Closure α (s ━ Closure α t)     [] by fol sTop ClosureTopspace tTop ClosedClosure tTop closed_in OpenInterClosureSubset INTER_COMM COMPLEMENT_INTER_DIFF;
1985     fol - tTop ClosureSubset SUBSET_DUALITY sTop SUBSET_DIFF SUBSET_TRANS SubsetClosure;
1986   qed;
1987 `;;
1988
1989 let Frontier_DEF = NewDefinition `;
1990   ∀α s.  Frontier α s = Closure α s ━ Interior α s`;;
1991
1992 let Frontier_THM = theorem `;
1993   ∀α s.  s ⊂ topspace α  ⇒  Frontier α s = Closure α s ━ Interior α s
1994   by fol Frontier_DEF`;;
1995
1996 let FrontierTopspace = theorem `;
1997   ∀α s.  s ⊂ topspace α  ⇒  Frontier α s ⊂ topspace α
1998   by fol Frontier_THM SUBSET_DIFF ClosureTopspace SUBSET_TRANS`;;
1999
2000 let FrontierClosed = theorem `;
2001   ∀α s.  s ⊂ topspace α  ⇒  closed_in α (Frontier α s)
2002   by simplify Frontier_THM ClosedClosure OpenInterior CLOSED_IN_DIFF`;;
2003
2004 let FrontierClosures = theorem `;
2005   ∀s.  s ⊂ topspace α  ⇒
2006     Frontier α s  =  (Closure α s) ∩ (Closure α (topspace α ━ s))
2007   by simplify SET_RULE [∀A s t.  s ⊂ A ∧ t ⊂ A   ⇒  s ━ (A ━ t) = s ∩ t] Frontier_THM InteriorClosure ClosureTopspace SUBSET_DIFF`;;
2008
2009 let FrontierStraddle = theorem `;
2010   ∀α a s.  s ⊂ topspace α  ⇒  (a ∈ Frontier α s  ⇔
2011     a ∈ topspace α  ∧  ∀t. open_in α t ∧ a ∈ t  ⇒
2012     (∃x. x ∈ s ∧ x ∈ t)  ∧  (∃x. ¬(x ∈ s) ∧ x ∈ t))
2013
2014   proof
2015     simplify SUBSET_DIFF FrontierClosures IN_INTER SUBSET_DIFF IN_Closure IN_DIFF;
2016     fol OPEN_IN_SUBSET SUBSET;
2017   qed;
2018 `;;
2019
2020 let FrontierSubsetClosed = theorem `;
2021   ∀α s.  closed_in α s  ⇒  (Frontier α s) ⊂ s
2022   by fol closed_in Frontier_THM ClosureClosed SUBSET_DIFF`;;
2023
2024 let FrontierEmpty = theorem `;
2025   ∀α.  Frontier α ∅ = ∅
2026   by fol Frontier_THM EMPTY_SUBSET ClosureEmpty EMPTY_DIFF`;;
2027
2028 let FrontierUniv = theorem `;
2029   ∀α. Frontier α (topspace α) = ∅
2030   by fol Frontier_DEF ClosureUniv InteriorUniv DIFF_EQ_EMPTY`;;
2031
2032 let FrontierSubsetEq = theorem `;
2033   ∀α s.  s ⊂ topspace α  ⇒  ((Frontier α s) ⊂ s ⇔ closed_in α s)
2034
2035   proof
2036     intro_TAC ∀α s, sTop;
2037     eq_tac     [Right] by fol FrontierSubsetClosed;
2038     simplify sTop Frontier_THM ;
2039     fol sTop InteriorSubset SET_RULE [∀s t u. s ━ t ⊂ u ∧ t ⊂ u ⇒ s ⊂ u] ClosureSubsetEq;
2040   qed;
2041 `;;
2042
2043 let FrontierComplement = theorem `;
2044   ∀α s.  s ⊂ topspace α  ⇒  Frontier α (topspace α ━ s) = Frontier α s
2045
2046   proof
2047     intro_TAC ∀α s, sTop;
2048     simplify sTop SUBSET_DIFF Frontier_THM ClosureComplement InteriorComplement;
2049     fol sTop InteriorTopspace ClosureTopspace SET_RULE [∀ Top Int Clo.
2050     Int ⊂ Top ∧ Clo ⊂ Top  ⇒  Top ━ Int ━ (Top ━ Clo) = Clo ━ Int];
2051   qed;
2052 `;;
2053
2054 let FrontierComplement = theorem `;
2055   ∀α s.  s ⊂ topspace α  ⇒  Frontier α (topspace α ━ s) = Frontier α s
2056
2057   proof
2058     intro_TAC ∀α s, sTop;
2059     simplify sTop SUBSET_DIFF Frontier_THM ClosureComplement InteriorComplement;
2060     fol sTop InteriorTopspace ClosureTopspace SET_RULE [∀ Top Int Clo.
2061     Int ⊂ Top ∧ Clo ⊂ Top  ⇒  Top ━ Int ━ (Top ━ Clo) = Clo ━ Int];
2062   qed;
2063 `;;
2064
2065 let FrontierDisjointEq = theorem `;
2066   ∀α s.  s ⊂ topspace α   ⇒  ((Frontier α s) ∩ s = ∅  ⇔  open_in α s)
2067
2068   proof
2069     intro_TAC ∀α s, sTop;
2070     topspace α ━ s ⊂ topspace α     [COMPsTop] by fol sTop SUBSET_DIFF;
2071     simplify sTop GSYM FrontierComplement OPEN_IN_CLOSED_IN;
2072     fol COMPsTop GSYM FrontierSubsetEq FrontierTopspace SUBSET_COMPLEMENT;
2073   qed;
2074 `;;
2075
2076 let FrontierInterSubset = theorem `;
2077   ∀α s t.  s ∪ t ⊂ topspace α  ⇒  Frontier α (s ∩ t)  ⊂  Frontier α s ∪ Frontier α t
2078
2079   proof
2080     intro_TAC ∀α s t, H1;
2081     s ⊂ topspace α ∧ t ⊂ topspace α ∧ s ∩ t ⊂ topspace α     [] by fol H1 SUBSET_UNION INTER_SUBSET SUBSET_TRANS;
2082     simplify - Frontier_THM InteriorInter DIFF_INTER INTER_SUBSET SubsetClosure DIFF_SUBSET UNION_TENSOR;
2083   qed;
2084 `;;
2085
2086 let FrontierUnionSubset = theorem `;
2087   ∀α s t.  s ∪ t ⊂ topspace α  ⇒
2088     Frontier α (s ∪ t)  ⊂  Frontier α s ∪ Frontier α t
2089
2090   proof
2091     intro_TAC ∀α s t, H1;
2092     s ⊂ topspace α ∧ t ⊂ topspace α     [stTop] by fol H1 SUBSET_UNION SUBSET_TRANS;
2093     simplify H1 - GSYM FrontierComplement DIFF_UNION;
2094     topspace α ━ s ∪ topspace α ━ t ⊂ topspace α     [] by fol SUBSET_DIFF UNION_SUBSET SUBSET_TRANS;
2095     fol - FrontierInterSubset;
2096   qed;
2097 `;;
2098
2099 let FrontierInteriors = theorem `;
2100   ∀α s.  s ⊂ topspace α  ⇒
2101     Frontier α s = topspace α ━ Interior α s ━ Interior α (topspace α ━ s)
2102   by simplify Frontier_THM ClosureInterior DOUBLE_DIFF_UNION UNION_COMM`;;
2103
2104 let FrontierFrontierSubset = theorem `;
2105   ∀α s.  s ⊂ topspace α  ⇒  Frontier α (Frontier α s) ⊂ Frontier α s
2106   by fol FrontierTopspace Frontier_THM FrontierClosed ClosureClosed SUBSET_DIFF`;;
2107
2108 let InteriorFrontier = theorem `;
2109   ∀α s.  s ⊂ topspace α  ⇒  Interior α (Frontier α s)  =
2110     Interior α (Closure α s) ━ Closure α (Interior α s)
2111
2112   proof
2113     intro_TAC ∀α s, sTop;
2114     Frontier α s = Closure α s ∩ (topspace α ━ Interior α s)     [] by fol sTop Frontier_THM ClosureTopspace COMPLEMENT_INTER_DIFF;
2115     Interior α (Frontier α s)  =
2116     Interior α (Closure α s) ∩ (topspace α ━ Closure α (Interior α s))     [] by fol - sTop ClosureTopspace InteriorTopspace SUBSET_DIFF InteriorInter InteriorComplement;
2117     fol - sTop ClosureTopspace InteriorTopspace COMPLEMENT_INTER_DIFF;
2118   qed;
2119 `;;
2120
2121 let InteriorFrontierEmpty = theorem `;
2122   ∀α s.  open_in α s ∨ closed_in α s  ⇒  Interior α (Frontier α s) = ∅
2123   by fol InteriorFrontier SET_RULE [∀s t. s ━ t = ∅ ⇔ s ⊂ t] OPEN_IN_SUBSET closed_in
2124   InteriorOpen ClosureTopspace InteriorSubset
2125   ClosureClosed InteriorTopspace ClosureSubset`;;
2126
2127 let FrontierFrontier = theorem `;
2128   ∀α s.  open_in α s ∨ closed_in α s  ⇒
2129     Frontier α (Frontier α s) = Frontier α s
2130
2131   proof
2132     intro_TAC ∀α s, openORclosed;
2133     s ⊂ topspace α     [sTop] by fol openORclosed OPEN_IN_SUBSET closed_in;
2134     Frontier α (Frontier α s) = Closure α (Frontier α s)     [] by fol sTop FrontierTopspace Frontier_THM openORclosed InteriorFrontierEmpty DIFF_EMPTY;
2135     fol - sTop FrontierClosed ClosureClosed;
2136   qed;
2137 `;;
2138
2139 let UnionFrontierPart1 = theorem `;
2140   ∀α s t.  s ∪ t ⊂ topspace α  ⇒
2141     Frontier α s ∩ Interior α t  ⊂  Frontier  α (s ∩ t)
2142
2143   proof
2144     intro_TAC ∀α s t, H1;
2145     s ⊂ topspace α ∧ t ⊂ topspace α ∧ s ∩ t ⊂ topspace α     [stTop] by fol H1 SUBSET_UNION INTER_SUBSET SUBSET_TRANS;
2146     rewrite SUBSET IN_INTER;
2147     X_genl_TAC a;     intro_TAC aFs aIt;
2148     consider O such that
2149     open_in α O ∧ a ∈ O ∧ O ⊂ t     [aOs] by fol aIt stTop IN_Interior;
2150     a ∈ topspace α     [] by fol stTop aFs FrontierTopspace SUBSET;
2151     simplify stTop FrontierStraddle -;
2152     X_genl_TAC P;     intro_TAC Popen aP;
2153     a ∈ O ∩ P ∧ open_in α (O ∩ P)     [aOPopen] by fol aOs aP IN_INTER Popen OPEN_IN_INTER;
2154     consider x y such that
2155     x ∈ s ∧ x ∈ O ∩ P ∧ ¬(y ∈ s) ∧ y ∈ O ∩ P     [xExists] by fol aOs Popen OPEN_IN_INTER aOPopen stTop aFs FrontierStraddle;
2156     fol xExists aOs IN_INTER SUBSET;
2157   qed;
2158 `;;
2159
2160 let UnionFrontierPart2 = theorem `;
2161   ∀α s t.  s ∪ t ⊂ topspace α  ⇒
2162     Frontier α s ━ Frontier α t  ⊂
2163     Frontier α (s ∩ t) ∪ Frontier α (s ∪ t)
2164
2165   proof
2166     intro_TAC ∀α s t, stTop;
2167     s ⊂ topspace α ∧ t ⊂ topspace α     [] by fol stTop SUBSET_UNION INTER_SUBSET SUBSET_TRANS;
2168     Frontier α s ━ Frontier α t = Frontier α s ∩ Interior α t  ∪
2169     Frontier α (topspace α ━ s) ∩ Interior α (topspace α ━ t)     [] by fol - FrontierTopspace FrontierInteriors FrontierComplement
2170     SET_RULE [∀A s t u. s ⊂ A  ⇒  s ━ (A ━ t ━ u) = s ∩ t ∪ s ∩ u];
2171     Frontier α s ━ Frontier α t  ⊂
2172     Frontier α (s ∩ t) ∪  Frontier α (topspace α ━ (s ∪ t))     [] by simplify - stTop UnionFrontierPart1 UNION_TENSOR SUBSET_DIFF UNION_SUBSET DIFF_UNION;
2173     fol - stTop FrontierComplement;
2174   qed;
2175 `;;
2176
2177 let UnionFrontierPart3 = theorem `;
2178   ∀α s t a.  s ∪ t ⊂ topspace α  ⇒
2179     a ∈ Frontier α s ∧ a ∉ Frontier α t  ⇒
2180     a ∈ Frontier α (s ∩ t)  ∨  a ∈ Frontier α (s ∪ t)
2181
2182   proof
2183     intro_TAC ∀α s t a, H1;
2184     rewrite ∉ GSYM IN_INTER GSYM IN_DIFF GSYM IN_UNION;
2185     fol H1 UnionFrontierPart2 SUBSET;
2186   qed;
2187 `;;
2188
2189 let UnionFrontier = theorem `;
2190   ∀α s t.  s ∪ t ⊂ topspace α  ⇒
2191     Frontier α s ∪ Frontier α t =
2192     Frontier α (s ∪ t) ∪ Frontier α (s ∩ t) ∪ Frontier α s ∩ Frontier α t
2193
2194   proof
2195     intro_TAC ∀α s t, H1;
2196     s ⊂ topspace α ∧ t ⊂ topspace α     [stTop] by fol H1 SUBSET_UNION INTER_SUBSET SUBSET_TRANS;
2197     rewrite GSYM SUBSET_ANTISYM_EQ;
2198     conj_tac     [Right] by fol SET_RULE [∀s t. s ∩ t ⊂ s ∪ t] stTop FrontierUnionSubset UNION_SUBSET FrontierInterSubset;
2199     rewrite SUBSET IN_INTER IN_UNION;
2200     fol H1 UnionFrontierPart3 INTER_COMM UNION_COMM ∉;
2201   qed;
2202 `;;
2203
2204 let ConnectedInterFrontier = theorem `;
2205   ∀α s t.  s ∪ t ⊂ topspace α  ⇒
2206     Connected (subtopology α s) ∧ ¬(s ∩ t = ∅) ∧ ¬(s ━ t = ∅)
2207     ⇒ ¬(s ∩ Frontier α t = ∅)
2208
2209   proof
2210     intro_TAC ∀α s t, H1;
2211     s ⊂ topspace α ∧ t ⊂ topspace α     [stTop] by fol H1 SUBSET_UNION SUBSET_TRANS;
2212     ONCE_REWRITE_TAC TAUT [∀a b c d. a ∧ b ∧ c ⇒ ¬d  ⇔  b ∧ c ∧ d ⇒ ¬a];
2213     intro_TAC sINTERtNonempty sDIFFtNonempty sInterFtEmpty;
2214     simplify stTop ConnectedOpenIn;
2215     exists_TAC s ∩ Interior α t;
2216     exists_TAC s ∩ Interior α (topspace α  ━  t);
2217     simplify stTop SUBSET_DIFF OpenInterior OpenInOpenInter;
2218     Interior α t ⊂ t  ∧  Interior α (topspace α ━ t) ⊂ topspace α ━ t     [IntSubs] by fol stTop SUBSET_DIFF InteriorSubset;
2219     s  ⊂  Interior α t ∪ Interior α (topspace α ━ t)     [] by fol stTop sInterFtEmpty FrontierInteriors DOUBLE_DIFF_UNION COMPLEMENT_DISJOINT;
2220     set sDIFFtNonempty sINTERtNonempty IntSubs -;
2221   qed;
2222 `;;
2223
2224 let InteriorClosedEqEmptyAsFrontier = theorem `;
2225   ∀α s.  s ⊂ topspace α  ⇒
2226     (closed_in α s ∧ Interior α s = ∅  ⇔  ∃t. open_in α t ∧ s = Frontier α t)
2227
2228   proof
2229     intro_TAC ∀α s, sTop;
2230     eq_tac     [Right] by fol OPEN_IN_SUBSET FrontierClosed InteriorFrontierEmpty;
2231     intro_TAC sClosed sEmptyInt;
2232     exists_TAC topspace α ━ s;
2233     fol sClosed closed_in sTop FrontierComplement Frontier_THM sEmptyInt DIFF_EMPTY ClosureClosed;
2234   qed;
2235 `;;
2236
2237 let ClosureUnionFrontier = theorem `;
2238   ∀α s.  s ⊂ topspace α  ⇒  Closure α s = s ∪ Frontier α s
2239
2240   proof
2241     intro_TAC ∀α s, sTop;
2242     simplify sTop Frontier_THM;
2243     s ⊂ Closure α s ∧ Interior α s ⊂ s     [] by fol sTop ClosureSubset InteriorSubset;
2244     set -;
2245   qed;
2246 `;;
2247
2248 let FrontierInteriorSubset = theorem `;
2249   ∀α s.  s ⊂ topspace α  ⇒  Frontier α (Interior α s) ⊂ Frontier α s
2250   by simplify InteriorTopspace Frontier_THM InteriorInterior InteriorSubset SubsetClosure DIFF_SUBSET`;;
2251
2252 let FrontierClosureSubset = theorem `;
2253   ∀α s.  s ⊂ topspace α  ⇒  Frontier α (Closure α s) ⊂ Frontier α s
2254   by simplify ClosureTopspace Frontier_THM ClosureClosure ClosureTopspace ClosureSubset SubsetInterior SUBSET_DUALITY`;;
2255
2256 let SetDiffFrontier = theorem `;
2257   ∀α s.  s ⊂ topspace α  ⇒  s ━ Frontier α s = Interior α s
2258
2259   proof
2260     intro_TAC ∀α s, sTop;
2261     simplify sTop Frontier_THM;
2262     s ⊂ Closure α s ∧ Interior α s ⊂ s     [] by fol sTop ClosureSubset InteriorSubset;
2263     set -;
2264   qed;
2265 `;;
2266
2267 let FrontierInterSubsetInter = theorem `;
2268   ∀α s t.  s ∪ t ⊂ topspace α  ⇒
2269     Frontier α (s ∩ t)  ⊂
2270     Closure α s ∩ Frontier α t  ∪  Frontier α s ∩ Closure α t
2271
2272   proof
2273     intro_TAC ∀α s t, H1;
2274     s ⊂ topspace α ∧ t ⊂ topspace α ∧ s ∩ t ⊂ topspace α     [stTop] by fol H1 SUBSET_UNION INTER_SUBSET SUBSET_TRANS;
2275     simplify H1 stTop Frontier_THM InteriorInter;
2276     Closure α (s ∩ t) ⊂ Closure α s ∩ Closure α t     [] by fol stTop ClosureInterSubset;
2277     set -;
2278   qed;
2279 `;;
2280
2281 let FrontierUnionPart1 = theorem `;
2282   ∀α s t.  s ∪ t ⊂ topspace α  ⇒  Closure α s ∩ Closure α t = ∅
2283     ⇒ Frontier α s ∩ Interior α (s ∪ t) = ∅
2284
2285   proof
2286     intro_TAC ∀α s t, H1, CsCtDisjoint;
2287     s ⊂ topspace α ∧ t ⊂ topspace α ∧ s ∩ t ⊂ topspace α     [stTop] by fol H1 SUBSET_UNION INTER_SUBSET SUBSET_TRANS;
2288     Frontier α s ∩ Interior α (s ∪ t)  ⊂ topspace α     [FIstTop] by fol stTop FrontierTopspace INTER_SUBSET SUBSET_TRANS;
2289     Frontier α s ∩ Interior α (s ∪ t) ∩ (topspace α ━ Closure α t) = ∅     []
2290     proof
2291       simplify stTop GSYM InteriorComplement H1 SUBSET_DIFF InteriorInter Frontier_THM;
2292       Interior α (s ∪ t) ∩ Interior α (topspace α ━ t)  ⊂ Interior α s     [] by
2293       fol SET_RULE [∀A s t. s ⊂ A  ⇒  (s ∪ t) ∩ (A ━ t) = s ━ t] H1 SUBSET_DIFF InteriorInter stTop SubsetInterior;
2294       set -;
2295     qed;
2296     Frontier α s ∩ Interior α (s ∪ t)  ⊂  Closure α t     [] by fol H1 CsCtDisjoint - FIstTop COMPLEMENT_DISJOINT INTER_ACI;
2297     fol SET_RULE [∀ s t F I. s ∩ t = ∅ ∧ F ⊂ s ∧ F ∩ I ⊂ t  ⇒  F ∩ I = ∅] CsCtDisjoint stTop Frontier_THM SUBSET_DIFF  -;
2298   qed;
2299 `;;
2300
2301 let FrontierUnion = theorem `;
2302   ∀α s t.  s ∪ t ⊂ topspace α  ⇒  Closure α s ∩ Closure α t = ∅
2303     ⇒ Frontier α (s ∪ t) = Frontier α s ∪ Frontier α t
2304
2305   proof
2306     intro_TAC ∀α s t, H1, CsCtDisjoint;
2307     s ⊂ topspace α ∧ t ⊂ topspace α ∧ s ∩ t ⊂ topspace α     [stTop] by fol H1 SUBSET_UNION INTER_SUBSET SUBSET_TRANS;
2308     MATCH_MP_TAC SUBSET_ANTISYM;
2309     simplify H1 FrontierUnionSubset Frontier_THM;
2310     Frontier α s ∩ Interior α (s ∪ t)  =  ∅  ∧
2311     Frontier α t ∩ Interior α (s ∪ t)  =  ∅     [usePart1] by fol H1 CsCtDisjoint FrontierUnionPart1 INTER_COMM UNION_COMM;
2312     Frontier α s ⊂ Closure α (s ∪ t)  ∧  Frontier α t ⊂ Closure α (s ∪ t)     [] by fol stTop Frontier_THM SUBSET_DIFF H1 SUBSET_UNION SubsetClosure SUBSET_TRANS;
2313     set usePart1 -;
2314   qed;
2315 `;;
2316
2317 (* ------------------------------------------------------------------------- *)
2318 (* The universal Euclidean versions are what we use most of the time.        *)
2319 (* ------------------------------------------------------------------------- *)
2320
2321 let open_def = NewDefinition `;
2322   open s  ⇔  ∀x. x ∈ s ⇒ ∃e. &0 < e ∧ ∀x'. dist(x',x) < e ⇒ x' ∈ s`;;
2323
2324 let closed = NewDefinition `;
2325   closed s ⇔ open (UNIV ━ s)`;;
2326
2327 let euclidean = new_definition
2328  `euclidean = mk_topology (UNIV, open)`;;
2329
2330 let OPEN_EMPTY = theorem `;
2331   open ∅
2332   by rewrite open_def NOT_IN_EMPTY`;;
2333
2334 let OPEN_UNIV = theorem `;
2335   open UNIV
2336   by fol open_def IN_UNIV REAL_LT_01`;;
2337
2338 let OPEN_INTER = theorem `;
2339   ∀s t. open s ∧ open t ⇒ open (s ∩ t)
2340
2341   proof
2342     intro_TAC ∀s t, sOpen tOpen;
2343     rewrite open_def IN_INTER;
2344     intro_TAC ∀x, xs xt;
2345     consider d1 such that
2346     &0 < d1 ∧ ∀x'. dist (x',x) < d1 ⇒ x' ∈ s     [d1Exists] by fol sOpen xs open_def;
2347     consider d2 such that
2348     &0 < d2 ∧ ∀x'. dist (x',x) < d2 ⇒ x' ∈ t     [d2Exists] by fol tOpen xt open_def;
2349     consider e such that &0 < e /\ e < d1 /\ e < d2     [eExists] by fol d1Exists d2Exists REAL_DOWN2;
2350     fol - d1Exists d2Exists REAL_LT_TRANS;
2351   qed;
2352 `;;
2353
2354 let OPEN_UNIONS = theorem `;
2355   (∀s. s ∈ f ⇒ open s)  ⇒  open (UNIONS f)
2356   by fol open_def IN_UNIONS`;;
2357
2358 let IstopologyEuclidean = theorem `;
2359     istopology (UNIV, open)
2360     by simplify istopology IN IN_UNIV SUBSET OPEN_EMPTY OPEN_UNIV OPEN_INTER OPEN_UNIONS`;;
2361
2362 let OPEN_IN = theorem `;
2363   open  =  open_in euclidean
2364   by fol euclidean topology_tybij IstopologyEuclidean TopologyPAIR PAIR_EQ`;;
2365
2366 let TOPSPACE_EUCLIDEAN = theorem `;
2367   topspace euclidean = UNIV
2368   by fol euclidean IstopologyEuclidean topology_tybij TopologyPAIR PAIR_EQ`;;
2369
2370 let OPEN_EXISTS_IN = theorem `;
2371   ∀P Q.  (∀a. P a ⇒ open {x | Q a x})  ⇒  open {x | ∃a. P a ∧ Q a x}
2372   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN OPEN_IN OPEN_IN_EXISTS_IN`;;
2373
2374 let OPEN_EXISTS = theorem `;
2375   ∀Q.  (∀a. open {x | Q a x})  ⇒  open {x | ∃a. Q a x}
2376
2377   proof
2378     intro_TAC ∀Q;
2379     (∀a. T ⇒ open {x | Q a x}) ⇒ open {x | ∃a. T ∧ Q a x}     [] by simplify OPEN_EXISTS_IN;
2380     MP_TAC -;
2381     fol;
2382   qed;
2383 `;;
2384
2385 let TOPSPACE_EUCLIDEAN_SUBTOPOLOGY = theorem `;
2386  ∀s. topspace (subtopology euclidean s) = s
2387   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN TopspaceSubtopology`;;
2388
2389 let OPEN_IN_REFL = theorem `;
2390   ∀s. open_in (subtopology euclidean s) s
2391   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN OpenInRefl`;;
2392
2393 let CLOSED_IN_REFL = theorem `;
2394   ∀s. closed_in (subtopology euclidean s) s
2395   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosedInRefl`;;
2396
2397 let CLOSED_IN = theorem `;
2398   ∀s. closed  =  closed_in euclidean
2399   by fol closed closed_in TOPSPACE_EUCLIDEAN OPEN_IN SUBSET_UNIV EXTENSION IN`;;
2400
2401 let OPEN_UNION = theorem `;
2402   ∀s t.  open s ∧ open t  ⇒  open(s ∪ t)
2403   by fol OPEN_IN OPEN_IN_UNION`;;
2404
2405 let OPEN_SUBOPEN = theorem `;
2406   ∀s. open s ⇔ ∀x. x ∈ s ⇒ ∃t. open t ∧ x ∈ t ∧ t ⊂ s
2407   by fol OPEN_IN OPEN_IN_SUBOPEN`;;
2408
2409 let CLOSED_EMPTY = theorem `;
2410   closed ∅
2411   by fol CLOSED_IN CLOSED_IN_EMPTY`;;
2412
2413 let CLOSED_UNIV = theorem `;
2414   closed UNIV
2415   by fol CLOSED_IN TOPSPACE_EUCLIDEAN CLOSED_IN_TOPSPACE`;;
2416
2417 let CLOSED_UNION = theorem `;
2418   ∀s t.  closed s ∧ closed t  ⇒  closed(s ∪ t)
2419   by fol CLOSED_IN CLOSED_IN_UNION`;;
2420
2421 let CLOSED_INTER = theorem `;
2422   ∀s t.  closed s ∧ closed t  ⇒  closed(s ∩ t)
2423   by fol CLOSED_IN CLOSED_IN_INTER`;;
2424
2425 let CLOSED_INTERS = theorem `;
2426   ∀f. (∀s. s ∈ f ⇒ closed s)  ⇒  closed (INTERS f)
2427   by fol CLOSED_IN CLOSED_IN_INTERS INTERS_0 CLOSED_UNIV`;;
2428
2429 let CLOSED_FORALL_IN = theorem `;
2430   ∀P Q.  (∀a. P a ⇒ closed {x | Q a x})
2431     ⇒  closed {x | ∀a. P a ⇒ Q a x}
2432
2433   proof
2434     intro_TAC ∀P Q;
2435     case_split Pnonempty | Pempty by fol;
2436     suppose ¬(P = ∅);
2437       simplify CLOSED_IN Pnonempty CLOSED_IN_FORALL_IN;
2438     end;
2439     suppose P = ∅;
2440       {x | ∀a. P a ⇒ Q a x} = UNIV     [] by set Pempty;
2441       simplify - CLOSED_UNIV;
2442     end;
2443   qed;
2444 `;;
2445
2446 let CLOSED_FORALL = theorem `;
2447   ∀Q. (∀a. closed {x | Q a x}) ⇒ closed {x | ∀a. Q a x}
2448
2449   proof
2450     intro_TAC ∀Q;
2451     (∀a. T ⇒ closed {x | Q a x}) ⇒ closed {x | ∀a. T ⇒ Q a x}     [] by simplify CLOSED_FORALL_IN;
2452     MP_TAC -;
2453     fol;
2454   qed;
2455 `;;
2456
2457 let OPEN_CLOSED = theorem `;
2458   ∀s.  open s  ⇔  closed(UNIV ━ s)
2459   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN OPEN_IN CLOSED_IN OPEN_IN_CLOSED_IN`;;
2460
2461 let OPEN_DIFF = theorem `;
2462   ∀s t.  open s ∧ closed t  ⇒  open(s ━ t)
2463   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN OPEN_IN CLOSED_IN OPEN_IN_DIFF`;;
2464
2465 let CLOSED_DIFF = theorem `;
2466   ∀s t.  closed s ∧ open t  ⇒  closed (s ━ t)
2467   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN OPEN_IN CLOSED_IN CLOSED_IN_DIFF`;;
2468
2469 let OPEN_INTERS = theorem `;
2470   ∀s.  FINITE s ∧ (∀t. t ∈ s ⇒ open t)  ⇒  open (INTERS s)
2471   by fol OPEN_IN OPEN_IN_INTERS INTERS_0 OPEN_UNIV`;;
2472
2473 let CLOSED_UNIONS = theorem `;
2474   ∀s.  FINITE s ∧ (∀t. t ∈ s ⇒ closed t)  ⇒  closed (UNIONS s)
2475   by fol CLOSED_IN CLOSED_IN_UNIONS`;;
2476
2477 (* ------------------------------------------------------------------------- *)
2478 (* Open and closed balls and spheres.                                        *)
2479 (* ------------------------------------------------------------------------- *)
2480
2481 let ball = new_definition
2482   `ball(x,e) = {y | dist(x,y) < e}`;;
2483
2484 let cball = new_definition
2485   `cball(x,e) = {y | dist(x,y) <= e}`;;
2486
2487 let IN_BALL = theorem `;
2488  ∀x y e. y ∈ ball(x,e)  ⇔  dist(x,y) < e
2489   by rewrite ball IN_ELIM_THM`;;
2490
2491 let IN_CBALL = theorem `;
2492   ∀x y e. y ∈ cball(x, e)  ⇔  dist(x, y) <= e
2493   by rewrite cball IN_ELIM_THM`;;
2494
2495 let BALL_SUBSET_CBALL = theorem `;
2496   ∀x e. ball (x,e) ⊂ cball (x, e)
2497
2498   proof
2499      rewrite IN_BALL IN_CBALL SUBSET;
2500      real_arithmetic;
2501   qed;
2502 `;;
2503
2504 let OPEN_BALL = theorem `;
2505   ∀x e. open (ball (x,e))
2506
2507   proof
2508     rewrite open_def ball IN_ELIM_THM;
2509     fol DIST_SYM REAL_SUB_LT REAL_LT_SUB_LADD REAL_ADD_SYM REAL_LET_TRANS DIST_TRIANGLE;
2510   qed;
2511 `;;
2512
2513 let CENTRE_IN_BALL = theorem `;
2514   ∀x e. x ∈ ball(x,e)  ⇔  &0 < e
2515   by fol IN_BALL DIST_REFL`;;
2516
2517 let OPEN_CONTAINS_BALL = theorem `;
2518   ∀s. open s  ⇔  ∀x. x ∈ s ⇒ ∃e. &0 < e ∧ ball(x,e) ⊂ s
2519   by rewrite open_def SUBSET IN_BALL DIST_SYM`;;
2520
2521 let HALF_CBALL_IN_BALL = theorem `;
2522   ∀e. &0 < e  ⇒  &0 < e/ &2 ∧ e / &2 < e ∧ cball (x, e/ &2) ⊂ ball (x, e)
2523
2524   proof
2525     intro_TAC ∀e, H1;
2526      &0 < e/ &2  ∧  e / &2 < e     [] by real_arithmetic H1;
2527      fol - SUBSET IN_CBALL IN_BALL REAL_LET_TRANS;
2528   qed;
2529 `;;
2530
2531 let OPEN_IN_CONTAINS_CBALL_LEMMA = theorem `;
2532   ∀t s x.  x ∈ s  ⇒
2533     ((∃e. &0 < e ∧ ball (x, e) ∩ t ⊂ s) ⇔
2534     (∃e. &0 < e ∧ cball (x, e) ∩ t ⊂ s))
2535   by fol BALL_SUBSET_CBALL HALF_CBALL_IN_BALL INTER_TENSOR SUBSET_REFL SUBSET_TRANS`;;
2536
2537 (* ------------------------------------------------------------------------- *)
2538 (* Basic "localization" results are handy for connectedness.                 *)
2539 (* ------------------------------------------------------------------------- *)
2540
2541 let OPEN_IN_OPEN = theorem `;
2542   ∀s u.  open_in (subtopology euclidean u) s  ⇔  ∃t. open t ∧ (s = u ∩ t)
2543   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN OPEN_IN OpenInSubtopology INTER_COMM`;;
2544
2545 let OPEN_IN_INTER_OPEN = theorem `;
2546   ∀s t u.  open_in (subtopology euclidean u) s  ∧  open t
2547     ⇒ open_in (subtopology euclidean u) (s ∩ t)
2548   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN OPEN_IN OpenInSubtopologyInterOpen`;;
2549
2550 let OPEN_IN_OPEN_INTER = theorem `;
2551   ∀u s.  open s  ⇒  open_in (subtopology euclidean u) (u ∩ s)
2552   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN OPEN_IN OpenInOpenInter`;;
2553
2554 let OPEN_OPEN_IN_TRANS = theorem `;
2555   ∀s t.  open s  ∧  open t  ∧  t ⊂ s
2556     ⇒ open_in (subtopology euclidean s) t
2557   by fol OPEN_IN OpenOpenInTrans`;;
2558
2559 let OPEN_SUBSET = theorem `;
2560   ∀s t.  s ⊂ t  ∧  open s  ⇒  open_in (subtopology euclidean t) s
2561   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN OPEN_IN OpenSubset`;;
2562
2563 let CLOSED_IN_CLOSED = theorem `;
2564   ∀s u.
2565     closed_in (subtopology euclidean u) s  ⇔  ∃t. closed t ∧ (s = u ∩ t)
2566   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN ClosedInSubtopology INTER_COMM`;;
2567
2568 let CLOSED_SUBSET_EQ = theorem `;
2569   ∀u s.  closed s  ⇒  (closed_in (subtopology euclidean u) s  ⇔  s ⊂ u)
2570   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN ClosedSubsetEq`;;
2571
2572 let CLOSED_IN_INTER_CLOSED = theorem `;
2573   ∀s t u.  closed_in (subtopology euclidean u) s  ∧  closed t
2574     ⇒ closed_in (subtopology euclidean u) (s ∩ t)
2575   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN ClosedInInterClosed`;;
2576
2577 let CLOSED_IN_CLOSED_INTER = theorem `;
2578   ∀u s. closed s  ⇒  closed_in (subtopology euclidean u) (u ∩ s)
2579   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN ClosedInClosedInter`;;
2580
2581 let CLOSED_SUBSET = theorem `;
2582   ∀s t.  s ⊂ t ∧ closed s  ⇒  closed_in (subtopology euclidean t) s
2583   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN ClosedSubset`;;
2584
2585 let OPEN_IN_SUBSET_TRANS = theorem `;
2586   ∀s t u.  open_in (subtopology euclidean u) s  ∧  s ⊂ t  ∧  t ⊂ u
2587     ⇒ open_in (subtopology euclidean t) s
2588   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN OpenInSubsetTrans`;;
2589
2590 let CLOSED_IN_SUBSET_TRANS = theorem `;
2591   ∀s t u.  closed_in (subtopology euclidean u) s  ∧  s ⊂ t  ∧  t ⊂ u
2592     ⇒ closed_in (subtopology euclidean t) s
2593   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN ClosedInSubsetTrans`;;
2594
2595 let OPEN_IN_CONTAINS_BALL_LEMMA = theorem `;
2596   ∀t s x.  x ∈ s  ⇒
2597     ((∃E. open E  ∧  x ∈ E  ∧  E ∩ t ⊂ s)  ⇔
2598     (∃e. &0 < e  ∧  ball (x,e) ∩ t ⊂ s))
2599
2600   proof
2601     intro_TAC ∀ t s x, xs;
2602     eq_tac     [Right] by fol CENTRE_IN_BALL OPEN_BALL;
2603     intro_TAC H2;
2604     consider a such that
2605     open a ∧ x ∈ a ∧ a ∩ t ⊂ s     [aExists] by fol H2;
2606     consider e such that
2607     &0 < e ∧ ball(x,e) ⊂ a     [eExists] by fol - OPEN_CONTAINS_BALL;
2608     fol aExists - INTER_SUBSET GSYM SUBSET_INTER SUBSET_TRANS;
2609   qed;
2610 `;;
2611
2612 let OPEN_IN_CONTAINS_BALL = theorem `;
2613   ∀s t.  open_in (subtopology euclidean t) s  ⇔
2614     s ⊂ t  ∧  ∀x. x ∈ s ⇒ ∃e. &0 < e ∧ ball(x,e) ∩ t ⊂ s
2615   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN SubtopologyOpenInSubopen GSYM OPEN_IN GSYM OPEN_IN_CONTAINS_BALL_LEMMA`;;
2616
2617 let OPEN_IN_CONTAINS_CBALL = theorem `;
2618   ∀s t.  open_in (subtopology euclidean t) s  ⇔
2619     s ⊂ t  ∧  ∀x. x ∈ s ⇒ ∃e. &0 < e ∧ cball(x,e) ∩ t ⊂ s
2620   by fol OPEN_IN_CONTAINS_BALL OPEN_IN_CONTAINS_CBALL_LEMMA`;;
2621
2622 let open_in = theorem `;
2623   ∀u s.  open_in (subtopology euclidean u) s   ⇔
2624     s ⊂ u  ∧
2625     ∀x. x ∈ s ⇒ ∃e. &0 < e ∧
2626     ∀x'. x' ∈ u ∧ dist(x',x) < e ⇒ x' ∈ s
2627   by rewrite OPEN_IN_CONTAINS_BALL IN_INTER SUBSET IN_BALL CONJ_SYM DIST_SYM`;;
2628
2629 (* ------------------------------------------------------------------------- *)
2630 (* These "transitivity" results are handy too.                               *)
2631 (* ------------------------------------------------------------------------- *)
2632
2633 let OPEN_IN_TRANS = theorem `;
2634   ∀s t u. open_in (subtopology euclidean t) s  ∧
2635     open_in (subtopology euclidean u) t
2636     ⇒ open_in (subtopology euclidean u) s
2637
2638   proof
2639     intro_TAC ∀s t u;
2640     t ⊂ topspace euclidean  ∧  u ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2641     fol - OPEN_IN OpenInTrans;
2642   qed;
2643 `;;
2644
2645 let OPEN_IN_TRANS_EQ = theorem `;
2646   ∀s t.  (∀u. open_in (subtopology euclidean t) u
2647     ⇒  open_in (subtopology euclidean s) t)
2648     ⇔  open_in (subtopology euclidean s) t
2649   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN OpenInTransEq`;;
2650
2651 let OPEN_IN_OPEN_TRANS = theorem `;
2652   ∀u s.  open_in (subtopology euclidean u) s ∧ open u  ⇒  open s
2653
2654   proof
2655     intro_TAC ∀u s, H1;
2656     u ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2657     fol - H1 OPEN_IN OpenInOpenTrans;
2658   qed;
2659 `;;
2660
2661 let CLOSED_IN_TRANS = theorem `;
2662   ∀s t u.  closed_in (subtopology euclidean t) s  ∧
2663     closed_in (subtopology euclidean u) t
2664     ⇒ closed_in (subtopology euclidean u) s
2665
2666   proof
2667     intro_TAC ∀s t u;
2668     t ⊂ topspace euclidean ∧ u ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2669     fol - ClosedInSubtopologyTrans;
2670   qed;
2671 `;;
2672
2673 let CLOSED_IN_TRANS_EQ = theorem `;
2674   ∀s t.
2675     (∀u. closed_in (subtopology euclidean t) u ⇒ closed_in (subtopology euclidean s) t)
2676     ⇔ closed_in (subtopology euclidean s) t
2677   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosedInSubtopologyTransEq`;;
2678
2679 let CLOSED_IN_CLOSED_TRANS = theorem `;
2680   ∀s u. closed_in (subtopology euclidean u) s ∧ closed u ⇒ closed s
2681
2682   proof
2683     intro_TAC ∀u s;
2684     u ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2685     fol - CLOSED_IN ClosedInClosedTrans;
2686   qed;
2687 `;;
2688
2689 let OPEN_IN_SUBTOPOLOGY_INTER_SUBSET = theorem `;
2690   ∀s u v. open_in (subtopology euclidean u) (u ∩ s)  ∧  v ⊂ u
2691     ⇒ open_in (subtopology euclidean v) (v ∩ s)
2692   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN OpenInSubtopologyInterSubset`;;
2693
2694 let OPEN_IN_OPEN_EQ = theorem `;
2695   ∀s t.  open s  ⇒  (open_in (subtopology euclidean s) t ⇔ open t ∧ t ⊂ s)
2696   by fol OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN OpenInOpenEq`;;
2697
2698 let CLOSED_IN_CLOSED_EQ = theorem `;
2699   ∀s t.  closed s  ⇒
2700     (closed_in (subtopology euclidean s) t ⇔ closed t ∧ t ⊂ s)
2701   by fol CLOSED_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosedInClosedEq`;;
2702
2703 (* ------------------------------------------------------------------------- *)
2704 (* Also some invariance theorems for relative topology.                      *)
2705 (* ------------------------------------------------------------------------- *)
2706
2707 let OPEN_IN_INJECTIVE_LINEAR_IMAGE = theorem `;
2708   ∀f s t.  linear f ∧ (∀x y. f x = f y ⇒ x = y) ⇒
2709     (open_in (subtopology euclidean (IMAGE f t)) (IMAGE f s) ⇔
2710     open_in (subtopology euclidean t) s)
2711
2712   proof
2713     rewrite open_in FORALL_IN_IMAGE IMP_CONJ SUBSET;
2714     intro_TAC ∀f s t, H1, H2;
2715     ∀x s. f x ∈ IMAGE f s ⇔ x ∈ s     [fInjMap] by set H2;
2716     rewrite -;
2717     ∀x y. f x - f y = f (x - y)     [fSubLinear] by fol H1 LINEAR_SUB;
2718     consider B1 such that
2719     &0 < B1  ∧  ∀x. norm (f x) <= B1 * norm x     [B1exists] by fol H1 LINEAR_BOUNDED_POS;
2720     consider B2 such that
2721     &0 < B2  ∧  ∀x. norm x * B2 <= norm (f x)     [B2exists] by fol H1 H2 LINEAR_INJECTIVE_BOUNDED_BELOW_POS;
2722     AP_TERM_TAC;
2723     eq_tac     [Left]
2724     proof
2725       intro_TAC H3, ∀x, xs;
2726       consider e such that
2727       &0 < e  ∧  ∀x'. x' ∈ t ⇒ dist (f x',f x) < e ⇒ x' ∈ s     [eExists] by fol H3 xs;
2728       exists_TAC e / B1;
2729       simplify REAL_LT_DIV eExists B1exists;
2730       intro_TAC ∀x', x't;
2731       ∀x. norm(f x) <= B1 * norm(x)  ∧ norm(x) * B1 < e  ⇒  norm(f x) < e     [normB1] by real_arithmetic;
2732       simplify fSubLinear B1exists H3 eExists x't normB1 dist REAL_LT_RDIV_EQ;
2733     qed;
2734     intro_TAC H3, ∀x, xs;
2735     consider e such that
2736     &0 < e  ∧  ∀x'. x' ∈ t ⇒ dist (x',x) < e ⇒ x' ∈ s     [eExists] by fol H3 xs;
2737     exists_TAC e * B2;
2738     simplify REAL_LT_MUL eExists B2exists;
2739     intro_TAC ∀x', x't;
2740     ∀x. norm x <= norm (f x) / B2 ∧ norm(f x) / B2 < e  ⇒  norm x < e     [normB2] by real_arithmetic;
2741     simplify fSubLinear B2exists H3 eExists x't normB2 dist REAL_LE_RDIV_EQ REAL_LT_LDIV_EQ;
2742   qed;
2743 `;;
2744
2745 add_linear_invariants [OPEN_IN_INJECTIVE_LINEAR_IMAGE];;
2746
2747 let CLOSED_IN_INJECTIVE_LINEAR_IMAGE = theorem `;
2748   ∀f s t. linear f ∧ (∀x y. f x = f y ⇒ x = y)  ⇒
2749     (closed_in (subtopology euclidean (IMAGE f t)) (IMAGE f s)  ⇔
2750     closed_in (subtopology euclidean t) s)
2751
2752   proof
2753     rewrite closed_in TOPSPACE_EUCLIDEAN_SUBTOPOLOGY;
2754     GEOM_TRANSFORM_TAC[];
2755   qed;
2756 `;;
2757
2758 add_linear_invariants [CLOSED_IN_INJECTIVE_LINEAR_IMAGE];;
2759
2760 (* ------------------------------------------------------------------------- *)
2761 (* Subspace topology results only proved for Euclidean space.                *)
2762 (* ------------------------------------------------------------------------- *)
2763
2764 (* ISTOPLOGY_SUBTOPOLOGY can not be proved, as the definition of topology    *)
2765 (* there is different from the one here.                                     *)
2766
2767 let OPEN_IN_SUBTOPOLOGY = theorem `;
2768   ∀u s.  open_in (subtopology euclidean u) s  ⇔
2769     ∃t. open_in euclidean t ∧ s = t ∩ u
2770   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN OpenInSubtopology`;;
2771
2772 let TOPSPACE_SUBTOPOLOGY = theorem `;
2773   ∀u.  topspace(subtopology euclidean u) = topspace euclidean ∩ u
2774
2775   proof
2776     intro_TAC ∀u;
2777     u ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2778     fol - TopspaceSubtopology INTER_COMM SUBSET_INTER_ABSORPTION;
2779   qed;
2780 `;;
2781
2782 let CLOSED_IN_SUBTOPOLOGY = theorem `;
2783   ∀u s. closed_in (subtopology euclidean u) s  ⇔
2784   ∃t. closed_in euclidean t ∧ s = t ∩ u
2785   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closed_in ClosedInSubtopology`;;
2786
2787 let OPEN_IN_SUBTOPOLOGY_REFL = theorem `;
2788   ∀u. open_in (subtopology euclidean u) u  ⇔  u ⊂ topspace euclidean
2789   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN OPEN_IN_REFL`;;
2790
2791 let CLOSED_IN_SUBTOPOLOGY_REFL = theorem `;
2792   ∀u. closed_in (subtopology euclidean u) u  ⇔  u ⊂ topspace euclidean
2793   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN_REFL`;;
2794
2795 let SUBTOPOLOGY_UNIV = theorem `;
2796   subtopology euclidean UNIV = euclidean
2797
2798   proof
2799     rewrite GSYM Topology_Eq;
2800     conj_tac     [Left] by fol TOPSPACE_EUCLIDEAN TOPSPACE_EUCLIDEAN_SUBTOPOLOGY;
2801     rewrite GSYM OPEN_IN OPEN_IN_OPEN INTER_UNIV;
2802     fol;
2803   qed;
2804 `;;
2805
2806 let SUBTOPOLOGY_SUPERSET = theorem `;
2807   ∀s.  topspace euclidean ⊂ s  ⇒  subtopology euclidean s = euclidean
2808   by simplify TOPSPACE_EUCLIDEAN UNIV_SUBSET SUBTOPOLOGY_UNIV`;;
2809
2810 let OPEN_IN_IMP_SUBSET = theorem `;
2811   ∀s t.  open_in (subtopology euclidean s) t  ⇒  t ⊂ s
2812   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN OpenInImpSubset`;;
2813
2814 let CLOSED_IN_IMP_SUBSET = theorem `;
2815   ∀s t.  closed_in (subtopology euclidean s) t  ⇒  t ⊂ s
2816   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosedInImpSubset`;;
2817
2818 let OPEN_IN_SUBTOPOLOGY_UNION = theorem `;
2819   ∀s t u.  open_in (subtopology euclidean t) s  ∧
2820     open_in (subtopology euclidean u) s
2821     ⇒  open_in (subtopology euclidean (t ∪ u)) s
2822   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN OpenInSubtopologyUnion`;;
2823
2824 let CLOSED_IN_SUBTOPOLOGY_UNION = theorem `;
2825   ∀s t u.  closed_in (subtopology euclidean t) s  ∧
2826     closed_in (subtopology euclidean u) s
2827     ⇒  closed_in (subtopology euclidean (t ∪ u)) s
2828   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosedInSubtopologyUnion`;;
2829
2830 (* ------------------------------------------------------------------------- *)
2831 (* Connectedness.                                                            *)
2832 (* ------------------------------------------------------------------------- *)
2833
2834 let connected_DEF = NewDefinition `;
2835   connected s  ⇔  Connected (subtopology euclidean s)`;;
2836
2837 let connected = theorem `;
2838   ∀s.  connected s  ⇔  ¬(∃e1 e2.
2839     open e1  ∧  open e2  ∧  s ⊂ e1 ∪ e2  ∧
2840     e1 ∩ e2 ∩ s = ∅  ∧  ¬(e1 ∩ s = ∅)  ∧  ¬(e2 ∩ s = ∅))
2841   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN connected_DEF OPEN_IN ConnectedSubtopology`;;
2842
2843 let CONNECTED_CLOSED = theorem `;
2844   ∀s.  connected s ⇔
2845     ¬(∃e1 e2. closed e1  ∧  closed e2  ∧  s ⊂ e1 ∪ e2  ∧
2846     e1 ∩ e2 ∩ s = ∅  ∧  ¬(e1 ∩ s = ∅)  ∧  ¬(e2 ∩ s = ∅))
2847   by simplify connected_DEF CLOSED_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN connected_DEF CLOSED_IN ConnectedClosedSubtopology`;;
2848
2849 let CONNECTED_OPEN_IN = theorem `;
2850   ∀s. connected s  ⇔  ¬(∃e1 e2.
2851     open_in (subtopology euclidean s) e1 ∧
2852     open_in (subtopology euclidean s) e2 ∧
2853     s ⊂ e1 ∪ e2  ∧  e1 ∩ e2 = ∅  ∧  ¬(e1 = ∅)  ∧  ¬(e2 = ∅))
2854   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN connected_DEF OPEN_IN ConnectedOpenIn`;;
2855
2856 let CONNECTED_OPEN_IN_EQ = theorem `;
2857   ∀s. connected s  ⇔  ¬(∃e1 e2.
2858     open_in (subtopology euclidean s) e1 ∧
2859     open_in (subtopology euclidean s) e2 ∧
2860     e1 ∪ e2 = s ∧ e1 ∩ e2 = ∅ ∧
2861     ¬(e1 = ∅) ∧ ¬(e2 = ∅))
2862   by simplify connected_DEF Connected_DEF SUBSET_UNIV TOPSPACE_EUCLIDEAN TopspaceSubtopology EQ_SYM_EQ`;;
2863
2864 let CONNECTED_CLOSED_IN = theorem `;
2865   ∀s. connected s  ⇔  ¬(∃e1 e2.
2866     closed_in (subtopology euclidean s) e1 ∧
2867     closed_in (subtopology euclidean s) e2 ∧
2868     s ⊂ e1 ∪ e2  ∧  e1 ∩ e2 = ∅  ∧  ¬(e1 = ∅)  ∧  ¬(e2 = ∅))
2869   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN connected_DEF CLOSED_IN ConnectedClosedIn`;;
2870
2871 let CONNECTED_CLOSED_IN_EQ = theorem `;
2872   ∀s. connected s  ⇔  ¬(∃e1 e2.
2873     closed_in (subtopology euclidean s) e1  ∧
2874     closed_in (subtopology euclidean s) e2  ∧
2875     e1 ∪ e2 = s  ∧  e1 ∩ e2 = ∅  ∧  ¬(e1 = ∅)  ∧  ¬(e2 = ∅))
2876   by simplify connected_DEF ConnectedClosed SUBSET_UNIV TOPSPACE_EUCLIDEAN TopspaceSubtopology EQ_SYM_EQ`;;
2877
2878 let CONNECTED_CLOPEN = theorem `;
2879   ∀s. connected s  ⇔
2880     ∀t. open_in (subtopology euclidean s) t  ∧
2881       closed_in (subtopology euclidean s) t ⇒ t = ∅ ∨ t = s
2882   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN connected_DEF ConnectedClopen TopspaceSubtopology`;;
2883
2884 let CONNECTED_CLOSED_SET = theorem `;
2885   ∀s.  closed s ⇒
2886     (connected s  ⇔
2887     ¬(∃e1 e2. closed e1 ∧ closed e2 ∧
2888     ¬(e1 = ∅)  ∧  ¬(e2 = ∅)  ∧  e1 ∪ e2 = s  ∧  e1 ∩ e2 = ∅))
2889   by simplify connected_DEF CLOSED_IN  closed_in ConnectedClosedSet`;;
2890
2891 let CONNECTED_OPEN_SET = theorem `;
2892   ∀s.  open s  ⇒
2893     (connected s ⇔
2894     ¬(∃e1 e2.  open e1  ∧  open e2  ∧
2895     ¬(e1 = ∅)  ∧  ¬(e2 = ∅)  ∧  e1 ∪ e2 = s  ∧  e1 ∩ e2 = ∅))
2896   by simplify connected_DEF OPEN_IN ConnectedOpenSet`;;
2897
2898 let CONNECTED_EMPTY = theorem `;
2899   connected ∅
2900   by rewrite connected_DEF ConnectedEmpty`;;
2901
2902 let CONNECTED_SING = theorem `;
2903   ∀a. connected {a}
2904
2905   proof
2906     intro_TAC ∀a;
2907     a ∈ topspace euclidean     [] by fol IN_UNIV TOPSPACE_EUCLIDEAN;
2908     fol - ConnectedSing connected_DEF;
2909   qed;
2910 `;;
2911
2912 let CONNECTED_UNIONS = theorem `;
2913   ∀P.  (∀s. s ∈ P ⇒ connected s) ∧ ¬(INTERS P = ∅)
2914     ⇒ connected(UNIONS P)
2915
2916   proof
2917     intro_TAC ∀P;
2918     ∀s. s ∈ P ⇒ s ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2919     fol - connected_DEF ConnectedUnions;
2920   qed;
2921 `;;
2922
2923 let CONNECTED_UNION = theorem `;
2924   ∀s t.  connected s  ∧  connected t  ∧  ¬(s ∩ t = ∅)
2925     ⇒ connected (s ∪ t)
2926
2927   proof
2928     intro_TAC ∀s t;
2929     s ⊂ topspace euclidean  ∧  t ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2930     fol - connected_DEF ConnectedUnion;
2931   qed;
2932 `;;
2933
2934 let CONNECTED_DIFF_OPEN_FROM_CLOSED = theorem `;
2935   ∀s t u.  s ⊂ t  ∧  t ⊂ u  ∧  open s  ∧  closed t  ∧
2936     connected u ∧ connected(t ━ s)
2937     ⇒  connected(u ━ s)
2938   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN connected_DEF OPEN_IN CLOSED_IN ConnectedDiffOpenFromClosed`;;
2939
2940 let CONNECTED_DISJOINT_UNIONS_OPEN_UNIQUE = theorem `;
2941   ∀f f'.  pairwise DISJOINT f ∧ pairwise DISJOINT f' ∧
2942     (∀s. s ∈ f ⇒ open s ∧ connected s ∧ ¬(s = ∅)) ∧
2943     (∀s. s ∈ f' ⇒ open s ∧ connected s ∧ ¬(s = ∅)) ∧
2944     UNIONS f = UNIONS f'
2945     ⇒ f = f'
2946   by rewrite connected_DEF OPEN_IN ConnectedDisjointUnionsOpenUnique`;;
2947
2948 let CONNECTED_FROM_CLOSED_UNION_AND_INTER = theorem `;
2949   ∀s t.  closed s ∧ closed t ∧ connected (s ∪ t) ∧ connected (s ∩ t)
2950     ⇒ connected s ∧ connected t
2951
2952   proof
2953     intro_TAC ∀s t;
2954     s ∪ t ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2955     fol -  connected_DEF CLOSED_IN ConnectedFromClosedUnionAndInter;
2956   qed;
2957 `;;
2958
2959 let CONNECTED_FROM_OPEN_UNION_AND_INTER = theorem `;
2960   ∀s t.  open s ∧ open t ∧ connected (s ∪ t) ∧ connected (s ∩ t)
2961     ⇒ connected s ∧ connected t
2962
2963   proof
2964     intro_TAC ∀s t;
2965     s ∪ t ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2966     fol -  connected_DEF OPEN_IN ConnectedFromOpenUnionAndInter;
2967   qed;
2968 `;;
2969
2970 (* ------------------------------------------------------------------------- *)
2971 (* Sort of induction principle for connected sets.                           *)
2972 (* ------------------------------------------------------------------------- *)
2973
2974 let CONNECTED_INDUCTION = theorem `;
2975   ∀P Q s.  connected s ∧
2976     (∀t a. open_in (subtopology euclidean s) t ∧ a ∈ t  ⇒  ∃z. z ∈ t ∧ P z) ∧
2977     (∀a. a ∈ s  ⇒  ∃t. open_in (subtopology euclidean s) t ∧ a ∈ t ∧
2978     ∀x y. x ∈ t ∧ y ∈ t ∧ P x ∧ P y ∧ Q x ⇒ Q y)
2979     ⇒ ∀a b. a ∈ s ∧ b ∈ s ∧ P a ∧ P b ∧ Q a ⇒ Q b
2980
2981   proof
2982     intro_TAC ∀P Q s;
2983     s ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2984     MP_TAC -;
2985     rewrite connected_DEF ConnectedInduction;
2986   qed;
2987 `;;
2988
2989 let CONNECTED_EQUIVALENCE_RELATION_GEN_LEMMA = theorem `;
2990   ∀P R s.
2991         connected s ∧
2992         (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
2993         (∀t a. open_in (subtopology euclidean s) t ∧ a ∈ t
2994                ⇒ ∃z. z ∈ t ∧ P z) ∧
2995         (∀a. a ∈ s
2996              ⇒ ∃t. open_in (subtopology euclidean s) t ∧ a ∈ t ∧
2997                      ∀x y. x ∈ t ∧ y ∈ t ∧ P x ∧ P y ⇒ R x y)
2998         ⇒ ∀a b. a ∈ s ∧ b ∈ s ∧ P a ∧ P b ⇒ R a b
2999
3000   proof
3001     intro_TAC ∀P R s;
3002     s ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
3003     MP_TAC -;
3004     rewrite connected_DEF ConnectedEquivalenceRelationGen;
3005   qed;
3006 `;;
3007
3008 let CONNECTED_EQUIVALENCE_RELATION_GEN = theorem `;
3009   ∀P R s.
3010         connected s ∧
3011         (∀x y. R x y ⇒ R y x) ∧
3012         (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
3013         (∀t a. open_in (subtopology euclidean s) t ∧ a ∈ t
3014                ⇒ ∃z. z ∈ t ∧ P z) ∧
3015         (∀a. a ∈ s
3016              ⇒ ∃t. open_in (subtopology euclidean s) t ∧ a ∈ t ∧
3017                      ∀x y. x ∈ t ∧ y ∈ t ∧ P x ∧ P y ⇒ R x y)
3018         ⇒ ∀a b. a ∈ s ∧ b ∈ s ∧ P a ∧ P b ⇒ R a b
3019
3020   proof
3021     intro_TAC ∀P R s;
3022     MP_TAC ISPECL [P; R; s] CONNECTED_EQUIVALENCE_RELATION_GEN_LEMMA;
3023     fol;
3024   qed;
3025 `;;
3026
3027 let CONNECTED_INDUCTION_SIMPLE = theorem `;
3028   ∀P s.  connected s ∧ (∀a. a ∈ s
3029     ⇒ ∃t. open_in (subtopology euclidean s) t ∧ a ∈ t ∧
3030     ∀x y. x ∈ t ∧ y ∈ t ∧ P x ⇒ P y)
3031     ⇒ ∀a b. a ∈ s ∧ b ∈ s ∧ P a ⇒ P b
3032
3033   proof
3034     intro_TAC ∀P s;
3035     s ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
3036     MP_TAC -;
3037     rewrite connected_DEF ConnectedInductionSimple;
3038   qed;
3039 `;;
3040
3041 let CONNECTED_EQUIVALENCE_RELATION = theorem `;
3042   ∀R s.  connected s ∧
3043     (∀x y. R x y ⇒ R y x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
3044     (∀a. a ∈ s
3045     ⇒ ∃t. open_in (subtopology euclidean s) t ∧ a ∈ t ∧ ∀x. x ∈ t ⇒ R a x)
3046     ⇒ ∀a b. a ∈ s ∧ b ∈ s ⇒ R a b
3047
3048   proof
3049     intro_TAC ∀R s;
3050     s ⊂ topspace euclidean     [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
3051     MP_TAC -;
3052     rewrite connected_DEF ConnectedEquivalenceRelation;
3053   qed;
3054 `;;
3055
3056 (* ------------------------------------------------------------------------- *)
3057 (* Limit points.                                                             *)
3058 (* ------------------------------------------------------------------------- *)
3059
3060 parse_as_infix ("limit_point_of",(12,"right"));;
3061
3062 let limit_point_of_DEF = NewDefinition `;
3063   x limit_point_of s  ⇔  x ∈ LimitPointOf euclidean s`;;
3064
3065 let limit_point_of = theorem `;
3066   x limit_point_of s  ⇔
3067     ∀t. x ∈ t ∧ open t  ⇒  ∃y. ¬(y = x) ∧ y ∈ s ∧ y ∈ t
3068   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN IN_UNIV IN_LimitPointOf limit_point_of_DEF OPEN_IN`;;
3069
3070 let LIMPT_SUBSET = theorem `;
3071   ∀x s t.  x limit_point_of s ∧ s ⊂ t  ⇒  x limit_point_of t
3072   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN limit_point_of_DEF LimptSubset SUBSET`;;
3073
3074 let CLOSED_LIMPT = theorem `;
3075   ∀s.  closed s  ⇔  ∀x. x limit_point_of s ⇒ x ∈ s
3076   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN IN_UNIV limit_point_of_DEF CLOSED_IN ClosedLimpt SUBSET`;;
3077
3078 let LIMPT_EMPTY = theorem `;
3079   ∀x.  ¬(x limit_point_of ∅)
3080   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN IN_UNIV limit_point_of_DEF GSYM ∉ LimptEmpty`;;
3081
3082 let NO_LIMIT_POINT_IMP_CLOSED = theorem `;
3083   ∀s. ¬(∃x. x limit_point_of s) ⇒ closed s
3084   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN IN_UNIV limit_point_of_DEF CLOSED_IN NoLimitPointImpClosed NOT_EXISTS_THM ∉`;;
3085
3086 let LIMIT_POINT_UNION = theorem `;
3087   ∀s t x.  x limit_point_of (s ∪ t)  ⇔
3088     x limit_point_of s  ∨  x limit_point_of t
3089   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN IN_UNIV limit_point_of_DEF LimitPointUnion EXTENSION IN_UNION`;;
3090
3091 let LimitPointOf_euclidean = theorem `;
3092   ∀s.  LimitPointOf euclidean s = {x | x limit_point_of s}
3093   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN IN_UNIV limit_point_of_DEF LimitPointOf IN_ELIM_THM EXTENSION`;;
3094
3095 (* ------------------------------------------------------------------------- *)
3096 (* Interior of a set.                                                        *)
3097 (* ------------------------------------------------------------------------- *)
3098
3099 let interior_DEF = NewDefinition `;
3100   interior = Interior euclidean`;;
3101
3102 let interior = theorem `;
3103   ∀s. interior s = {x | ∃t. open t ∧ x ∈ t ∧ t ⊂ s}
3104   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF Interior_DEF OPEN_IN`;;
3105
3106 let INTERIOR_EQ = theorem `;
3107   ∀s.  interior s = s  ⇔  open s
3108   by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorEq EQ_SYM_EQ`;;
3109
3110 let INTERIOR_OPEN = theorem `;
3111   ∀s.  open s  ⇒  interior s = s
3112   by fol interior_DEF OPEN_IN InteriorOpen`;;
3113
3114 let INTERIOR_EMPTY = theorem `;
3115   interior ∅ = ∅
3116   by fol interior_DEF OPEN_IN InteriorEmpty`;;
3117
3118 let INTERIOR_UNIV = theorem `;
3119   interior UNIV = UNIV
3120   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF InteriorUniv`;;
3121
3122 let OPEN_INTERIOR = theorem `;
3123   ∀s. open (interior s)
3124   by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN  OpenInterior`;;
3125
3126 let INTERIOR_INTERIOR = theorem `;
3127   ∀s. interior (interior s) = interior s
3128   by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN  InteriorInterior`;;
3129
3130 let INTERIOR_SUBSET = theorem `;
3131   ∀s. interior s ⊂ s
3132   by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN  InteriorSubset`;;
3133
3134 let SUBSET_INTERIOR = theorem `;
3135   ∀s t.  s ⊂ t  ⇒  interior s ⊂ interior t
3136   by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN SubsetInterior`;;
3137
3138 let INTERIOR_MAXIMAL = theorem `;
3139   ∀s t.  t ⊂ s ∧ open t  ⇒  t ⊂ interior s
3140   by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorMaximal`;;
3141
3142 let INTERIOR_MAXIMAL_EQ = theorem `;
3143   ∀s t.  open s  ⇒  (s ⊂ interior t ⇔ s ⊂ t)
3144   by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorMaximalEq`;;
3145
3146 let INTERIOR_UNIQUE = theorem `;
3147   ∀s t.  t ⊂ s  ∧  open t ∧  (∀t'. t' ⊂ s ∧ open t' ⇒ t' ⊂ t)
3148     ⇒ interior s = t
3149   by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorUnique`;;
3150
3151 let IN_INTERIOR = theorem `;
3152   ∀x s.  x ∈ interior s  ⇔  ∃e. &0 < e ∧ ball(x,e) ⊂ s
3153
3154   proof
3155     simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF IN_Interior GSYM OPEN_IN;
3156     fol OPEN_CONTAINS_BALL SUBSET_TRANS CENTRE_IN_BALL OPEN_BALL;
3157   qed;
3158 `;;
3159
3160 let OPEN_SUBSET_INTERIOR = theorem `;
3161   ∀s t.  open s  ⇒  (s ⊂ interior t  ⇔  s ⊂ t)
3162   by fol interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN OpenSubsetInterior`;;
3163
3164 let INTERIOR_INTER = theorem `;
3165   ∀s t. interior (s ∩ t) = interior s ∩ interior t
3166   by simplify interior_DEF SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorInter`;;
3167
3168 let INTERIOR_FINITE_INTERS = theorem `;
3169   ∀s.  FINITE s  ⇒  interior (INTERS s) = INTERS (IMAGE interior s)
3170
3171   proof
3172   intro_TAC ∀s, H1;
3173   assume ¬(s = ∅)     [sNonempty] by simplify INTERS_0 IMAGE_CLAUSES INTERIOR_UNIV;
3174       simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN H1 sNonempty interior_DEF InteriorFiniteInters;
3175   qed;
3176 `;;
3177
3178 let INTERIOR_FINITE_INTERS = theorem `;
3179   ∀s.  FINITE s  ⇒  interior (INTERS s) = INTERS (IMAGE interior s)
3180
3181   proof
3182   intro_TAC ∀s, H1;
3183   assume s = ∅     [sEmpty] by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN H1 interior_DEF InteriorFiniteInters;
3184   rewrite INTERS_0 IMAGE_CLAUSES sEmpty INTERIOR_UNIV;
3185   qed;
3186 `;;
3187
3188 let INTERIOR_INTERS_SUBSET = theorem `;
3189   ∀f.  interior (INTERS f) ⊂ INTERS (IMAGE interior f)
3190
3191   proof
3192     intro_TAC ∀f;
3193     assume f = ∅     [fEmpty] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF InteriorIntersSubset;
3194     rewrite INTERS_0 IMAGE_CLAUSES - INTERIOR_UNIV SUBSET_REFL;
3195   qed;
3196 `;;
3197
3198 let UNION_INTERIOR_SUBSET = theorem `;
3199   ∀s t.  interior s ∪ interior t  ⊂  interior(s ∪ t)
3200   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF UnionInteriorSubset`;;
3201
3202 let INTERIOR_EQ_EMPTY = theorem `;
3203   ∀s.  interior s = ∅  ⇔  ∀t. open t ∧ t ⊂ s ⇒ t = ∅
3204   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF OPEN_IN InteriorEqEmpty`;;
3205
3206 let INTERIOR_EQ_EMPTY_ALT = theorem `;
3207   ∀s.  interior s = ∅  ⇔  ∀t. open t ∧ ¬(t = ∅) ⇒ ¬(t ━ s = ∅)
3208   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF OPEN_IN InteriorEqEmptyAlt`;;
3209
3210 let INTERIOR_UNIONS_OPEN_SUBSETS = theorem `;
3211   ∀s.  UNIONS {t | open t ∧ t ⊂ s} = interior s
3212   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF OPEN_IN InteriorUnionsOpenSubsets`;;
3213
3214 (* ------------------------------------------------------------------------- *)
3215 (* Closure of a set.                                                         *)
3216 (* ------------------------------------------------------------------------- *)
3217
3218 let closure_DEF = NewDefinition `;
3219   closure = Closure euclidean`;;
3220
3221 let closure = theorem `;
3222   ∀s.  closure s = s UNION {x | x limit_point_of s}
3223   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF LimitPointOf_euclidean Closure_THM`;;
3224
3225 let CLOSURE_INTERIOR = theorem `;
3226   ∀s. closure s = UNIV ━ interior (UNIV ━ s)
3227
3228   proof
3229     rewrite closure_DEF GSYM TOPSPACE_EUCLIDEAN interior_DEF;
3230     simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosureInterior;
3231   qed;
3232 `;;
3233
3234 let INTERIOR_CLOSURE = theorem `;
3235   ∀s.  interior s = UNIV ━ (closure (UNIV ━ s))
3236
3237   proof
3238     rewrite closure_DEF GSYM TOPSPACE_EUCLIDEAN  interior_DEF;
3239     simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorClosure;
3240   qed;
3241 `;;
3242
3243 let CLOSED_CLOSURE = theorem `;
3244   ∀s.  closed (closure s)
3245   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosedClosure`;;
3246
3247 let CLOSURE_SUBSET = theorem `;
3248   ∀s.  s ⊂ closure s
3249   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureSubset`;;
3250
3251 let SUBSET_CLOSURE = theorem `;
3252   ∀s t.  s ⊂ t  ⇒  closure s ⊂ closure t
3253   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF SubsetClosure`;;
3254
3255 let CLOSURE_HULL = theorem `;
3256   ∀s. closure s = closed hull s
3257   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureHull`;;
3258
3259 let CLOSURE_EQ = theorem `;
3260   ∀s.  closure s = s  ⇔  closed s
3261   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureEq`;;
3262
3263 let CLOSURE_CLOSED = theorem `;
3264   ∀s.  closed s  ⇒  closure s = s
3265   by fol CLOSED_IN closure_DEF ClosureClosed`;;
3266
3267 let CLOSURE_CLOSURE = theorem `;
3268   ∀s.  closure (closure s) = closure s
3269   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureClosure`;;
3270
3271 let CLOSURE_UNION = theorem `;
3272   ∀s t.  closure (s ∪ t)  =  closure s ∪ closure t
3273   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureUnion`;;
3274
3275 let CLOSURE_INTER_SUBSET = theorem `;
3276   ∀s t.  closure (s ∩ t)  ⊂  closure s ∩ closure t
3277   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureInterSubset`;;
3278
3279 let CLOSURE_INTERS_SUBSET = theorem `;
3280   ∀f.  closure (INTERS f)  ⊂  INTERS (IMAGE closure f)
3281   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureIntersSubset`;;
3282
3283 let CLOSURE_MINIMAL = theorem `;
3284   ∀s t.  s ⊂ t ∧ closed t  ⇒  closure s ⊂ t
3285   by fol CLOSED_IN closure_DEF ClosureMinimal`;;
3286
3287 let CLOSURE_MINIMAL_EQ = theorem `;
3288   ∀s t.  closed t  ⇒  (closure s ⊂ t ⇔ s ⊂ t)
3289   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureMinimalEq`;;
3290
3291 let CLOSURE_UNIQUE = theorem `;
3292   ∀s t.  s ⊂ t ∧ closed t ∧ (∀t'. s ⊂ t' ∧ closed t' ⇒ t ⊂ t')
3293     ⇒ closure s = t
3294   by fol CLOSED_IN closure_DEF ClosureUnique`;;
3295
3296
3297 let CLOSURE_EMPTY = theorem `;
3298   closure ∅ = ∅
3299   by fol closure_DEF ClosureEmpty`;;
3300
3301 let CLOSURE_UNIV = theorem `;
3302   closure UNIV = UNIV
3303   by fol TOPSPACE_EUCLIDEAN closure_DEF ClosureUniv`;;
3304
3305 let CLOSURE_UNIONS = theorem `;
3306   ∀f.  FINITE f  ⇒  closure (UNIONS f) = UNIONS {closure s | s ∈ f}
3307   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF ClosureUnions`;;
3308
3309 let CLOSURE_EQ_EMPTY = theorem `;
3310   ∀s.  closure s = ∅  ⇔  s = ∅
3311   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF ClosureEqEmpty`;;
3312
3313 let CLOSURE_SUBSET_EQ = theorem `;
3314   ∀s.  closure s ⊂ s  ⇔  closed s
3315   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF CLOSED_IN ClosureSubsetEq`;;
3316
3317 let OPEN_INTER_CLOSURE_EQ_EMPTY = theorem `;
3318   ∀s t.  open s  ⇒  (s ∩ closure t = ∅  ⇔  s ∩ t = ∅)
3319   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF OPEN_IN OpenInterClosureEqEmpty`;;
3320
3321 let OPEN_INTER_CLOSURE_SUBSET = theorem `;
3322   ∀s t.  open s  ⇒  s ∩ closure t ⊂ closure (s ∩ t)
3323   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF OPEN_IN OpenInterClosureSubset`;;
3324
3325 let CLOSURE_OPEN_INTER_SUPERSET = theorem `;
3326   ∀s t.  open s ∧ s ⊂ closure t  ⇒  closure (s ∩ t) = closure s
3327   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF OPEN_IN ClosureOpenInterSuperset`;;
3328
3329 let CLOSURE_COMPLEMENT = theorem `;
3330   ∀s.  closure (UNIV ━ s) = UNIV ━ interior s
3331
3332   proof
3333     rewrite closure_DEF GSYM TOPSPACE_EUCLIDEAN  interior_DEF;
3334     simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosureComplement;
3335   qed;
3336 `;;
3337
3338 let INTERIOR_COMPLEMENT = theorem `;
3339   ∀s.  interior (UNIV ━ s) = UNIV ━ closure s
3340
3341   proof
3342     rewrite closure_DEF GSYM TOPSPACE_EUCLIDEAN  interior_DEF;
3343     simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorComplement;
3344   qed;
3345 `;;
3346
3347 let CONNECTED_INTERMEDIATE_CLOSURE = theorem `;
3348   ∀s t.  connected s ∧ s ⊂ t ∧ t ⊂ closure s  ⇒  connected t
3349   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF connected_DEF ConnectedIntermediateClosure`;;
3350
3351 let CONNECTED_CLOSURE = theorem `;
3352   ∀s.  connected s  ⇒  connected (closure s)
3353   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF connected_DEF ConnectedClosure`;;
3354
3355 let CONNECTED_UNION_STRONG = theorem `;
3356   ∀s t.  connected s ∧ connected t ∧ ¬(closure s ∩ t = ∅)
3357         ⇒ connected (s ∪ t)
3358   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF connected_DEF ConnectedUnionStrong`;;
3359
3360 let INTERIOR_DIFF = theorem `;
3361   ∀s t.  interior (s ━ t) = interior s ━ closure t
3362   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF interior_DEF InteriorDiff`;;
3363
3364 let CLOSED_IN_LIMPT = theorem `;
3365   ∀s t.  closed_in (subtopology euclidean t) s  ⇔
3366     s ⊂ t  ∧  ∀x. x limit_point_of s ∧ x ∈ t ⇒ x ∈ s
3367   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF limit_point_of_DEF ClosedInLimpt_ALT`;;
3368
3369 let CLOSED_IN_INTER_CLOSURE = theorem `;
3370   ∀s t.  closed_in (subtopology euclidean s) t  ⇔  s ∩ closure t = t
3371   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF limit_point_of_DEF ClosedInInterClosure`;;
3372
3373 let INTERIOR_CLOSURE_IDEMP = theorem `;
3374   ∀s. interior (closure (interior (closure s))) = interior (closure s)
3375   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF interior_DEF InteriorClosureIdemp`;;
3376
3377 let CLOSURE_INTERIOR_IDEMP = theorem `;
3378   ∀s.  closure (interior (closure (interior s))) = closure (interior s)
3379   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF interior_DEF ClosureInteriorIdemp`;;
3380
3381 let INTERIOR_CLOSED_UNION_EMPTY_INTERIOR = theorem `;
3382   ∀s t.  closed s ∧ interior t = ∅  ⇒  interior (s ∪ t) = interior s
3383   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN interior_DEF InteriorClosedUnionEmptyInterior`;;
3384
3385 let INTERIOR_UNION_EQ_EMPTY = theorem `;
3386   ∀s t.  closed s ∨ closed t
3387         ⇒ (interior (s ∪ t) = ∅  ⇔  interior s = ∅ ∧ interior t = ∅)
3388   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN interior_DEF InteriorUnionEqEmpty`;;
3389
3390 let NOWHERE_DENSE_UNION = theorem `;
3391   ∀s t.  interior (closure (s ∪ t)) = ∅  ⇔
3392         interior (closure s) = ∅  ∧  interior (closure t) = ∅
3393   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF interior_DEF NowhereDenseUnion`;;
3394
3395 let NOWHERE_DENSE = theorem `;
3396   ∀s.  interior (closure s) = ∅ ⇔
3397     ∀t. open t ∧ ¬(t = ∅)  ⇒  ∃u. open u ∧ ¬(u = ∅) ∧ u ⊂ t ∧ u ∩ s = ∅
3398   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF closure_DEF OPEN_IN NowhereDense`;;
3399
3400 let INTERIOR_CLOSURE_INTER_OPEN = theorem `;
3401   ∀s t.  open s ∧ open t ⇒
3402     interior (closure (s ∩ t))  =  interior(closure s) ∩ interior (closure t)
3403   by simplify interior_DEF closure_DEF OPEN_IN InteriorClosureInterOpen`;;
3404
3405 let CLOSURE_INTERIOR_UNION_CLOSED = theorem `;
3406   ∀s t.  closed s ∧ closed t  ⇒
3407     closure (interior (s ∪ t))  = closure (interior s) ∪ closure (interior t)
3408   by simplify interior_DEF closure_DEF CLOSED_IN ClosureInteriorUnionClosed`;;
3409
3410 let REGULAR_OPEN_INTER = theorem `;
3411   ∀s t.  interior (closure s) = s ∧ interior (closure t) = t
3412     ⇒ interior (closure (s ∩ t)) = s ∩ t
3413   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF closure_DEF RegularOpenInter`;;
3414
3415 let REGULAR_CLOSED_UNION = theorem `;
3416   ∀s t.  closure (interior s) = s  ∧  closure (interior t) = t
3417     ⇒  closure (interior (s ∪ t)) = s ∪ t
3418   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF closure_DEF RegularClosedUnion`;;
3419
3420 let DIFF_CLOSURE_SUBSET = theorem `;
3421   ∀s t.  closure s ━ closure t ⊂ closure (s ━ t)
3422   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF DiffClosureSubset`;;
3423
3424 (* ------------------------------------------------------------------------- *)
3425 (* Frontier (aka boundary).                                                  *)
3426 (* ------------------------------------------------------------------------- *)
3427
3428 let frontier_DEF = NewDefinition `;
3429   frontier = Frontier euclidean`;;
3430
3431 let frontier = theorem `;
3432   ∀s.  frontier s = (closure s) DIFF (interior s)
3433   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF closure_DEF interior_DEF Frontier_THM`;;
3434
3435 let FRONTIER_CLOSED = theorem `;
3436   ∀s. closed (frontier s)
3437   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF CLOSED_IN FrontierClosed`;;
3438
3439 let FRONTIER_CLOSURES = theorem `;
3440   ∀s.  frontier s  =  (closure s) ∩ (closure (UNIV ━ s))
3441   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF closure_DEF FrontierClosures`;;
3442
3443 let FRONTIER_STRADDLE = theorem `;
3444   ∀a s.  a ∈ frontier s ⇔  ∀e. &0 < e ⇒
3445     (∃x. x ∈ s ∧ dist(a,x) < e)  ∧  (∃x. ¬(x ∈ s) ∧ dist(a,x) < e)
3446
3447   proof
3448     simplify SUBSET_UNIV IN_UNIV TOPSPACE_EUCLIDEAN frontier_DEF closure_DEF FrontierStraddle GSYM OPEN_IN;
3449     fol IN_BALL SUBSET OPEN_CONTAINS_BALL CENTRE_IN_BALL OPEN_BALL;
3450   qed;
3451 `;;
3452
3453 let FRONTIER_SUBSET_CLOSED = theorem `;
3454   ∀s.  closed s  ⇒  (frontier s) ⊂ s
3455   by fol frontier_DEF CLOSED_IN FrontierSubsetClosed`;;
3456
3457 let FRONTIER_EMPTY = theorem `;
3458   frontier ∅ = ∅
3459   by fol frontier_DEF FrontierEmpty`;;
3460
3461 let FRONTIER_UNIV = theorem `;
3462   frontier UNIV = ∅
3463   by fol frontier_DEF TOPSPACE_EUCLIDEAN FrontierUniv`;;
3464
3465 let FRONTIER_SUBSET_EQ = theorem `;
3466   ∀s. (frontier s) ⊂ s ⇔ closed s
3467   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF CLOSED_IN FrontierSubsetEq`;;
3468
3469 let FRONTIER_COMPLEMENT = theorem `;
3470   ∀s. frontier (UNIV ━ s) = frontier s
3471   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF FrontierComplement`;;
3472
3473 let FRONTIER_DISJOINT_EQ = theorem `;
3474   ∀s.  (frontier s) ∩ s = ∅  ⇔  open s
3475   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF OPEN_IN FrontierDisjointEq`;;
3476
3477 let FRONTIER_INTER_SUBSET = theorem `;
3478   ∀s t.  frontier (s ∩ t)  ⊂  frontier s ∪ frontier t
3479   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF FrontierInterSubset`;;
3480
3481 let FRONTIER_UNION_SUBSET = theorem `;
3482   ∀s t.  frontier (s ∪ t)  ⊂  frontier s ∪ frontier t
3483   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF FrontierUnionSubset`;;
3484
3485 let FRONTIER_INTERIORS = theorem `;
3486   frontier s = UNIV ━ interior(s) ━ interior(UNIV ━ s)
3487   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF interior_DEF FrontierInteriors`;;
3488
3489 let FRONTIER_FRONTIER_SUBSET = theorem `;
3490   ∀s.  frontier (frontier s) ⊂ frontier s
3491   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF FrontierFrontierSubset`;;
3492
3493 let INTERIOR_FRONTIER = theorem `;
3494   ∀s.  interior (frontier s)  =  interior (closure s) ━ closure (interior s)
3495   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF frontier_DEF closure_DEF InteriorFrontier`;;
3496
3497 let INTERIOR_FRONTIER_EMPTY = theorem `;
3498   ∀s.  open s ∨ closed s  ⇒  interior (frontier s) = ∅
3499   by fol OPEN_IN CLOSED_IN interior_DEF frontier_DEF InteriorFrontierEmpty`;;
3500
3501 let UNION_FRONTIER = theorem `;
3502   ∀s t.  frontier s ∪ frontier t =
3503     frontier (s ∪ t) ∪ frontier (s ∩ t) ∪ frontier s ∩ frontier t
3504   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF UnionFrontier`;;
3505
3506 let CONNECTED_INTER_FRONTIER = theorem `;
3507   ∀s t.  connected s ∧ ¬(s ∩ t = ∅) ∧ ¬(s ━ t = ∅)
3508     ⇒  ¬(s ∩ frontier t = ∅)
3509   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN connected_DEF frontier_DEF ConnectedInterFrontier`;;
3510
3511 let INTERIOR_CLOSED_EQ_EMPTY_AS_FRONTIER = theorem `;
3512   ∀s. closed s ∧ interior s = ∅  ⇔  ∃t. open t ∧ s = frontier t
3513   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN interior_DEF OPEN_IN frontier_DEF InteriorClosedEqEmptyAsFrontier`;;
3514
3515 let FRONTIER_UNION = theorem `;
3516   ∀s t.  closure s ∩ closure t = ∅
3517     ⇒ frontier (s ∪ t) = frontier s ∪ frontier t
3518   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF closure_DEF FrontierUnion`;;
3519
3520 let CLOSURE_UNION_FRONTIER = theorem `;
3521   ∀s. closure s = s ∪ frontier s
3522   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF frontier_DEF ClosureUnionFrontier`;;
3523
3524 let FRONTIER_INTERIOR_SUBSET = theorem `;
3525   ∀s.  frontier (interior s) ⊂ frontier s
3526   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF interior_DEF FrontierInteriorSubset`;;
3527
3528 let FRONTIER_CLOSURE_SUBSET = theorem `;
3529   ∀s.  frontier (closure s) ⊂ frontier s
3530   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF closure_DEF FrontierClosureSubset`;;
3531
3532 let SET_DIFF_FRONTIER = theorem `;
3533   ∀s.  s ━ frontier s = interior s
3534   by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF interior_DEF SetDiffFrontier`;;
3535
3536 let FRONTIER_INTER_SUBSET_INTER = theorem `;
3537   ∀s t.  frontier (s ∩ t)  ⊂  closure s ∩ frontier t ∪ frontier s ∩ closure t
3538   by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF closure_DEF FrontierInterSubsetInter`;;