1 (* (c) Copyright, Bill Richter 2013 *)
2 (* Distributed under the same license as HOL Light *)
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 *)
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. *)
20 needs "RichterHilbertAxiomGeometry/readable.ml";;
21 needs "Multivariate/determinants.ml";;
23 ParseAsInfix("∉",(11, "right"));;
25 let NOTIN = NewDefinition `;
26 ∀a l. a ∉ l ⇔ ¬(a ∈ l)`;;
28 let DIFF_UNION = theorem `;
29 ∀u s t. u ━ (s ∪ t) = (u ━ s) ∩ (u ━ t)
32 let DIFF_INTER = theorem `;
33 ∀u s t. u ━ (s ∩ t) = (u ━ s) ∪ (u ━ t)
36 let DIFF_REFL = theorem `;
37 ∀u t. t ⊂ u ⇒ u ━ (u ━ t) = t
40 let DIFF_SUBSET = theorem `;
41 ∀u s t. s ⊂ t ⇒ s ━ u ⊂ t ━ u
44 let DOUBLE_DIFF_UNION = theorem `;
45 ∀A s t. A ━ s ━ t = A ━ (s ∪ t)
48 let SUBSET_COMPLEMENT = theorem `;
49 ∀s t A. s ⊂ A ⇒ (s ⊂ A ━ t ⇔ s ∩ t = ∅)
52 let COMPLEMENT_DISJOINT = theorem `;
53 ∀A s t. s ⊂ A ⇒ (s ⊂ t ⇔ s ∩ (A ━ t) = ∅)
56 let COMPLEMENT_DUALITY = theorem `;
57 ∀A s t. s ⊂ A ∧ t ⊂ A ⇒ (s = t ⇔ A ━ s = A ━ t)
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))
64 let SUBSET_DUALITY = theorem `;
65 ∀s t u. t ⊂ u ⇒ s ━ u ⊂ s ━ t
68 let COMPLEMENT_INTER_DIFF = theorem `;
69 ∀A s t. s ⊂ A ⇒ s ━ t = s ∩ (A ━ t)
72 let INTERS_SUBSET = theorem `;
73 ∀f t. ¬(f = ∅) ∧ (∀s. s ∈ f ⇒ s ⊂ t) ⇒ INTERS f ⊂ t
76 let IN_SET_FUNCTION_PREDICATE = theorem `;
77 ∀x f P. x ∈ {f y | P y} ⇔ ∃y. x = f y ∧ P y
80 let INTER_TENSOR = theorem `;
81 ∀s s' t t'. s ⊂ s' ∧ t ⊂ t' ⇒ s ∩ t ⊂ s' ∩ t'
84 let UNION_TENSOR = theorem `;
85 ∀s s' t t'. s ⊂ s' ∧ t ⊂ t' ⇒ s ∪ t ⊂ s' ∪ t'
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)
93 let istopology = NewDefinition `;
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`;;
98 let UnderlyingSpace = NewDefinition `;
99 UnderlyingSpace α = FST α`;;
101 let OpenSets = NewDefinition `;
102 OpenSets α = SND α`;;
104 let ExistsTopology = theorem `;
105 ∀X. ∃α. istopology α ∧ UnderlyingSpace α = X
109 consider L such that L = {U | U ⊂ X} [Lexists] by fol;
111 rewrite istopology IN_ELIM_THM Lexists UnderlyingSpace;
116 let topology_tybij_th = theorem `;
118 by fol ExistsTopology`;;
121 new_type_definition "topology" ("mk_topology","dest_topology")
124 let ISTOPOLOGYdest_topology = theorem `;
125 ∀α. istopology (dest_topology α)
126 by fol topology_tybij`;;
128 let OpenIn = NewDefinition `;
129 ∀α. open_in α = OpenSets (dest_topology α)`;;
131 let topspace = NewDefinition `;
132 ∀α. topspace α = UnderlyingSpace (dest_topology α)`;;
134 let TopologyPAIR = theorem `;
135 ∀α. dest_topology α = (topspace α, open_in α)
136 by rewrite PAIR_EQ OpenIn topspace UnderlyingSpace OpenSets`;;
138 let Topology_Eq = theorem `;
139 ∀α β. topspace α = topspace β ∧ (∀U. open_in α U ⇔ open_in β U)
144 eq_tac [Right] by fol;
146 dest_topology α = dest_topology β [] by simplify TopologyPAIR PAIR_EQ H1 H2 FUN_EQ_THM;
147 fol - topology_tybij;
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)
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;
165 let OPEN_IN_SUBSET = theorem `;
166 ∀α s. open_in α s ⇒ s ⊂ topspace α
167 by fol OpenInCLAUSES`;;
169 let OPEN_IN_EMPTY = theorem `;
171 by fol OpenInCLAUSES`;;
173 let OPEN_IN_INTER = theorem `;
174 ∀α s t. open_in α s ∧ open_in α t ⇒ open_in α (s ∩ t)
175 by fol OpenInCLAUSES`;;
177 let OPEN_IN_UNIONS = theorem `;
178 ∀α k. (∀s. s ∈ k ⇒ open_in α s) ⇒ open_in α (UNIONS k)
179 by fol OpenInCLAUSES`;;
181 let OpenInTopspace = theorem `;
182 ∀α. open_in α (topspace α)
183 by fol OpenInCLAUSES`;;
185 let OPEN_IN_UNION = theorem `;
186 ∀α s t. open_in α s ∧ open_in α t ⇒ open_in α (s ∪ t)
190 ∀x. x ∈ {s, t} ⇔ x = s ∨ x = t [] by fol IN_INSERT NOT_IN_EMPTY;
191 fol - UNIONS_2 H OPEN_IN_UNIONS;
195 let OPEN_IN_TOPSPACE = theorem `;
196 ∀α. open_in α (topspace α)
197 by fol OpenInCLAUSES`;;
199 let OPEN_IN_INTERS = theorem `;
200 ∀α s. FINITE s ∧ ¬(s = ∅) ∧ (∀t. t ∈ s ⇒ open_in α t)
201 ⇒ open_in α (INTERS s)
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;
214 let OPEN_IN_SUBOPEN = theorem `;
215 ∀α s. open_in α s ⇔ ∀x. x ∈ s ⇒ ∃t. open_in α t ∧ x ∈ t ∧ t ⊂ s
219 eq_tac [Left] by set;
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;
228 let closed_in = NewDefinition `;
229 ∀α s. closed_in α s ⇔
230 s ⊂ topspace α ∧ open_in α (topspace α ━ s)`;;
232 let CLOSED_IN_SUBSET = theorem `;
233 ∀α s. closed_in α s ⇒ s ⊂ topspace α
236 let CLOSED_IN_EMPTY = theorem `;
238 by fol closed_in EMPTY_SUBSET DIFF_EMPTY OPEN_IN_TOPSPACE`;;
240 let CLOSED_IN_TOPSPACE = theorem `;
241 ∀α. closed_in α (topspace α)
242 by fol closed_in SUBSET_REFL DIFF_EQ_EMPTY OPEN_IN_EMPTY`;;
244 let CLOSED_IN_UNION = theorem `;
245 ∀α s t. closed_in α s ∧ closed_in α t ⇒ closed_in α (s ∪ t)
248 intro_TAC ∀α s t, Hst;
249 fol Hst closed_in DIFF_UNION UNION_SUBSET OPEN_IN_INTER;
253 let CLOSED_IN_INTERS = theorem `;
254 ∀α k. ¬(k = ∅) ∧ (∀s. s ∈ k ⇒ closed_in α s) ⇒ closed_in α (INTERS k)
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;
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}
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;
275 {x | ∀a. P a ⇒ x ∈ {x | Q a x}} = {x | ∀a. P a ⇒ Q a x} [] by set;
276 simplify fDef INTERS_GSPEC -;
280 let CLOSED_IN_INTER = theorem `;
281 ∀α s t. closed_in α s ∧ closed_in α t ⇒ closed_in α (s ∩ t)
284 intro_TAC ∀α s t, Hs Ht;
285 rewrite GSYM INTERS_2;
286 MATCH_MP_TAC CLOSED_IN_INTERS;
291 let OPEN_IN_CLOSED_IN_EQ = theorem `;
292 ∀α s. open_in α s ⇔ s ⊂ topspace α ∧ closed_in α (topspace α ━ 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;
301 let OPEN_IN_CLOSED_IN = theorem `;
303 ⇒ (open_in α s ⇔ closed_in α (topspace α ━ s))
304 by fol OPEN_IN_CLOSED_IN_EQ`;;
306 let OPEN_IN_DIFF = theorem `;
307 ∀α s t. open_in α s ∧ closed_in α t ⇒ open_in α (s ━ t)
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;
316 let CLOSED_IN_DIFF = theorem `;
317 ∀α s t. closed_in α s ∧ open_in α t ⇒ closed_in α (s ━ t)
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;
326 let CLOSED_IN_UNIONS = theorem `;
327 ∀α s. FINITE s ∧ (∀t. t ∈ s ⇒ closed_in α t)
328 ⇒ closed_in α (UNIONS s)
333 MATCH_MP_TAC FINITE_INDUCT;
334 fol UNIONS_INSERT UNIONS_0 CLOSED_IN_EMPTY IN_INSERT CLOSED_IN_UNION;
338 let subtopology = NewDefinition `;
339 ∀α u. subtopology α u = mk_topology (u, {s ∩ u | open_in α s})`;;
341 let IstopologySubtopology = theorem `;
342 ∀α u:A->bool. u ⊂ topspace α ⇒ istopology (u, {s ∩ u | open_in α s})
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]
351 intro_TAC ∀s' s, H1 H2;
352 set MESON [H1; H2; OPEN_IN_INTER] [open_in α (s' ∩ s)];
354 ∀k. k ⊂ {s | open_in α s} ⇒ open_in α (UNIONS k) ∧
355 UNIONS (IMAGE (λs. s ∩ u) k) = (UNIONS k) ∩ u [unionsOpen]
358 open_in α (UNIONS k) [] by fol kProp SUBSET IN_ELIM_THM OPEN_IN_UNIONS;
359 simplify - UNIONS_IMAGE UNIONS_GSPEC INTER_UNIONS;
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;
367 let OpenInSubtopology = theorem `;
368 ∀α u s. u ⊂ topspace α ⇒
369 (open_in (subtopology α u) s ⇔ ∃t. open_in α t ∧ s = t ∩ u)
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;
378 let TopspaceSubtopology = theorem `;
379 ∀α u. u ⊂ topspace α ⇒ topspace (subtopology α u) = u
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;
389 let OpenInRefl = theorem `;
390 ∀α s. s ⊂ topspace α ⇒ open_in (subtopology α s) s
391 by fol TopspaceSubtopology OPEN_IN_TOPSPACE`;;
393 let ClosedInRefl = theorem `;
394 ∀α s. s ⊂ topspace α ⇒ closed_in (subtopology α s) s
395 by fol TopspaceSubtopology CLOSED_IN_TOPSPACE`;;
397 let ClosedInSubtopology = theorem `;
398 ∀α u C. u ⊂ topspace α ⇒
399 (closed_in (subtopology α u) C ⇔ ∃D. closed_in α D ∧ C = D ∩ u)
402 intro_TAC ∀α u C, H1;
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 []
413 STRIP_TAC; exists_TAC X ━ t;
414 ASM_SIMP_TAC H1 OPEN_IN_SUBSET DIFF_REFL SUBSET_DIFF;
416 STRIP_TAC; exists_TAC X ━ D;
417 ASM_SIMP_TAC SUBSET_DIFF;
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;
425 let OPEN_IN_SUBTOPOLOGY_EMPTY = theorem `;
426 ∀α s. open_in (subtopology α ∅) s ⇔ s = ∅
429 simplify EMPTY_SUBSET OpenInSubtopology INTER_EMPTY;
434 let CLOSED_IN_SUBTOPOLOGY_EMPTY = theorem `;
435 ∀α s. closed_in (subtopology α ∅) s ⇔ s = ∅
438 simplify EMPTY_SUBSET ClosedInSubtopology INTER_EMPTY;
443 let SUBTOPOLOGY_TOPSPACE = theorem `;
444 ∀α. subtopology α (topspace α) = α
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;
454 let OpenInImpSubset = theorem `;
455 ∀α s t. s ⊂ topspace α ⇒
456 open_in (subtopology α s) t ⇒ t ⊂ s
457 by fol OpenInSubtopology INTER_SUBSET`;;
459 let ClosedInImpSubset = theorem `;
460 ∀α s t. s ⊂ topspace α ⇒
461 closed_in (subtopology α s) t ⇒ t ⊂ s
462 by fol ClosedInSubtopology INTER_SUBSET`;;
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
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;
477 set MESON [abExist; OPEN_IN_INTER] [open_in α (a ∩ b)] abExist;
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
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;
494 set MESON [abExist; CLOSED_IN_INTER] [closed_in α (a ∩ b)] abExist;
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)
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;
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`;;
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`;;
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`;;
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`;;
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`;;
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)
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;
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`;;
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`;;
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
565 intro_TAC ∀α s t u, uSubset tSubset;
566 simplify uSubset tSubset OpenInSubtopology;
567 intro_TAC sOpen_u s_t t_u;
569 open_in α a ∧ s = a ∩ u [aExists] by fol uSubset sOpen_u OpenInSubtopology;
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
580 intro_TAC ∀α s t u, uSubset tSubset;
581 simplify uSubset tSubset ClosedInSubtopology;
582 intro_TAC sClosed_u s_t t_u;
584 closed_in α a ∧ s = a ∩ u [aExists] by fol uSubset sClosed_u ClosedInSubtopology;
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
595 intro_TAC ∀α s t u, H1 H2;
596 simplify H1 H2 OpenInSubtopology;
597 fol H1 H2 OpenInSubtopology OPEN_IN_INTER INTER_ASSOC;
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`;;
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`;;
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
618 simplify OpenInSubtopology;
619 fol OPEN_IN_INTER INTER_ASSOC;
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)
629 intro_TAC ∀α u s, H1;
630 rewriteL OPEN_IN_SUBOPEN;
631 simplify H1 OpenInSubtopology;
632 eq_tac [Right] by fol SUBSET IN_INTER;
635 proof simplify SUBSET; fol H2 IN_INTER; qed;
638 open_in α t ∧ x ∈ t ∩ u ∧ t ∩ u ⊂ s [tExists] by fol H2 xs;
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
649 simplify ClosedInSubtopology;
650 fol CLOSED_IN_INTER INTER_ASSOC;
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)
660 intro_TAC ∀α s t, H1 H2;
661 fol H1 H2 ClosedInSubtopologyTrans CLOSED_IN_TOPSPACE;
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`;;
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)
676 simplify OpenInSubtopology;
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`;;
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`;;
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`;;
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}
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;
710 let Connected_DEF = NewDefinition `;
712 ¬(∃e1 e2. open_in α e1 ∧ open_in α e2 ∧ topspace α = e1 ∪ e2 ∧
713 e1 ∩ e2 = ∅ ∧ ¬(e1 = ∅) ∧ ¬(e2 = ∅))`;;
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)
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;
726 let ConnectedClosed = theorem `;
728 ¬(∃e1 e2. closed_in α e1 ∧ closed_in α e2 ∧
729 topspace α = e1 ∪ e2 ∧ e1 ∩ e2 = ∅ ∧ ¬(e1 = ∅) ∧ ¬(e2 = ∅))
732 rewrite Connected_DEF;
733 fol ConnectedClosedHelp;
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 = ∅)))
744 simplify Connected_DEF TopspaceSubtopology;
745 fol SUBSET_REFL OpenInImpSubset UNION_SUBSET SUBSET_ANTISYM;
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 = ∅)))
756 simplify ConnectedClosed TopspaceSubtopology;
757 fol SUBSET_REFL ClosedInImpSubset UNION_SUBSET SUBSET_ANTISYM;
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 = ∅)))
769 simplify H1 Connected_DEF OpenInSubtopology TopspaceSubtopology;
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;
780 rewrite LEFT_IMP_EXISTS_THM;
781 intro_TAC ∀e1 e2, e12Exist;
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 = ∅)
795 proof simplify ConnectedSubtopology; fol; qed;
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 = ∅)))
806 simplify H1 ConnectedSubtopology;
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;
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;
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 = ∅)
834 proof simplify ConnectedClosedSubtopology; fol; qed;
837 let ConnectedClopen = theorem `;
839 ∀t. open_in α t ∧ closed_in α t ⇒ t = ∅ ∨ t = topspace α
843 simplify Connected_DEF closed_in TAUT [(¬a ⇔ b) ⇔ (a ⇔ ¬b)] NOT_FORALL_THM NOT_IMP DE_MORGAN_THM;
846 rewrite LEFT_IMP_EXISTS_THM; intro_TAC ∀e1 e2, H1 H2 H3 H4 H5 H6;
848 e1 ⊂ topspace α ∧ e2 = topspace α ━ e1 ∧ ¬(e1 = topspace alpha) [] by set H3 H4 H6;
851 rewrite LEFT_IMP_EXISTS_THM; intro_TAC ∀t, H1;
852 exists_TAC t; exists_TAC topspace α ━ t;
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 = ∅))
864 intro_TAC ∀α s, H1, H2;
865 simplify H1 ConnectedClosedSubtopology;
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;
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;
880 let ConnectedOpenSet = theorem `;
882 (Connected (subtopology α s) ⇔
883 ¬(∃e1 e2. open_in α e1 ∧ open_in α e2 ∧
884 ¬(e1 = ∅) ∧ ¬(e2 = ∅) ∧ e1 ∪ e2 = s ∧ e1 ∩ e2 = ∅))
888 simplify H1 OPEN_IN_SUBSET ConnectedSubtopology;
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;
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;
904 let ConnectedEmpty = theorem `;
905 ∀α. Connected (subtopology α ∅)
908 simplify Connected_DEF INTER_EMPTY EMPTY_SUBSET TopspaceSubtopology;
909 fol UNION_SUBSET SUBSET_EMPTY;
913 let ConnectedSing = theorem `;
914 ∀α a. a ∈ topspace α ⇒ Connected (subtopology α {a})
917 simplify Connected_DEF SING_SUBSET TopspaceSubtopology;
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))
929 simplify H1 ConnectedSubtopology UNIONS_SUBSET NOT_EXISTS_THM;
930 intro_TAC allConnected PnotDisjoint, ∀[d/e1] [e/e2];
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
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 -;
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))
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;
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))
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;
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;
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
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;
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 = ∅) []
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;
1019 fol - sf fTop fConn ConnectedSubtopology;
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'
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;
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)
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]
1062 MP_TAC ISPECL [α; s] ConnectedClosedSet;
1063 simplify stTop sClosed NOTsConn;
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;
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;
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)
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]
1098 MP_TAC ISPECL [α; s] ConnectedOpenSet;
1099 simplify stTop sOpen NOTsConn;
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;
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;
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
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) []
1129 simplify sTop ConnectedOpenIn;
1131 {b | ∃t. open_in (subtopology α s) t ∧ b ∈ t ∧ ∀x. x ∈ t ∧ P x ⇒ Q x};
1133 {b | ∃t. open_in (subtopology α s) t ∧ b ∈ t ∧ ∀x. x ∈ t ∧ P x ⇒ ¬(Q x)};
1136 ONCE_REWRITE_TAC OPEN_IN_SUBOPEN;
1138 rewrite IN_ELIM_THM;
1139 MATCH_MP_TAC MONO_EXISTS;
1140 set atOpenImplies_ztPz;
1144 ONCE_REWRITE_TAC OPEN_IN_SUBOPEN;
1146 rewrite IN_ELIM_THM;
1147 MATCH_MP_TAC MONO_EXISTS;
1148 set atOpenImplies_ztPz;
1152 rewrite SUBSET IN_ELIM_THM IN_UNION;
1153 X_genl_TAC c; intro_TAC cs;
1154 MP_TAC SPECL [c] asImplies_atOpen_xytPxPyQxasImpliesQy;
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;
1160 ONCE_REWRITE_TAC TAUT [∀p. ¬p ⇔ p ⇒ F];
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;
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) ∧
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
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 []
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;
1193 fol aINs Pa bINs Pb asImplies_atOpen_xytPxPyImpliesRxy -;
1197 let ConnectedInductionSimple = theorem `;
1198 ∀α P s. s ⊂ topspace α ⇒
1199 Connected (subtopology α 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
1206 intro_TAC ∀α P s, sTop;
1207 MP_TAC ISPECL [α; (λx. T ∨ x ∈ s); P; s] ConnectedInduction;
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) ∧
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
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 []
1223 intro_TAC ∀[p/a], pINs;
1224 MP_TAC ISPECL [α; λx. R p x; s] ConnectedInductionSimple;
1226 fol asImplies_atOpen_xtImpliesRax Rcomm Rtrans;
1228 fol asImplies_atOpen_xtImpliesRax -;
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}`;;
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`;;
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}) = ∅)
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;
1255 let LimptSubset = theorem `;
1256 ∀α s t. t ⊂ topspace α ⇒
1257 s ⊂ t ⇒ LimitPointOf α s ⊂ LimitPointOf α t
1260 intro_TAC ∀α s t, tTop, st;
1261 s ⊂ topspace α [sTop] by fol tTop st SUBSET_TRANS;
1262 simplify tTop sTop IN_LimitPointOf SUBSET;
1267 let ClosedLimpt = theorem `;
1268 ∀α s. s ⊂ topspace α ⇒
1269 (closed_in α s ⇔ LimitPointOf α s ⊂ s)
1273 simplify H1 closed_in;
1274 ONCE_REWRITE_TAC OPEN_IN_SUBOPEN;
1275 simplify H1 IN_LimitPointOf SUBSET IN_DIFF;
1278 fol OPEN_IN_SUBSET SUBSET;
1282 let LimptEmpty = theorem `;
1283 ∀α x. x ∈ topspace α ⇒ x ∉ LimitPointOf α ∅
1284 by fol EMPTY_SUBSET IN_LimitPointOf OPEN_IN_TOPSPACE NOT_IN_EMPTY ∉`;;
1286 let NoLimitPointImpClosed = theorem `;
1287 ∀α s. s ⊂ topspace α ⇒ (∀x. x ∉ LimitPointOf α s) ⇒ closed_in α s
1288 by fol ClosedLimpt SUBSET ∉`;;
1290 let LimitPointUnion = theorem `;
1291 ∀α s t. s ∪ t ⊂ topspace α ⇒
1292 LimitPointOf α (s ∪ t) = LimitPointOf α s ∪ LimitPointOf α t
1295 intro_TAC ∀α s t, H1;
1296 s ⊂ topspace α ∧ t ⊂ topspace α [stTop] by fol H1 UNION_SUBSET;
1297 rewrite EXTENSION IN_UNION;
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;
1309 let Interior_DEF = NewDefinition `;
1310 ∀α s. Interior α s =
1311 {x | s ⊂ topspace α ∧ ∃t. open_in α t ∧ x ∈ t ∧ t ⊂ s}`;;
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`;;
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`;;
1323 let InteriorEq = theorem `;
1324 ∀α s. s ⊂ topspace α ⇒
1325 (open_in α s ⇔ s = Interior α s)
1329 rewriteL OPEN_IN_SUBOPEN;
1330 simplify EXTENSION H1 IN_Interior;
1335 let InteriorOpen = theorem `;
1336 ∀α s. open_in α s ⇒ Interior α s = s
1337 by fol OPEN_IN_SUBSET InteriorEq`;;
1339 let InteriorEmpty = theorem `;
1340 ∀α. Interior α ∅ = ∅
1341 by fol OPEN_IN_EMPTY EMPTY_SUBSET InteriorOpen`;;
1343 let InteriorUniv = theorem `;
1344 ∀α. Interior α (topspace α) = topspace α
1345 by simplify OpenInTopspace InteriorOpen`;;
1347 let OpenInterior = theorem `;
1348 ∀α s. s ⊂ topspace α ⇒ open_in α (Interior α s)
1351 ONCE_REWRITE_TAC OPEN_IN_SUBOPEN;
1352 fol IN_Interior SUBSET;
1356 let InteriorInterior = theorem `;
1357 ∀α s. s ⊂ topspace α ⇒
1358 Interior α (Interior α s) = Interior α s
1359 by fol OpenInterior InteriorOpen`;;
1361 let InteriorSubset = theorem `;
1362 ∀α s. s ⊂ topspace α ⇒ Interior α s ⊂ s
1366 simplify SUBSET Interior_DEF IN_ELIM_THM;
1371 let InteriorTopspace = theorem `;
1372 ∀α s. s ⊂ topspace α ⇒ Interior α s ⊂ topspace α
1373 by fol SUBSET_TRANS InteriorSubset`;;
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`;;
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`;;
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`;;
1390 let InteriorUnique = theorem `;
1391 ∀α s t. s ⊂ topspace α ⇒
1392 t ⊂ s ∧ open_in α t ∧ (∀t'. t' ⊂ s ∧ open_in α t' ⇒ t' ⊂ t)
1394 by fol SUBSET_ANTISYM InteriorSubset OpenInterior InteriorMaximal`;;
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`;;
1401 let InteriorInter = theorem `;
1402 ∀α s t. s ⊂ topspace α ∧ t ⊂ topspace α ⇒
1403 Interior α (s ∩ t) = Interior α s ∩ Interior α t
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;
1414 let InteriorFiniteInters = theorem `;
1415 ∀α s. FINITE s ⇒ ¬(s = ∅) ⇒ (∀t. t ∈ s ⇒ t ⊂ topspace α) ⇒
1416 Interior α (INTERS s) = INTERS (IMAGE (Interior α) s)
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;
1428 let InteriorIntersSubset = theorem `;
1429 ∀α f. ¬(f = ∅) ∧ (∀t. t ∈ f ⇒ t ⊂ topspace α) ⇒
1430 Interior α (INTERS f) ⊂ INTERS (IMAGE (Interior α) f)
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;
1440 let UnionInteriorSubset = theorem `;
1441 ∀α s t. s ⊂ topspace α ∧ t ⊂ topspace α ⇒
1442 Interior α s ∪ Interior α t ⊂ Interior α (s ∪ t)
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;
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`;;
1456 let InteriorEqEmptyAlt = theorem `;
1457 ∀α s. s ⊂ topspace α ⇒
1458 (Interior α s = ∅ ⇔ ∀t. open_in α t ∧ ¬(t = ∅) ⇒ ¬(t ━ s = ∅))
1461 simplify InteriorEqEmpty;
1466 let InteriorUnionsOpenSubsets = theorem `;
1467 ∀α s. s ⊂ topspace α ⇒ UNIONS {t | open_in α t ∧ t ⊂ s} = Interior α s
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;
1478 let InteriorClosedUnionEmptyInterior = theorem `;
1479 ∀α s t. s ⊂ topspace α ∧ t ⊂ topspace α ⇒
1480 closed_in α s ∧ Interior α t = ∅ ⇒
1481 Interior α (s ∪ t) = Interior α s
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 []
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;
1497 fol SUBSET_ANTISYM H1 stTop OpenInterior - InteriorMaximal SUBSET_UNION SubsetInterior;
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 = ∅)
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;
1514 let Closure_DEF = NewDefinition `;
1515 ∀α s. Closure α s = s ∪ LimitPointOf α s`;;
1517 let Closure_THM = theorem `;
1518 ∀α s. s ⊂ topspace α ⇒ Closure α s = s ∪ LimitPointOf α s
1519 by fol Closure_DEF`;;
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)
1527 intro_TAC ∀α s x, H1;
1528 simplify H1 Closure_THM IN_UNION IN_LimitPointOf;
1533 let ClosureSubset = theorem `;
1534 ∀α s. s ⊂ topspace α ⇒ s ⊂ Closure α s
1535 by fol SUBSET IN_Closure`;;
1537 let ClosureTopspace = theorem `;
1538 ∀α s. s ⊂ topspace α ⇒ Closure α s ⊂ topspace α
1539 by fol SUBSET IN_Closure`;;
1541 let ClosureInterior = theorem `;
1542 ∀α s. s ⊂ topspace α ⇒
1543 Closure α s = topspace α ━ (Interior α (topspace α ━ s))
1547 simplify H1 EXTENSION IN_Closure IN_DIFF IN_Interior SUBSET;
1548 fol OPEN_IN_SUBSET SUBSET;
1552 let InteriorClosure = theorem `;
1553 ∀α s. s ⊂ topspace α ⇒
1554 Interior α s = topspace α ━ (Closure α (topspace α ━ s))
1555 by fol SUBSET_DIFF InteriorTopspace DIFF_REFL ClosureInterior`;;
1557 let ClosedClosure = theorem `;
1558 ∀α s. s ⊂ topspace α ⇒ closed_in α (Closure α s)
1559 by fol closed_in ClosureInterior DIFF_REFL SUBSET_DIFF InteriorTopspace OpenInterior`;;
1561 let SubsetClosure = theorem `;
1562 ∀α s t. t ⊂ topspace α ⇒ s ⊂ t ⇒ Closure α s ⊂ Closure α t
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;
1571 let ClosureHull = theorem `;
1572 ∀α s. s ⊂ topspace α ⇒ Closure α s = (closed_in α) hull s
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;
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`;;
1586 let ClosureClosed = theorem `;
1587 ∀α s. closed_in α s ⇒ Closure α s = s
1588 by fol closed_in ClosureEq`;;
1590 let ClosureClosure = theorem `;
1591 ∀α s. s ⊂ topspace α ⇒ Closure α (Closure α s) = Closure α s
1592 by fol ClosureTopspace ClosureHull HULL_HULL`;;
1594 let ClosureUnion = theorem `;
1595 ∀α s t. s ∪ t ⊂ topspace α
1596 ⇒ Closure α (s ∪ t) = Closure α s ∪ Closure α t
1599 intro_TAC ∀α s t, H1;
1600 s ⊂ topspace α ∧ t ⊂ topspace α [stTop] by fol H1 UNION_SUBSET;
1601 simplify H1 stTop Closure_THM LimitPointUnion;
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`;;
1611 let ClosureIntersSubset = theorem `;
1612 ∀α f. (∀s. s ∈ f ⇒ s ⊂ topspace α) ⇒
1613 Closure α (INTERS f) ⊂ INTERS (IMAGE (Closure α) f)
1617 rewrite SET_RULE [s ⊂ INTERS f ⇔ ∀t. t ∈ f ⇒ s ⊂ t] FORALL_IN_IMAGE;
1620 s ⊂ topspace α ∧ INTERS f ⊂ s ∧ INTERS f ⊂ topspace α [] by set H1 sf;
1621 fol SubsetClosure -;
1625 let ClosureMinimal = theorem `;
1626 ∀α s t. s ⊂ t ∧ closed_in α t ⇒ Closure α s ⊂ t
1627 by fol closed_in SubsetClosure ClosureClosed`;;
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`;;
1634 let ClosureUnique = theorem `;
1635 ∀α s t. s ⊂ t ∧ closed_in α t ∧ (∀u. s ⊂ u ∧ closed_in α u ⇒ t ⊂ u)
1637 by fol closed_in SUBSET_ANTISYM_EQ ClosureMinimal SUBSET_TRANS ClosureSubset ClosedClosure`;;
1639 let ClosureUniv = theorem `;
1640 ∀α. Closure α (topspace α) = topspace α
1641 by simplify SUBSET_REFL CLOSED_IN_TOPSPACE ClosureEq`;;
1643 let ClosureEmpty = theorem `;
1645 by fol EMPTY_SUBSET CLOSED_IN_EMPTY ClosureClosed`;;
1647 let ClosureUnions = theorem `;
1648 ∀α f. FINITE f ⇒ (∀ t. t ∈ f ⇒ t ⊂ topspace α) ⇒
1649 Closure α (UNIONS f) = UNIONS {Closure α t | t ∈ f}
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;
1660 let ClosureEqEmpty = theorem `;
1661 ∀α s. s ⊂ topspace α ⇒ (Closure α s = ∅ ⇔ s = ∅)
1662 by fol ClosureEmpty ClosureSubset SUBSET_EMPTY`;;
1664 let ClosureSubsetEq = theorem `;
1665 ∀α s. s ⊂ topspace α ⇒ (Closure α s ⊂ s ⇔ closed_in α s)
1666 by fol ClosureEq ClosureSubset SUBSET_ANTISYM`;;
1668 let OpenInterClosureEqEmpty = theorem `;
1669 ∀α s t. s ⊂ topspace α ∧ t ⊂ topspace α ⇒
1670 open_in α s ⇒ (s ∩ Closure α t = ∅ ⇔ s ∩ t = ∅)
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;
1681 let OpenInterClosureSubset = theorem `;
1682 ∀α s t. t ⊂ topspace α ⇒
1683 open_in α s ⇒ s ∩ Closure α t ⊂ Closure α (s ∩ t)
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) []
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;
1698 simplify - UNION_TENSOR SUBSET_REFL;
1702 let ClosureOpenInterSuperset = theorem `;
1703 ∀α s t. s ⊂ topspace α ∧ t ⊂ topspace α ⇒
1704 open_in α s ∧ s ⊂ Closure α t ⇒ Closure α (s ∩ t) = Closure α s
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;
1716 let ClosureComplement = theorem `;
1717 ∀α s. s ⊂ topspace α ⇒
1718 Closure α (topspace α ━ s) = topspace α ━ Interior α s
1719 by fol InteriorClosure SUBSET_DIFF ClosureTopspace DIFF_REFL`;;
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`;;
1726 let ClosureInteriorComplement = theorem `;
1727 ∀α s. s ⊂ topspace α ⇒
1728 topspace α ━ Closure α (Interior α s)
1729 = Interior α (Closure α (topspace α ━ s))
1730 by fol InteriorTopspace InteriorComplement ClosureComplement`;;
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`;;
1738 let ConnectedIntermediateClosure = theorem `;
1739 ∀α s t. s ⊂ topspace α ⇒
1740 Connected (subtopology α s) ∧ s ⊂ t ∧ t ⊂ Closure α s
1741 ⇒ Connected (subtopology α t)
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;
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;
1757 let ConnectedClosure = theorem `;
1758 ∀α s. s ⊂ topspace α ⇒ Connected (subtopology α s) ⇒
1759 Connected (subtopology α (Closure α s))
1760 by fol ClosureTopspace ClosureSubset SUBSET_REFL ConnectedIntermediateClosure`;;
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))
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;
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`;;
1784 let ClosedInLimpt = theorem `;
1785 ∀α s t. s ⊂ topspace α ∧ t ⊂ topspace α ⇒
1786 (closed_in (subtopology α t) s ⇔
1787 s ⊂ t ∧ LimitPointOf α s ∩ t ⊂ s)
1790 intro_TAC ∀α s t, H1 H2;
1791 simplify H2 ClosedInSubtopology;
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;
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;
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`;;
1811 let ClosedInInterClosure = theorem `;
1812 ∀α s t. s ⊂ topspace α ∧ t ⊂ topspace α ⇒
1813 (closed_in (subtopology α s) t ⇔ s ∩ Closure α t = t)
1815 proof simplify Closure_THM ClosedInLimpt; set; qed;
1818 let InteriorClosureIdemp = theorem `;
1819 ∀α s. s ⊂ topspace α ⇒
1820 Interior α (Closure α (Interior α (Closure α s)))
1821 = Interior α (Closure α s)
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;
1836 let InteriorClosureIdemp = theorem `;
1837 ∀α s. s ⊂ topspace α ⇒
1838 Interior α (Closure α (Interior α (Closure α s)))
1839 = Interior α (Closure α s)
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;
1852 let ClosureInteriorIdemp = theorem `;
1853 ∀α s. s ⊂ topspace α ⇒
1854 Closure α (Interior α (Closure α (Interior α s)))
1855 = Closure α (Interior α s)
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;
1866 let InteriorClosureDiffSpaceEmpty = theorem `;
1867 ∀α s. s ⊂ topspace α ⇒ Interior α (Closure α s ━ s) = ∅
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 ∉;
1883 let NowhereDenseUnion = theorem `;
1884 ∀α s t. s ∪ t ⊂ topspace α ⇒
1885 (Interior α (Closure α (s ∪ t)) = ∅ ⇔
1886 Interior α (Closure α s) = ∅ ∧ Interior α (Closure α t) = ∅)
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;
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 = ∅)
1903 simplify H1 ClosureTopspace InteriorEqEmptyAlt;
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 = ∅];
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;
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)
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) []
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;
1949 fol stTop ClosureTopspace - CsIntCtTop OpenInterior InteriorMaximal;
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)
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;
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`;;
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`;;
1978 let DiffClosureSubset = theorem `;
1979 ∀α s t. s ⊂ topspace α ∧ t ⊂ topspace α ⇒
1980 Closure α s ━ Closure α t ⊂ Closure α (s ━ t)
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;
1989 let Frontier_DEF = NewDefinition `;
1990 ∀α s. Frontier α s = Closure α s ━ Interior α s`;;
1992 let Frontier_THM = theorem `;
1993 ∀α s. s ⊂ topspace α ⇒ Frontier α s = Closure α s ━ Interior α s
1994 by fol Frontier_DEF`;;
1996 let FrontierTopspace = theorem `;
1997 ∀α s. s ⊂ topspace α ⇒ Frontier α s ⊂ topspace α
1998 by fol Frontier_THM SUBSET_DIFF ClosureTopspace SUBSET_TRANS`;;
2000 let FrontierClosed = theorem `;
2001 ∀α s. s ⊂ topspace α ⇒ closed_in α (Frontier α s)
2002 by simplify Frontier_THM ClosedClosure OpenInterior CLOSED_IN_DIFF`;;
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`;;
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))
2015 simplify SUBSET_DIFF FrontierClosures IN_INTER SUBSET_DIFF IN_Closure IN_DIFF;
2016 fol OPEN_IN_SUBSET SUBSET;
2020 let FrontierSubsetClosed = theorem `;
2021 ∀α s. closed_in α s ⇒ (Frontier α s) ⊂ s
2022 by fol closed_in Frontier_THM ClosureClosed SUBSET_DIFF`;;
2024 let FrontierEmpty = theorem `;
2025 ∀α. Frontier α ∅ = ∅
2026 by fol Frontier_THM EMPTY_SUBSET ClosureEmpty EMPTY_DIFF`;;
2028 let FrontierUniv = theorem `;
2029 ∀α. Frontier α (topspace α) = ∅
2030 by fol Frontier_DEF ClosureUniv InteriorUniv DIFF_EQ_EMPTY`;;
2032 let FrontierSubsetEq = theorem `;
2033 ∀α s. s ⊂ topspace α ⇒ ((Frontier α s) ⊂ s ⇔ closed_in α s)
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;
2043 let FrontierComplement = theorem `;
2044 ∀α s. s ⊂ topspace α ⇒ Frontier α (topspace α ━ s) = Frontier α s
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];
2054 let FrontierComplement = theorem `;
2055 ∀α s. s ⊂ topspace α ⇒ Frontier α (topspace α ━ s) = Frontier α s
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];
2065 let FrontierDisjointEq = theorem `;
2066 ∀α s. s ⊂ topspace α ⇒ ((Frontier α s) ∩ s = ∅ ⇔ open_in α s)
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;
2076 let FrontierInterSubset = theorem `;
2077 ∀α s t. s ∪ t ⊂ topspace α ⇒ Frontier α (s ∩ t) ⊂ Frontier α s ∪ Frontier α t
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;
2086 let FrontierUnionSubset = theorem `;
2087 ∀α s t. s ∪ t ⊂ topspace α ⇒
2088 Frontier α (s ∪ t) ⊂ Frontier α s ∪ Frontier α t
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;
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`;;
2104 let FrontierFrontierSubset = theorem `;
2105 ∀α s. s ⊂ topspace α ⇒ Frontier α (Frontier α s) ⊂ Frontier α s
2106 by fol FrontierTopspace Frontier_THM FrontierClosed ClosureClosed SUBSET_DIFF`;;
2108 let InteriorFrontier = theorem `;
2109 ∀α s. s ⊂ topspace α ⇒ Interior α (Frontier α s) =
2110 Interior α (Closure α s) ━ Closure α (Interior α s)
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;
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`;;
2127 let FrontierFrontier = theorem `;
2128 ∀α s. open_in α s ∨ closed_in α s ⇒
2129 Frontier α (Frontier α s) = Frontier α s
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;
2139 let UnionFrontierPart1 = theorem `;
2140 ∀α s t. s ∪ t ⊂ topspace α ⇒
2141 Frontier α s ∩ Interior α t ⊂ Frontier α (s ∩ t)
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;
2160 let UnionFrontierPart2 = theorem `;
2161 ∀α s t. s ∪ t ⊂ topspace α ⇒
2162 Frontier α s ━ Frontier α t ⊂
2163 Frontier α (s ∩ t) ∪ Frontier α (s ∪ t)
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;
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)
2183 intro_TAC ∀α s t a, H1;
2184 rewrite ∉ GSYM IN_INTER GSYM IN_DIFF GSYM IN_UNION;
2185 fol H1 UnionFrontierPart2 SUBSET;
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
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 ∉;
2204 let ConnectedInterFrontier = theorem `;
2205 ∀α s t. s ∪ t ⊂ topspace α ⇒
2206 Connected (subtopology α s) ∧ ¬(s ∩ t = ∅) ∧ ¬(s ━ t = ∅)
2207 ⇒ ¬(s ∩ Frontier α t = ∅)
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 -;
2224 let InteriorClosedEqEmptyAsFrontier = theorem `;
2225 ∀α s. s ⊂ topspace α ⇒
2226 (closed_in α s ∧ Interior α s = ∅ ⇔ ∃t. open_in α t ∧ s = Frontier α t)
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;
2237 let ClosureUnionFrontier = theorem `;
2238 ∀α s. s ⊂ topspace α ⇒ Closure α s = s ∪ Frontier α s
2241 intro_TAC ∀α s, sTop;
2242 simplify sTop Frontier_THM;
2243 s ⊂ Closure α s ∧ Interior α s ⊂ s [] by fol sTop ClosureSubset InteriorSubset;
2248 let FrontierInteriorSubset = theorem `;
2249 ∀α s. s ⊂ topspace α ⇒ Frontier α (Interior α s) ⊂ Frontier α s
2250 by simplify InteriorTopspace Frontier_THM InteriorInterior InteriorSubset SubsetClosure DIFF_SUBSET`;;
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`;;
2256 let SetDiffFrontier = theorem `;
2257 ∀α s. s ⊂ topspace α ⇒ s ━ Frontier α s = Interior α s
2260 intro_TAC ∀α s, sTop;
2261 simplify sTop Frontier_THM;
2262 s ⊂ Closure α s ∧ Interior α s ⊂ s [] by fol sTop ClosureSubset InteriorSubset;
2267 let FrontierInterSubsetInter = theorem `;
2268 ∀α s t. s ∪ t ⊂ topspace α ⇒
2269 Frontier α (s ∩ t) ⊂
2270 Closure α s ∩ Frontier α t ∪ Frontier α s ∩ Closure α t
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;
2281 let FrontierUnionPart1 = theorem `;
2282 ∀α s t. s ∪ t ⊂ topspace α ⇒ Closure α s ∩ Closure α t = ∅
2283 ⇒ Frontier α s ∩ Interior α (s ∪ t) = ∅
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) = ∅ []
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;
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 -;
2301 let FrontierUnion = theorem `;
2302 ∀α s t. s ∪ t ⊂ topspace α ⇒ Closure α s ∩ Closure α t = ∅
2303 ⇒ Frontier α (s ∪ t) = Frontier α s ∪ Frontier α t
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;
2317 (* ------------------------------------------------------------------------- *)
2318 (* The universal Euclidean versions are what we use most of the time. *)
2319 (* ------------------------------------------------------------------------- *)
2321 let open_def = NewDefinition `;
2322 open s ⇔ ∀x. x ∈ s ⇒ ∃e. &0 < e ∧ ∀x'. dist(x',x) < e ⇒ x' ∈ s`;;
2324 let closed = NewDefinition `;
2325 closed s ⇔ open (UNIV ━ s)`;;
2327 let euclidean = new_definition
2328 `euclidean = mk_topology (UNIV, open)`;;
2330 let OPEN_EMPTY = theorem `;
2332 by rewrite open_def NOT_IN_EMPTY`;;
2334 let OPEN_UNIV = theorem `;
2336 by fol open_def IN_UNIV REAL_LT_01`;;
2338 let OPEN_INTER = theorem `;
2339 ∀s t. open s ∧ open t ⇒ open (s ∩ t)
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;
2354 let OPEN_UNIONS = theorem `;
2355 (∀s. s ∈ f ⇒ open s) ⇒ open (UNIONS f)
2356 by fol open_def IN_UNIONS`;;
2358 let IstopologyEuclidean = theorem `;
2359 istopology (UNIV, open)
2360 by simplify istopology IN IN_UNIV SUBSET OPEN_EMPTY OPEN_UNIV OPEN_INTER OPEN_UNIONS`;;
2362 let OPEN_IN = theorem `;
2363 open = open_in euclidean
2364 by fol euclidean topology_tybij IstopologyEuclidean TopologyPAIR PAIR_EQ`;;
2366 let TOPSPACE_EUCLIDEAN = theorem `;
2367 topspace euclidean = UNIV
2368 by fol euclidean IstopologyEuclidean topology_tybij TopologyPAIR PAIR_EQ`;;
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`;;
2374 let OPEN_EXISTS = theorem `;
2375 ∀Q. (∀a. open {x | Q a x}) ⇒ open {x | ∃a. Q a x}
2379 (∀a. T ⇒ open {x | Q a x}) ⇒ open {x | ∃a. T ∧ Q a x} [] by simplify OPEN_EXISTS_IN;
2385 let TOPSPACE_EUCLIDEAN_SUBTOPOLOGY = theorem `;
2386 ∀s. topspace (subtopology euclidean s) = s
2387 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN TopspaceSubtopology`;;
2389 let OPEN_IN_REFL = theorem `;
2390 ∀s. open_in (subtopology euclidean s) s
2391 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN OpenInRefl`;;
2393 let CLOSED_IN_REFL = theorem `;
2394 ∀s. closed_in (subtopology euclidean s) s
2395 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosedInRefl`;;
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`;;
2401 let OPEN_UNION = theorem `;
2402 ∀s t. open s ∧ open t ⇒ open(s ∪ t)
2403 by fol OPEN_IN OPEN_IN_UNION`;;
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`;;
2409 let CLOSED_EMPTY = theorem `;
2411 by fol CLOSED_IN CLOSED_IN_EMPTY`;;
2413 let CLOSED_UNIV = theorem `;
2415 by fol CLOSED_IN TOPSPACE_EUCLIDEAN CLOSED_IN_TOPSPACE`;;
2417 let CLOSED_UNION = theorem `;
2418 ∀s t. closed s ∧ closed t ⇒ closed(s ∪ t)
2419 by fol CLOSED_IN CLOSED_IN_UNION`;;
2421 let CLOSED_INTER = theorem `;
2422 ∀s t. closed s ∧ closed t ⇒ closed(s ∩ t)
2423 by fol CLOSED_IN CLOSED_IN_INTER`;;
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`;;
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}
2435 case_split Pnonempty | Pempty by fol;
2437 simplify CLOSED_IN Pnonempty CLOSED_IN_FORALL_IN;
2440 {x | ∀a. P a ⇒ Q a x} = UNIV [] by set Pempty;
2441 simplify - CLOSED_UNIV;
2446 let CLOSED_FORALL = theorem `;
2447 ∀Q. (∀a. closed {x | Q a x}) ⇒ closed {x | ∀a. Q a x}
2451 (∀a. T ⇒ closed {x | Q a x}) ⇒ closed {x | ∀a. T ⇒ Q a x} [] by simplify CLOSED_FORALL_IN;
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`;;
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`;;
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`;;
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`;;
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`;;
2477 (* ------------------------------------------------------------------------- *)
2478 (* Open and closed balls and spheres. *)
2479 (* ------------------------------------------------------------------------- *)
2481 let ball = new_definition
2482 `ball(x,e) = {y | dist(x,y) < e}`;;
2484 let cball = new_definition
2485 `cball(x,e) = {y | dist(x,y) <= e}`;;
2487 let IN_BALL = theorem `;
2488 ∀x y e. y ∈ ball(x,e) ⇔ dist(x,y) < e
2489 by rewrite ball IN_ELIM_THM`;;
2491 let IN_CBALL = theorem `;
2492 ∀x y e. y ∈ cball(x, e) ⇔ dist(x, y) <= e
2493 by rewrite cball IN_ELIM_THM`;;
2495 let BALL_SUBSET_CBALL = theorem `;
2496 ∀x e. ball (x,e) ⊂ cball (x, e)
2499 rewrite IN_BALL IN_CBALL SUBSET;
2504 let OPEN_BALL = theorem `;
2505 ∀x e. open (ball (x,e))
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;
2513 let CENTRE_IN_BALL = theorem `;
2514 ∀x e. x ∈ ball(x,e) ⇔ &0 < e
2515 by fol IN_BALL DIST_REFL`;;
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`;;
2521 let HALF_CBALL_IN_BALL = theorem `;
2522 ∀e. &0 < e ⇒ &0 < e/ &2 ∧ e / &2 < e ∧ cball (x, e/ &2) ⊂ ball (x, e)
2526 &0 < e/ &2 ∧ e / &2 < e [] by real_arithmetic H1;
2527 fol - SUBSET IN_CBALL IN_BALL REAL_LET_TRANS;
2531 let OPEN_IN_CONTAINS_CBALL_LEMMA = theorem `;
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`;;
2537 (* ------------------------------------------------------------------------- *)
2538 (* Basic "localization" results are handy for connectedness. *)
2539 (* ------------------------------------------------------------------------- *)
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`;;
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`;;
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`;;
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`;;
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`;;
2563 let CLOSED_IN_CLOSED = theorem `;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
2595 let OPEN_IN_CONTAINS_BALL_LEMMA = theorem `;
2597 ((∃E. open E ∧ x ∈ E ∧ E ∩ t ⊂ s) ⇔
2598 (∃e. &0 < e ∧ ball (x,e) ∩ t ⊂ s))
2601 intro_TAC ∀ t s x, xs;
2602 eq_tac [Right] by fol CENTRE_IN_BALL OPEN_BALL;
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;
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`;;
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`;;
2622 let open_in = theorem `;
2623 ∀u s. open_in (subtopology euclidean u) s ⇔
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`;;
2629 (* ------------------------------------------------------------------------- *)
2630 (* These "transitivity" results are handy too. *)
2631 (* ------------------------------------------------------------------------- *)
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
2640 t ⊂ topspace euclidean ∧ u ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2641 fol - OPEN_IN OpenInTrans;
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`;;
2651 let OPEN_IN_OPEN_TRANS = theorem `;
2652 ∀u s. open_in (subtopology euclidean u) s ∧ open u ⇒ open s
2656 u ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2657 fol - H1 OPEN_IN OpenInOpenTrans;
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
2668 t ⊂ topspace euclidean ∧ u ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2669 fol - ClosedInSubtopologyTrans;
2673 let CLOSED_IN_TRANS_EQ = theorem `;
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`;;
2679 let CLOSED_IN_CLOSED_TRANS = theorem `;
2680 ∀s u. closed_in (subtopology euclidean u) s ∧ closed u ⇒ closed s
2684 u ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2685 fol - CLOSED_IN ClosedInClosedTrans;
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`;;
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`;;
2698 let CLOSED_IN_CLOSED_EQ = theorem `;
2700 (closed_in (subtopology euclidean s) t ⇔ closed t ∧ t ⊂ s)
2701 by fol CLOSED_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosedInClosedEq`;;
2703 (* ------------------------------------------------------------------------- *)
2704 (* Also some invariance theorems for relative topology. *)
2705 (* ------------------------------------------------------------------------- *)
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)
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;
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;
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;
2729 simplify REAL_LT_DIV eExists B1exists;
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;
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;
2738 simplify REAL_LT_MUL eExists B2exists;
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;
2745 add_linear_invariants [OPEN_IN_INJECTIVE_LINEAR_IMAGE];;
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)
2753 rewrite closed_in TOPSPACE_EUCLIDEAN_SUBTOPOLOGY;
2754 GEOM_TRANSFORM_TAC[];
2758 add_linear_invariants [CLOSED_IN_INJECTIVE_LINEAR_IMAGE];;
2760 (* ------------------------------------------------------------------------- *)
2761 (* Subspace topology results only proved for Euclidean space. *)
2762 (* ------------------------------------------------------------------------- *)
2764 (* ISTOPLOGY_SUBTOPOLOGY can not be proved, as the definition of topology *)
2765 (* there is different from the one here. *)
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`;;
2772 let TOPSPACE_SUBTOPOLOGY = theorem `;
2773 ∀u. topspace(subtopology euclidean u) = topspace euclidean ∩ u
2777 u ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2778 fol - TopspaceSubtopology INTER_COMM SUBSET_INTER_ABSORPTION;
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`;;
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`;;
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`;;
2795 let SUBTOPOLOGY_UNIV = theorem `;
2796 subtopology euclidean UNIV = euclidean
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;
2806 let SUBTOPOLOGY_SUPERSET = theorem `;
2807 ∀s. topspace euclidean ⊂ s ⇒ subtopology euclidean s = euclidean
2808 by simplify TOPSPACE_EUCLIDEAN UNIV_SUBSET SUBTOPOLOGY_UNIV`;;
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`;;
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`;;
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`;;
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`;;
2830 (* ------------------------------------------------------------------------- *)
2831 (* Connectedness. *)
2832 (* ------------------------------------------------------------------------- *)
2834 let connected_DEF = NewDefinition `;
2835 connected s ⇔ Connected (subtopology euclidean s)`;;
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`;;
2843 let CONNECTED_CLOSED = theorem `;
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`;;
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`;;
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`;;
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`;;
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`;;
2878 let CONNECTED_CLOPEN = theorem `;
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`;;
2884 let CONNECTED_CLOSED_SET = theorem `;
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`;;
2891 let CONNECTED_OPEN_SET = theorem `;
2894 ¬(∃e1 e2. open e1 ∧ open e2 ∧
2895 ¬(e1 = ∅) ∧ ¬(e2 = ∅) ∧ e1 ∪ e2 = s ∧ e1 ∩ e2 = ∅))
2896 by simplify connected_DEF OPEN_IN ConnectedOpenSet`;;
2898 let CONNECTED_EMPTY = theorem `;
2900 by rewrite connected_DEF ConnectedEmpty`;;
2902 let CONNECTED_SING = theorem `;
2907 a ∈ topspace euclidean [] by fol IN_UNIV TOPSPACE_EUCLIDEAN;
2908 fol - ConnectedSing connected_DEF;
2912 let CONNECTED_UNIONS = theorem `;
2913 ∀P. (∀s. s ∈ P ⇒ connected s) ∧ ¬(INTERS P = ∅)
2914 ⇒ connected(UNIONS P)
2918 ∀s. s ∈ P ⇒ s ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2919 fol - connected_DEF ConnectedUnions;
2923 let CONNECTED_UNION = theorem `;
2924 ∀s t. connected s ∧ connected t ∧ ¬(s ∩ t = ∅)
2929 s ⊂ topspace euclidean ∧ t ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2930 fol - connected_DEF ConnectedUnion;
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)
2938 by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN connected_DEF OPEN_IN CLOSED_IN ConnectedDiffOpenFromClosed`;;
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'
2946 by rewrite connected_DEF OPEN_IN ConnectedDisjointUnionsOpenUnique`;;
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
2954 s ∪ t ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2955 fol - connected_DEF CLOSED_IN ConnectedFromClosedUnionAndInter;
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
2965 s ∪ t ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2966 fol - connected_DEF OPEN_IN ConnectedFromOpenUnionAndInter;
2970 (* ------------------------------------------------------------------------- *)
2971 (* Sort of induction principle for connected sets. *)
2972 (* ------------------------------------------------------------------------- *)
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
2983 s ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
2985 rewrite connected_DEF ConnectedInduction;
2989 let CONNECTED_EQUIVALENCE_RELATION_GEN_LEMMA = theorem `;
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) ∧
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
3002 s ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
3004 rewrite connected_DEF ConnectedEquivalenceRelationGen;
3008 let CONNECTED_EQUIVALENCE_RELATION_GEN = theorem `;
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) ∧
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
3022 MP_TAC ISPECL [P; R; s] CONNECTED_EQUIVALENCE_RELATION_GEN_LEMMA;
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
3035 s ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
3037 rewrite connected_DEF ConnectedInductionSimple;
3041 let CONNECTED_EQUIVALENCE_RELATION = theorem `;
3043 (∀x y. R x y ⇒ R y x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
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
3050 s ⊂ topspace euclidean [] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN;
3052 rewrite connected_DEF ConnectedEquivalenceRelation;
3056 (* ------------------------------------------------------------------------- *)
3058 (* ------------------------------------------------------------------------- *)
3060 parse_as_infix ("limit_point_of",(12,"right"));;
3062 let limit_point_of_DEF = NewDefinition `;
3063 x limit_point_of s ⇔ x ∈ LimitPointOf euclidean s`;;
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`;;
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`;;
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`;;
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`;;
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 ∉`;;
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`;;
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`;;
3095 (* ------------------------------------------------------------------------- *)
3096 (* Interior of a set. *)
3097 (* ------------------------------------------------------------------------- *)
3099 let interior_DEF = NewDefinition `;
3100 interior = Interior euclidean`;;
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`;;
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`;;
3110 let INTERIOR_OPEN = theorem `;
3111 ∀s. open s ⇒ interior s = s
3112 by fol interior_DEF OPEN_IN InteriorOpen`;;
3114 let INTERIOR_EMPTY = theorem `;
3116 by fol interior_DEF OPEN_IN InteriorEmpty`;;
3118 let INTERIOR_UNIV = theorem `;
3119 interior UNIV = UNIV
3120 by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF InteriorUniv`;;
3122 let OPEN_INTERIOR = theorem `;
3123 ∀s. open (interior s)
3124 by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN OpenInterior`;;
3126 let INTERIOR_INTERIOR = theorem `;
3127 ∀s. interior (interior s) = interior s
3128 by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorInterior`;;
3130 let INTERIOR_SUBSET = theorem `;
3132 by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorSubset`;;
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`;;
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`;;
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`;;
3146 let INTERIOR_UNIQUE = theorem `;
3147 ∀s t. t ⊂ s ∧ open t ∧ (∀t'. t' ⊂ s ∧ open t' ⇒ t' ⊂ t)
3149 by simplify interior_DEF OPEN_IN SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorUnique`;;
3151 let IN_INTERIOR = theorem `;
3152 ∀x s. x ∈ interior s ⇔ ∃e. &0 < e ∧ ball(x,e) ⊂ s
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;
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`;;
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`;;
3168 let INTERIOR_FINITE_INTERS = theorem `;
3169 ∀s. FINITE s ⇒ interior (INTERS s) = INTERS (IMAGE interior s)
3173 assume ¬(s = ∅) [sNonempty] by simplify INTERS_0 IMAGE_CLAUSES INTERIOR_UNIV;
3174 simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN H1 sNonempty interior_DEF InteriorFiniteInters;
3178 let INTERIOR_FINITE_INTERS = theorem `;
3179 ∀s. FINITE s ⇒ interior (INTERS s) = INTERS (IMAGE interior s)
3183 assume s = ∅ [sEmpty] by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN H1 interior_DEF InteriorFiniteInters;
3184 rewrite INTERS_0 IMAGE_CLAUSES sEmpty INTERIOR_UNIV;
3188 let INTERIOR_INTERS_SUBSET = theorem `;
3189 ∀f. interior (INTERS f) ⊂ INTERS (IMAGE interior f)
3193 assume f = ∅ [fEmpty] by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN interior_DEF InteriorIntersSubset;
3194 rewrite INTERS_0 IMAGE_CLAUSES - INTERIOR_UNIV SUBSET_REFL;
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`;;
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`;;
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`;;
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`;;
3214 (* ------------------------------------------------------------------------- *)
3215 (* Closure of a set. *)
3216 (* ------------------------------------------------------------------------- *)
3218 let closure_DEF = NewDefinition `;
3219 closure = Closure euclidean`;;
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`;;
3225 let CLOSURE_INTERIOR = theorem `;
3226 ∀s. closure s = UNIV ━ interior (UNIV ━ s)
3229 rewrite closure_DEF GSYM TOPSPACE_EUCLIDEAN interior_DEF;
3230 simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosureInterior;
3234 let INTERIOR_CLOSURE = theorem `;
3235 ∀s. interior s = UNIV ━ (closure (UNIV ━ s))
3238 rewrite closure_DEF GSYM TOPSPACE_EUCLIDEAN interior_DEF;
3239 simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorClosure;
3243 let CLOSED_CLOSURE = theorem `;
3244 ∀s. closed (closure s)
3245 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosedClosure`;;
3247 let CLOSURE_SUBSET = theorem `;
3249 by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureSubset`;;
3251 let SUBSET_CLOSURE = theorem `;
3252 ∀s t. s ⊂ t ⇒ closure s ⊂ closure t
3253 by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF SubsetClosure`;;
3255 let CLOSURE_HULL = theorem `;
3256 ∀s. closure s = closed hull s
3257 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureHull`;;
3259 let CLOSURE_EQ = theorem `;
3260 ∀s. closure s = s ⇔ closed s
3261 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureEq`;;
3263 let CLOSURE_CLOSED = theorem `;
3264 ∀s. closed s ⇒ closure s = s
3265 by fol CLOSED_IN closure_DEF ClosureClosed`;;
3267 let CLOSURE_CLOSURE = theorem `;
3268 ∀s. closure (closure s) = closure s
3269 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN CLOSED_IN closure_DEF ClosureClosure`;;
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`;;
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`;;
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`;;
3283 let CLOSURE_MINIMAL = theorem `;
3284 ∀s t. s ⊂ t ∧ closed t ⇒ closure s ⊂ t
3285 by fol CLOSED_IN closure_DEF ClosureMinimal`;;
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`;;
3291 let CLOSURE_UNIQUE = theorem `;
3292 ∀s t. s ⊂ t ∧ closed t ∧ (∀t'. s ⊂ t' ∧ closed t' ⇒ t ⊂ t')
3294 by fol CLOSED_IN closure_DEF ClosureUnique`;;
3297 let CLOSURE_EMPTY = theorem `;
3299 by fol closure_DEF ClosureEmpty`;;
3301 let CLOSURE_UNIV = theorem `;
3303 by fol TOPSPACE_EUCLIDEAN closure_DEF ClosureUniv`;;
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`;;
3309 let CLOSURE_EQ_EMPTY = theorem `;
3310 ∀s. closure s = ∅ ⇔ s = ∅
3311 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF ClosureEqEmpty`;;
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`;;
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`;;
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`;;
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`;;
3329 let CLOSURE_COMPLEMENT = theorem `;
3330 ∀s. closure (UNIV ━ s) = UNIV ━ interior s
3333 rewrite closure_DEF GSYM TOPSPACE_EUCLIDEAN interior_DEF;
3334 simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN ClosureComplement;
3338 let INTERIOR_COMPLEMENT = theorem `;
3339 ∀s. interior (UNIV ━ s) = UNIV ━ closure s
3342 rewrite closure_DEF GSYM TOPSPACE_EUCLIDEAN interior_DEF;
3343 simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN InteriorComplement;
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`;;
3351 let CONNECTED_CLOSURE = theorem `;
3352 ∀s. connected s ⇒ connected (closure s)
3353 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF connected_DEF ConnectedClosure`;;
3355 let CONNECTED_UNION_STRONG = theorem `;
3356 ∀s t. connected s ∧ connected t ∧ ¬(closure s ∩ t = ∅)
3358 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN closure_DEF connected_DEF ConnectedUnionStrong`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
3424 (* ------------------------------------------------------------------------- *)
3425 (* Frontier (aka boundary). *)
3426 (* ------------------------------------------------------------------------- *)
3428 let frontier_DEF = NewDefinition `;
3429 frontier = Frontier euclidean`;;
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`;;
3435 let FRONTIER_CLOSED = theorem `;
3436 ∀s. closed (frontier s)
3437 by simplify SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF CLOSED_IN FrontierClosed`;;
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`;;
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)
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;
3453 let FRONTIER_SUBSET_CLOSED = theorem `;
3454 ∀s. closed s ⇒ (frontier s) ⊂ s
3455 by fol frontier_DEF CLOSED_IN FrontierSubsetClosed`;;
3457 let FRONTIER_EMPTY = theorem `;
3459 by fol frontier_DEF FrontierEmpty`;;
3461 let FRONTIER_UNIV = theorem `;
3463 by fol frontier_DEF TOPSPACE_EUCLIDEAN FrontierUniv`;;
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`;;
3469 let FRONTIER_COMPLEMENT = theorem `;
3470 ∀s. frontier (UNIV ━ s) = frontier s
3471 by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF FrontierComplement`;;
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`;;
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`;;
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`;;
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`;;
3489 let FRONTIER_FRONTIER_SUBSET = theorem `;
3490 ∀s. frontier (frontier s) ⊂ frontier s
3491 by fol SUBSET_UNIV TOPSPACE_EUCLIDEAN frontier_DEF FrontierFrontierSubset`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;
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`;;