Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Families of Subsets, Subspaces and Mappings in Topological Spaces

**by****Agata Darmochwal**- Received June 21, 1989
- MML identifier: TOPS_2

- [ Mizar article, MML identifier index ]

environ vocabulary PRE_TOPC, SETFAM_1, SUBSET_1, BOOLE, TARSKI, FINSET_1, FUNCT_1, RELAT_1, FINSEQ_1, ORDINAL2, TOPS_2, SEQ_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, NAT_1, FINSEQ_1, FINSET_1, SETFAM_1, STRUCT_0, PRE_TOPC; constructors FUNCT_3, NAT_1, FINSEQ_1, PRE_TOPC, XREAL_0, MEMBERED; clusters PRE_TOPC, STRUCT_0, RELSET_1, ARYTM_3, MEMBERED, ZFMISC_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve x, y for set, k for Nat, T for TopStruct, GX for TopSpace, P, Q for Subset of T, M, N for Subset of T, F, G for Subset-Family of T, W, Z for Subset-Family of GX, A for SubSpace of T; :: :: A FAMILY OF SETS IN TOPOLOGICAL SPACES :: theorem :: TOPS_2:1 for T being 1-sorted, F being Subset-Family of T holds F c= bool [#]T; canceled; theorem :: TOPS_2:3 for T being 1-sorted, F being Subset-Family of T, X being set st X c= F holds X is Subset-Family of T; canceled; theorem :: TOPS_2:5 for T being non empty 1-sorted, F being Subset-Family of T st F is_a_cover_of T holds F <> {}; theorem :: TOPS_2:6 for T being 1-sorted, F, G being Subset-Family of T holds union F \ union G c= union(F \ G); canceled 2; theorem :: TOPS_2:9 for T being 1-sorted, F being Subset-Family of T holds COMPLEMENT(COMPLEMENT(F)) = F; theorem :: TOPS_2:10 for T being 1-sorted, F being Subset-Family of T holds F <> {} iff COMPLEMENT(F) <> {}; theorem :: TOPS_2:11 for T being 1-sorted, F being Subset-Family of T holds F <> {} implies meet COMPLEMENT(F) = (union F)`; theorem :: TOPS_2:12 for T being 1-sorted, F being Subset-Family of T holds F <> {} implies union COMPLEMENT(F) = (meet F)`; theorem :: TOPS_2:13 for T being 1-sorted, F being Subset-Family of T holds COMPLEMENT(F) is finite iff F is finite; :: :: CLOSED AND OPEN FAMILIES :: definition let T be TopStruct, F be Subset-Family of T; attr F is open means :: TOPS_2:def 1 for P being Subset of T holds P in F implies P is open; attr F is closed means :: TOPS_2:def 2 for P being Subset of T holds P in F implies P is closed; end; canceled 2; theorem :: TOPS_2:16 F is closed iff COMPLEMENT(F) is open; theorem :: TOPS_2:17 F is open iff COMPLEMENT(F) is closed; theorem :: TOPS_2:18 F c= G & G is open implies F is open; theorem :: TOPS_2:19 F c= G & G is closed implies F is closed; theorem :: TOPS_2:20 F is open & G is open implies F \/ G is open; theorem :: TOPS_2:21 F is open implies F /\ G is open; theorem :: TOPS_2:22 F is open implies F \ G is open; theorem :: TOPS_2:23 F is closed & G is closed implies F \/ G is closed; theorem :: TOPS_2:24 F is closed implies F /\ G is closed; theorem :: TOPS_2:25 F is closed implies F \ G is closed; theorem :: TOPS_2:26 W is open implies union W is open; theorem :: TOPS_2:27 W is open & W is finite implies meet W is open; theorem :: TOPS_2:28 W is closed & W is finite implies union W is closed; theorem :: TOPS_2:29 W is closed implies meet W is closed; :: :: SUBSPACES OF A TOPOLOGICAL SPACE :: canceled; theorem :: TOPS_2:31 for F being Subset-Family of A holds F is Subset-Family of T; theorem :: TOPS_2:32 for B being Subset of A holds B is open iff ex C being Subset of T st C is open & C /\ [#](A) = B; theorem :: TOPS_2:33 Q is open implies for P being Subset of A st P=Q holds P is open; theorem :: TOPS_2:34 Q is closed implies for P being Subset of A st P=Q holds P is closed; theorem :: TOPS_2:35 F is open implies for G being Subset-Family of A st G=F holds G is open; theorem :: TOPS_2:36 F is closed implies for G being Subset-Family of A st G=F holds G is closed; canceled; theorem :: TOPS_2:38 M /\ N is Subset of T|N; :: :: RESTRICTION OF A FAMILY :: definition let T be TopStruct, P be Subset of T, F be Subset-Family of T; func F|P -> Subset-Family of T|P means :: TOPS_2:def 3 for Q being Subset of T|P holds Q in it iff ex R being Subset of T st R in F & R /\ P = Q; end; canceled; theorem :: TOPS_2:40 F c= G implies F|M c= G|M; theorem :: TOPS_2:41 Q in F implies Q /\ M in F|M; theorem :: TOPS_2:42 Q c= union F implies Q /\ M c= union(F|M); theorem :: TOPS_2:43 M c= union F implies M = union (F|M); theorem :: TOPS_2:44 union(F|M) c= union F; theorem :: TOPS_2:45 M c= union (F|M) implies M c= union F; theorem :: TOPS_2:46 F is finite implies F|M is finite; theorem :: TOPS_2:47 F is open implies F|M is open; theorem :: TOPS_2:48 F is closed implies F|M is closed; theorem :: TOPS_2:49 for F being Subset-Family of A st F is open ex G being Subset-Family of T st G is open & for AA being Subset of T st AA = [#] A holds F = G|AA; theorem :: TOPS_2:50 ex f being Function st dom f = F & rng f = F|P & for x st x in F for Q st Q = x holds f.x = Q /\ P; :: :: MAPPING OF THE TOPOLOGICAL SPACES :: theorem :: TOPS_2:51 for T being 1-sorted, S being non empty 1-sorted, f being map of T, S holds dom f = [#]T & rng f c= [#]S; theorem :: TOPS_2:52 for T being 1-sorted, S being non empty 1-sorted, f being map of T, S holds f"([#]S) = [#]T; canceled; theorem :: TOPS_2:54 for T being 1-sorted, S being non empty 1-sorted, f being map of T, S, H being Subset-Family of S holds ("f).:H is Subset-Family of T; :: :: CONTINUOUS MAPPING :: reserve S, V for non empty TopStruct, f for map of T, S, g for map of S, V, H for Subset-Family of S, P1 for Subset of S; theorem :: TOPS_2:55 f is continuous iff (for P1 st P1 is open holds f"P1 is open); theorem :: TOPS_2:56 for T being TopSpace, S being non empty TopSpace, f being map of T, S holds f is continuous iff for P1 being Subset of S holds Cl(f"P1) c= f"(Cl P1); theorem :: TOPS_2:57 for T being TopSpace, S being non empty TopSpace, f being map of T, S holds f is continuous iff for P being Subset of T holds f.:(Cl P) c= Cl(f.:P); theorem :: TOPS_2:58 f is continuous & g is continuous implies g*f is continuous; theorem :: TOPS_2:59 f is continuous & H is open implies for F st F=("f).:H holds F is open; theorem :: TOPS_2:60 for T, S being TopStruct, f being map of T, S, H being Subset-Family of S st f is continuous & H is closed holds for F being Subset-Family of T st F=("f).:H holds F is closed; definition let T, S be 1-sorted, f be map of T,S; assume that rng f = [#]S and f is one-to-one; func f/" -> map of S,T equals :: TOPS_2:def 4 f"; synonym f"; end; canceled; theorem :: TOPS_2:62 for T being 1-sorted, S being non empty 1-sorted, f being map of T,S st rng f = [#]S & f is one-to-one holds dom(f") = [#]S & rng(f") = [#]T; theorem :: TOPS_2:63 for T, S being 1-sorted, f being map of T,S st rng f = [#]S & f is one-to-one holds f" is one-to-one; theorem :: TOPS_2:64 for T being 1-sorted, S being non empty 1-sorted, f being map of T,S st rng f = [#]S & f is one-to-one holds (f")" = f; theorem :: TOPS_2:65 for T, S being 1-sorted, f being map of T,S st rng f = [#]S & f is one-to-one holds f"*f = id dom f & f*f" = id rng f; theorem :: TOPS_2:66 for T being 1-sorted, S, V being non empty 1-sorted, f being map of T,S, g being map of S,V st dom f = [#]T & rng f = [#]S & f is one-to-one & dom g = [#]S & rng g = [#]V & g is one-to-one holds (g*f)" = f"*g"; theorem :: TOPS_2:67 for T, S being 1-sorted, f being map of T, S, P being Subset of T st rng f = [#]S & f is one-to-one holds f.:P = (f")"P; theorem :: TOPS_2:68 for T, S being 1-sorted, f being map of T,S, P1 being Subset of S st rng f = [#]S & f is one-to-one holds f"P1 = (f").:P1; :: :: HOMEOMORPHISM :: definition let S, T be TopStruct, f be map of S, T; attr f is being_homeomorphism means :: TOPS_2:def 5 dom f = [#]S & rng f = [#]T & f is one-to-one & f is continuous & f" is continuous; synonym f is_homeomorphism; end; canceled; theorem :: TOPS_2:70 f is_homeomorphism implies f" is_homeomorphism; theorem :: TOPS_2:71 for T, S, V being non empty TopStruct, f being map of T,S, g being map of S,V st f is_homeomorphism & g is_homeomorphism holds g*f is_homeomorphism; theorem :: TOPS_2:72 f is_homeomorphism iff dom f = [#]T & rng f = [#]S & f is one-to-one & for P holds P is closed iff f.:P is closed; reserve T, S for non empty TopSpace, P for Subset of T, P1 for Subset of S, f for map of T, S; theorem :: TOPS_2:73 f is_homeomorphism iff dom f = [#]T & rng f = [#]S & f is one-to-one & for P1 holds f"(Cl P1) = Cl(f"P1); theorem :: TOPS_2:74 f is_homeomorphism iff dom f = [#]T & rng f = [#] S & f is one-to-one & for P holds f.:(Cl P) = Cl(f.:P);

Back to top