:: Families of Subsets, Subspaces and Mappings in Topological Spaces :: by Agata Darmochwa{\l} :: :: Received June 21, 1989 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies SUBSET_1, PRE_TOPC, SETFAM_1, STRUCT_0, TARSKI, FUNCT_2, ZFMISC_1, XBOOLE_0, FINSET_1, FUNCT_1, RELAT_1, RCOMP_1, FINSEQ_1, NAT_1, XXREAL_0, ARYTM_3, CARD_1, ORDINAL2, VALUED_1, RELAT_2, CONNSP_1, TOPS_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, XCMPLX_0, NAT_1, FINSEQ_1, FINSET_1, SETFAM_1, STRUCT_0, PRE_TOPC, CONNSP_1; constructors SETFAM_1, PARTFUN1, FUNCT_3, XXREAL_0, XREAL_0, NAT_1, MEMBERED, FINSEQ_1, CONNSP_1, RELSET_1, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, PRE_TOPC, XREAL_0, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve x, y for set, T for TopStruct, GX for TopSpace, P, Q, 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; theorem :: TOPS_2:2 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; theorem :: TOPS_2:3 for T being non empty 1-sorted, F being Subset-Family of T st F is Cover of T holds F <> {}; theorem :: TOPS_2:4 for T being 1-sorted, F, G being Subset-Family of T holds union F \ union G c= union(F \ G); theorem :: TOPS_2:5 for T being set, F being Subset-Family of T holds F <> {} iff COMPLEMENT(F) <> {}; theorem :: TOPS_2:6 for T being set, F being Subset-Family of T holds F <> {} implies meet COMPLEMENT(F) = (union F)`; theorem :: TOPS_2:7 for T being set, F being Subset-Family of T holds F <> {} implies union COMPLEMENT(F) = (meet F)`; theorem :: TOPS_2:8 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; theorem :: TOPS_2:9 F is closed iff COMPLEMENT(F) is open; theorem :: TOPS_2:10 F is open iff COMPLEMENT(F) is closed; theorem :: TOPS_2:11 F c= G & G is open implies F is open; theorem :: TOPS_2:12 F c= G & G is closed implies F is closed; theorem :: TOPS_2:13 F is open & G is open implies F \/ G is open; theorem :: TOPS_2:14 F is open implies F /\ G is open; theorem :: TOPS_2:15 F is open implies F \ G is open; theorem :: TOPS_2:16 F is closed & G is closed implies F \/ G is closed; theorem :: TOPS_2:17 F is closed implies F /\ G is closed; theorem :: TOPS_2:18 F is closed implies F \ G is closed; theorem :: TOPS_2:19 W is open implies union W is open; theorem :: TOPS_2:20 W is open & W is finite implies meet W is open; theorem :: TOPS_2:21 W is closed & W is finite implies union W is closed; theorem :: TOPS_2:22 W is closed implies meet W is closed; :: :: SUBSPACES OF A TOPOLOGICAL SPACE :: theorem :: TOPS_2:23 for F being Subset-Family of A holds F is Subset-Family of T; theorem :: TOPS_2:24 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:25 Q is open implies for P being Subset of A st P=Q holds P is open; theorem :: TOPS_2:26 Q is closed implies for P being Subset of A st P=Q holds P is closed; theorem :: TOPS_2:27 F is open implies for G being Subset-Family of A st G=F holds G is open; theorem :: TOPS_2:28 F is closed implies for G being Subset-Family of A st G=F holds G is closed; theorem :: TOPS_2:29 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; theorem :: TOPS_2:30 F c= G implies F|M c= G|M; theorem :: TOPS_2:31 Q in F implies Q /\ M in F|M; theorem :: TOPS_2:32 Q c= union F implies Q /\ M c= union(F|M); theorem :: TOPS_2:33 M c= union F implies M = union (F|M); theorem :: TOPS_2:34 union(F|M) c= union F; theorem :: TOPS_2:35 M c= union (F|M) implies M c= union F; theorem :: TOPS_2:36 F is finite implies F|M is finite; theorem :: TOPS_2:37 F is open implies F|M is open; theorem :: TOPS_2:38 F is closed implies F|M is closed; theorem :: TOPS_2:39 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:40 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; theorem :: TOPS_2:41 for X,Y being 1-sorted, f being Function of X, Y st [#]Y = {} implies [#]X = {} holds f"([#]Y) = [#]X; theorem :: TOPS_2:42 for T being 1-sorted, S being non empty 1-sorted, f being Function of T, S, H being Subset-Family of S holds ("f).:H is Subset-Family of T; :: :: CONTINUOUS MAPPING :: reserve S for non empty TopStruct, f for Function of T, S, H for Subset-Family of S; theorem :: TOPS_2:43 for X,Y being TopStruct, f being Function of X,Y st [#]Y = {} implies [#]X = {} holds f is continuous iff for P being Subset of Y st P is open holds f"P is open; theorem :: TOPS_2:44 for T being TopSpace, S being TopSpace, f being Function 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:45 for T being TopSpace, S being non empty TopSpace, f being Function 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:46 for T,V being TopStruct,S being non empty TopStruct, f being Function of T,S, g being Function of S,V holds f is continuous & g is continuous implies g*f is continuous; theorem :: TOPS_2:47 f is continuous & H is open implies for F st F=("f).:H holds F is open; theorem :: TOPS_2:48 for T, S being TopStruct, f being Function 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 S, T be set, f be Function of S,T; assume f is bijective; func f/" -> Function of T,S equals :: TOPS_2:def 4 f"; end; notation let S, T be set, f be Function of S,T; synonym f" for f/"; end; theorem :: TOPS_2:49 for T being 1-sorted, S being non empty 1-sorted, f being Function of T,S st rng f = [#]S & f is one-to-one holds dom(f") = [#]S & rng(f") = [#]T; theorem :: TOPS_2:50 for T, S being 1-sorted, f being Function of T,S st rng f = [#]S & f is one-to-one holds f" is one-to-one; theorem :: TOPS_2:51 for T being 1-sorted, S being non empty 1-sorted, f being Function of T,S st rng f = [#]S & f is one-to-one holds (f")" = f; theorem :: TOPS_2:52 for T, S being 1-sorted, f being Function 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:53 for T being 1-sorted, S, V being non empty 1-sorted, f being Function of T,S, g being Function of S,V st 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:54 for T, S being 1-sorted, f being Function 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:55 for T, S being 1-sorted, f being Function 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 Function 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; end; theorem :: TOPS_2:56 f is being_homeomorphism implies f" is being_homeomorphism; theorem :: TOPS_2:57 for T, S, V being non empty TopStruct, f being Function of T,S, g being Function of S,V st f is being_homeomorphism & g is being_homeomorphism holds g*f is being_homeomorphism; theorem :: TOPS_2:58 f is being_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 for non empty TopSpace, S for TopSpace, P1 for Subset of S, f for Function of T, S; theorem :: TOPS_2:59 f is being_homeomorphism iff dom f = [#]T & rng f = [#]S & f is one-to-one & for P1 holds f"(Cl P1) = Cl(f"P1); reserve T for TopSpace, S for non empty TopSpace, P for Subset of T, f for Function of T, S; theorem :: TOPS_2:60 f is being_homeomorphism iff dom f = [#]T & rng f = [#]S & f is one-to-one & for P holds f.:(Cl P) = Cl(f.:P); theorem :: TOPS_2:61 :: TOPREAL5:5, AK, 21.02.2006 for X,Y being non empty TopSpace for f being Function of X,Y, A being Subset of X st f is continuous & A is connected holds f.:A is connected ; theorem :: TOPS_2:62 :: JORDAN18:2, AK, 21.02.2006 for S,T being non empty TopSpace, f being Function of S,T, A being Subset of T st f is being_homeomorphism & A is connected holds f"A is connected ; begin :: Addenda :: from JORDAN1, 2008.07.07, A.T. reserve GX,GY for non empty TopSpace; theorem :: TOPS_2:63 for GX being non empty TopSpace st (for x,y being Point of GX ex GY st (GY is connected & ex f being Function of GY,GX st f is continuous & x in rng(f )& y in rng(f))) holds GX is connected; :: Added by AK, 2009.09.20 theorem :: TOPS_2:64 for X being TopStruct, F being Subset-Family of X holds F is open iff F c= the topology of X; theorem :: TOPS_2:65 for X being TopStruct, F being Subset-Family of X holds F is closed iff F c= COMPLEMENT the topology of X; registration let X be TopStruct; cluster the topology of X -> open; cluster open for Subset-Family of X; end;