Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Topological Spaces and Continuous Functions

**by****Beata Padlewska, and****Agata Darmochwal**- Received April 14, 1989
- MML identifier: PRE_TOPC

- [ Mizar article, MML identifier index ]

environ vocabulary SETFAM_1, TARSKI, BOOLE, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL2, PRE_TOPC; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_2, SETFAM_1, STRUCT_0; constructors STRUCT_0, FUNCT_2, MEMBERED; clusters STRUCT_0, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1; requirements BOOLE, SUBSET; begin definition struct(1-sorted) TopStruct (# carrier -> set, topology -> Subset-Family of the carrier #); end; reserve T for TopStruct; :: :: The topological space :: definition let IT be TopStruct; attr IT is TopSpace-like means :: PRE_TOPC:def 1 the carrier of IT in the topology of IT & (for a being Subset-Family of IT st a c= the topology of IT holds union a in the topology of IT) & (for a,b being Subset of IT st a in the topology of IT & b in the topology of IT holds a /\ b in the topology of IT); end; definition cluster non empty strict TopSpace-like TopStruct; end; definition mode TopSpace is TopSpace-like TopStruct; end; definition let S be 1-sorted; mode Point of S is Element of S; end; reserve GX for TopSpace; canceled 4; theorem :: PRE_TOPC:5 {} in the topology of GX; definition let T be 1-sorted; func {}T -> Subset of T equals :: PRE_TOPC:def 2 {}; func [#]T -> Subset of T equals :: PRE_TOPC:def 3 the carrier of T; end; definition let T be 1-sorted; cluster {}T -> empty; end; canceled 6; theorem :: PRE_TOPC:12 for T being 1-sorted holds [#]T = the carrier of T; definition let T be non empty 1-sorted; cluster [#]T -> non empty; end; theorem :: PRE_TOPC:13 for T being non empty 1-sorted, p being Point of T holds p in [#]T; theorem :: PRE_TOPC:14 for T being 1-sorted, P being Subset of T holds P c= [#]T; theorem :: PRE_TOPC:15 for T being 1-sorted, P being Subset of T holds P /\ [#]T = P; theorem :: PRE_TOPC:16 for T being 1-sorted for A being set st A c= [#]T holds A is Subset of T; theorem :: PRE_TOPC:17 for T being 1-sorted, P being Subset of T holds P` = [#]T \ P; theorem :: PRE_TOPC:18 for T being 1-sorted, P being Subset of T holds P \/ P` = [#] T; theorem :: PRE_TOPC:19 for T being 1-sorted, P,Q being Subset of T holds P c= Q iff Q` c= P`; theorem :: PRE_TOPC:20 for T being 1-sorted, P being Subset of T holds P = P``; theorem :: PRE_TOPC:21 for T being 1-sorted for P,Q being Subset of T holds P c= Q` iff P misses Q; theorem :: PRE_TOPC:22 for T being 1-sorted, P being Subset of T holds [#]T \ ([#]T \ P) = P; theorem :: PRE_TOPC:23 for T being 1-sorted, P being Subset of T holds P <> [#]T iff [#]T \ P <> {}; theorem :: PRE_TOPC:24 for T being 1-sorted, P,Q being Subset of T st [#]T \ P = Q holds [#]T = P \/ Q; theorem :: PRE_TOPC:25 for T being 1-sorted, P,Q being Subset of T st [#]T = P \/ Q & P misses Q holds Q = [#]T \ P; theorem :: PRE_TOPC:26 for T being 1-sorted, P being Subset of T holds P misses P`; theorem :: PRE_TOPC:27 for T being 1-sorted holds [#]T = ({}T)`; definition let T be TopStruct, P be Subset of T; canceled; attr P is open means :: PRE_TOPC:def 5 P in the topology of T; end; definition let T be TopStruct, P be Subset of T; attr P is closed means :: PRE_TOPC:def 6 [#]T \ P is open; end; definition let T be 1-sorted, F be Subset-Family of T; redefine func union F -> Subset of T; end; definition let T be 1-sorted, F be Subset-Family of T; redefine func meet F -> Subset of T; end; definition let T be 1-sorted, F be Subset-Family of T; canceled; pred F is_a_cover_of T means :: PRE_TOPC:def 8 [#]T = union F; end; definition let T be TopStruct; mode SubSpace of T -> TopStruct means :: PRE_TOPC:def 9 [#]it c= [#]T & for P being Subset of it holds P in the topology of it iff ex Q being Subset of T st Q in the topology of T & P = Q /\ [#]it; end; definition let T be TopStruct; cluster strict SubSpace of T; end; definition let T be non empty TopStruct; cluster strict non empty SubSpace of T; end; scheme SubFamExS {A() -> TopStruct, P[Subset of A()]}: ex F being Subset-Family of A() st for B being Subset of A() holds B in F iff P[B]; definition let T be TopSpace; cluster -> TopSpace-like SubSpace of T; end; definition let T be TopStruct, P be Subset of T; func T|P -> strict SubSpace of T means :: PRE_TOPC:def 10 [#]it = P; end; definition let T be non empty TopStruct, P be non empty Subset of T; cluster T|P -> non empty; end; definition let T be TopSpace; cluster TopSpace-like strict SubSpace of T; end; definition let T be TopSpace, P be Subset of T; cluster T|P -> TopSpace-like; end; definition let S, T be 1-sorted; mode map of S, T is Function of the carrier of S, the carrier of T; canceled; end; definition let S, T be 1-sorted, f be Function of the carrier of S, the carrier of T, P be set; redefine func f.:P -> Subset of T; end; definition let S, T be 1-sorted, f be Function of the carrier of S, the carrier of T, P be set; redefine func f"P -> Subset of S; end; definition let S, T be TopStruct, f be map of S,T; attr f is continuous means :: PRE_TOPC:def 12 for P1 being Subset of T st P1 is closed holds f" P1 is closed; end; scheme TopAbstr{A() -> TopStruct,P[set]}: ex P being Subset of A() st for x being set st x in the carrier of A() holds x in P iff P[x]; canceled 11; theorem :: PRE_TOPC:39 for X' being SubSpace of T, A being Subset of X' holds A is Subset of T; canceled; theorem :: PRE_TOPC:41 for A being Subset of T st A <> {}T ex x being Point of T st x in A; theorem :: PRE_TOPC:42 [#]GX is closed; definition let T be TopSpace; cluster [#]T -> closed; end; definition let T be TopSpace; cluster closed Subset of T; end; definition let T be non empty TopSpace; cluster non empty closed Subset of T; end; theorem :: PRE_TOPC:43 for X' being SubSpace of T, B being Subset of X' holds B is closed iff ex C being Subset of T st C is closed & C /\ [#](X') = B; theorem :: PRE_TOPC:44 for F being Subset-Family of GX st for A being Subset of GX st A in F holds A is closed holds meet F is closed; :: :: The closure of a set :: definition let GX be TopStruct, A be Subset of GX; func Cl A -> Subset of GX means :: PRE_TOPC:def 13 for p being set st p in the carrier of GX holds p in it iff for G being Subset of GX st G is open holds p in G implies A meets G; end; theorem :: PRE_TOPC:45 for A being Subset of T, p being set st p in the carrier of T holds p in Cl A iff for C being Subset of T st C is closed holds (A c= C implies p in C); theorem :: PRE_TOPC:46 for A being Subset of GX ex F being Subset-Family of GX st (for C being Subset of GX holds C in F iff C is closed & A c= C) & Cl A = meet F; theorem :: PRE_TOPC:47 for X' being SubSpace of T, A being Subset of T, A1 being Subset of X' st A = A1 holds Cl A1 = (Cl A) /\ ([#]X'); theorem :: PRE_TOPC:48 for A being Subset of T holds A c= Cl A; theorem :: PRE_TOPC:49 for A,B being Subset of T st A c= B holds Cl A c= Cl B; theorem :: PRE_TOPC:50 for A,B being Subset of GX holds Cl(A \/ B) = Cl A \/ Cl B; theorem :: PRE_TOPC:51 for A, B being Subset of T holds Cl (A /\ B) c= (Cl A) /\ Cl B; theorem :: PRE_TOPC:52 for A being Subset of T holds (A is closed implies Cl A = A) & (T is TopSpace-like & Cl A = A implies A is closed); theorem :: PRE_TOPC:53 for A being Subset of T holds (A is open implies Cl([#](T) \ A) = [#](T) \ A) & (T is TopSpace-like & Cl([#](T) \ A) = [#](T) \ A implies A is open); theorem :: PRE_TOPC:54 for A being Subset of T, p being Point of T holds p in Cl A iff T is non empty & for G being Subset of T st G is open holds p in G implies A meets G;

Back to top