:: Families of Subsets, Subspaces and Mappings in Topological Spaces :: by Agata Darmochwa{\l} :: :: Received June 21, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin :: :: A FAMILY OF SETS IN TOPOLOGICAL SPACES :: theorem :: TOPS_2:1 for T being 1-sorted for F being Subset-Family of T holds F c= bool ([#] T) ; theorem Th2: :: TOPS_2:2 for T being 1-sorted for F being Subset-Family of T for X being set st X c= F holds X is Subset-Family of T proofend; theorem :: TOPS_2:3 for T being non empty 1-sorted for F being Subset-Family of T st F is Cover of T holds F <> {} proofend; theorem :: TOPS_2:4 for T being 1-sorted for F, G being Subset-Family of T holds (union F) \ (union G) c= union (F \ G) proofend; theorem :: TOPS_2:5 for T being set for F being Subset-Family of T holds ( F <> {} iff COMPLEMENT F <> {} ) proofend; theorem Th6: :: TOPS_2:6 for T being set for F being Subset-Family of T st F <> {} holds meet (COMPLEMENT F) = (union F) ` proofend; theorem Th7: :: TOPS_2:7 for T being set for F being Subset-Family of T st F <> {} holds union (COMPLEMENT F) = (meet F) ` proofend; Lm1: for T being 1-sorted for F being Subset-Family of T st COMPLEMENT F is finite holds F is finite proofend; theorem Th8: :: TOPS_2:8 for T being 1-sorted for F being Subset-Family of T holds ( COMPLEMENT F is finite iff F is finite ) proofend; :: :: CLOSED AND OPEN FAMILIES :: definition let T be TopStruct ; let F be Subset-Family of T; attrF is open means :Def1: :: TOPS_2:def 1 for P being Subset of T st P in F holds P is open ; attrF is closed means :Def2: :: TOPS_2:def 2 for P being Subset of T st P in F holds P is closed ; end; :: deftheorem Def1 defines open TOPS_2:def_1_:_ for T being TopStruct for F being Subset-Family of T holds ( F is open iff for P being Subset of T st P in F holds P is open ); :: deftheorem Def2 defines closed TOPS_2:def_2_:_ for T being TopStruct for F being Subset-Family of T holds ( F is closed iff for P being Subset of T st P in F holds P is closed ); theorem Th9: :: TOPS_2:9 for T being TopStruct for F being Subset-Family of T holds ( F is closed iff COMPLEMENT F is open ) proofend; theorem :: TOPS_2:10 for T being TopStruct for F being Subset-Family of T holds ( F is open iff COMPLEMENT F is closed ) proofend; theorem :: TOPS_2:11 for T being TopStruct for F, G being Subset-Family of T st F c= G & G is open holds F is open proofend; theorem :: TOPS_2:12 for T being TopStruct for F, G being Subset-Family of T st F c= G & G is closed holds F is closed proofend; theorem :: TOPS_2:13 for T being TopStruct for F, G being Subset-Family of T st F is open & G is open holds F \/ G is open proofend; theorem :: TOPS_2:14 for T being TopStruct for F, G being Subset-Family of T st F is open holds F /\ G is open proofend; theorem :: TOPS_2:15 for T being TopStruct for F, G being Subset-Family of T st F is open holds F \ G is open proofend; theorem :: TOPS_2:16 for T being TopStruct for F, G being Subset-Family of T st F is closed & G is closed holds F \/ G is closed proofend; theorem :: TOPS_2:17 for T being TopStruct for F, G being Subset-Family of T st F is closed holds F /\ G is closed proofend; theorem :: TOPS_2:18 for T being TopStruct for F, G being Subset-Family of T st F is closed holds F \ G is closed proofend; theorem Th19: :: TOPS_2:19 for GX being TopSpace for W being Subset-Family of GX st W is open holds union W is open proofend; theorem Th20: :: TOPS_2:20 for GX being TopSpace for W being Subset-Family of GX st W is open & W is finite holds meet W is open proofend; theorem :: TOPS_2:21 for GX being TopSpace for W being Subset-Family of GX st W is closed & W is finite holds union W is closed proofend; theorem :: TOPS_2:22 for GX being TopSpace for W being Subset-Family of GX st W is closed holds meet W is closed proofend; :: :: SUBSPACES OF A TOPOLOGICAL SPACE :: theorem :: TOPS_2:23 for T being TopStruct for A being SubSpace of T for F being Subset-Family of A holds F is Subset-Family of T proofend; theorem Th24: :: TOPS_2:24 for T being TopStruct for A being SubSpace of T for B being Subset of A holds ( B is open iff ex C being Subset of T st ( C is open & C /\ ([#] A) = B ) ) proofend; theorem Th25: :: TOPS_2:25 for T being TopStruct for Q being Subset of T for A being SubSpace of T st Q is open holds for P being Subset of A st P = Q holds P is open proofend; theorem Th26: :: TOPS_2:26 for T being TopStruct for Q being Subset of T for A being SubSpace of T st Q is closed holds for P being Subset of A st P = Q holds P is closed proofend; theorem :: TOPS_2:27 for T being TopStruct for F being Subset-Family of T for A being SubSpace of T st F is open holds for G being Subset-Family of A st G = F holds G is open proofend; theorem :: TOPS_2:28 for T being TopStruct for F being Subset-Family of T for A being SubSpace of T st F is closed holds for G being Subset-Family of A st G = F holds G is closed proofend; theorem Th29: :: TOPS_2:29 for T being TopStruct for M, N being Subset of T holds M /\ N is Subset of (T | N) proofend; :: :: RESTRICTION OF A FAMILY :: definition let T be TopStruct ; let P be Subset of T; let F be Subset-Family of T; funcF | P -> Subset-Family of (T | P) means :Def3: :: 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 ) ); existence ex b1 being Subset-Family of (T | P) st for Q being Subset of (T | P) holds ( Q in b1 iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) proofend; uniqueness for b1, b2 being Subset-Family of (T | P) st ( for Q being Subset of (T | P) holds ( Q in b1 iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds ( Q in b2 iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines | TOPS_2:def_3_:_ for T being TopStruct for P being Subset of T for F being Subset-Family of T for b4 being Subset-Family of (T | P) holds ( b4 = F | P iff for Q being Subset of (T | P) holds ( Q in b4 iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ); theorem :: TOPS_2:30 for T being TopStruct for M being Subset of T for F, G being Subset-Family of T st F c= G holds F | M c= G | M proofend; theorem Th31: :: TOPS_2:31 for T being TopStruct for Q, M being Subset of T for F being Subset-Family of T st Q in F holds Q /\ M in F | M proofend; theorem :: TOPS_2:32 for T being TopStruct for Q, M being Subset of T for F being Subset-Family of T st Q c= union F holds Q /\ M c= union (F | M) proofend; theorem :: TOPS_2:33 for T being TopStruct for M being Subset of T for F being Subset-Family of T st M c= union F holds M = union (F | M) proofend; theorem Th34: :: TOPS_2:34 for T being TopStruct for M being Subset of T for F being Subset-Family of T holds union (F | M) c= union F proofend; theorem :: TOPS_2:35 for T being TopStruct for M being Subset of T for F being Subset-Family of T st M c= union (F | M) holds M c= union F proofend; theorem :: TOPS_2:36 for T being TopStruct for M being Subset of T for F being Subset-Family of T st F is finite holds F | M is finite proofend; theorem :: TOPS_2:37 for T being TopStruct for M being Subset of T for F being Subset-Family of T st F is open holds F | M is open proofend; theorem :: TOPS_2:38 for T being TopStruct for M being Subset of T for F being Subset-Family of T st F is closed holds F | M is closed proofend; theorem :: TOPS_2:39 for T being TopStruct for A being SubSpace of T for F being Subset-Family of A st F is open holds ex G being Subset-Family of T st ( G is open & ( for AA being Subset of T st AA = [#] A holds F = G | AA ) ) proofend; theorem :: TOPS_2:40 for T being TopStruct for P being Subset of T for F being Subset-Family of T ex f being Function st ( dom f = F & rng f = F | P & ( for x being set st x in F holds for Q being Subset of T st Q = x holds f . x = Q /\ P ) ) proofend; theorem Th41: :: TOPS_2:41 for X, Y being 1-sorted for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds f " ([#] Y) = [#] X proofend; theorem :: TOPS_2:42 for T being 1-sorted for S being non empty 1-sorted for f being Function of T,S for H being Subset-Family of S holds (" f) .: H is Subset-Family of T proofend; theorem Th43: :: TOPS_2:43 for X, Y being TopStruct for 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 ) proofend; theorem Th44: :: TOPS_2:44 for T, S being TopSpace for 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) ) proofend; theorem Th45: :: TOPS_2:45 for T being TopSpace for S being non empty TopSpace for 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) ) proofend; theorem Th46: :: TOPS_2:46 for T, V being TopStruct for S being non empty TopStruct for f being Function of T,S for g being Function of S,V st f is continuous & g is continuous holds g * f is continuous proofend; theorem :: TOPS_2:47 for T being TopStruct for S being non empty TopStruct for f being Function of T,S for H being Subset-Family of S st f is continuous & H is open holds for F being Subset-Family of T st F = (" f) .: H holds F is open proofend; theorem :: TOPS_2:48 for T, S being TopStruct for f being Function of T,S for 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 proofend; definition let S, T be set ; let f be Function of S,T; assume A1: f is bijective ; funcf /" -> Function of T,S equals :Def4: :: TOPS_2:def 4 f " ; coherence f " is Function of T,S proofend; end; :: deftheorem Def4 defines /" TOPS_2:def_4_:_ for S, T being set for f being Function of S,T st f is bijective holds f /" = f " ; notation let S, T be set ; let f be Function of S,T; synonym f " for f /" ; end; theorem Th49: :: TOPS_2:49 for T being 1-sorted for S being non empty 1-sorted for f being Function of T,S st rng f = [#] S & f is one-to-one holds ( dom (f ") = [#] S & rng (f ") = [#] T ) proofend; theorem Th50: :: TOPS_2:50 for T, S being 1-sorted for f being Function of T,S st rng f = [#] S & f is one-to-one holds f " is one-to-one proofend; theorem Th51: :: TOPS_2:51 for T being 1-sorted for S being non empty 1-sorted for f being Function of T,S st rng f = [#] S & f is one-to-one holds (f ") " = f proofend; theorem :: TOPS_2:52 for T, S being 1-sorted for 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) ) proofend; theorem Th53: :: TOPS_2:53 for T being 1-sorted for S, V being non empty 1-sorted for f being Function of T,S for 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 ") proofend; theorem Th54: :: TOPS_2:54 for T, S being 1-sorted for f being Function of T,S for P being Subset of T st rng f = [#] S & f is one-to-one holds f .: P = (f ") " P proofend; theorem Th55: :: TOPS_2:55 for T, S being 1-sorted for f being Function of T,S for P1 being Subset of S st rng f = [#] S & f is one-to-one holds f " P1 = (f ") .: P1 proofend; :: :: HOMEOMORPHISM :: definition let S, T be TopStruct ; let f be Function of S,T; attrf is being_homeomorphism means :Def5: :: TOPS_2:def 5 ( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous ); end; :: deftheorem Def5 defines being_homeomorphism TOPS_2:def_5_:_ for S, T being TopStruct for f being Function of S,T holds ( f is being_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous ) ); theorem :: TOPS_2:56 for T being TopStruct for S being non empty TopStruct for f being Function of T,S st f is being_homeomorphism holds f " is being_homeomorphism proofend; theorem :: TOPS_2:57 for T, S, V being non empty TopStruct for f being Function of T,S for g being Function of S,V st f is being_homeomorphism & g is being_homeomorphism holds g * f is being_homeomorphism proofend; theorem :: TOPS_2:58 for T being TopStruct for S being non empty TopStruct for f being Function of T,S holds ( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds ( P is closed iff f .: P is closed ) ) ) ) proofend; theorem :: TOPS_2:59 for T being non empty TopSpace for S being TopSpace for f being Function of T,S holds ( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) ) proofend; theorem :: TOPS_2:60 for T being TopSpace for S being non empty TopSpace for f being Function of T,S holds ( f is being_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) ) proofend; theorem Th61: :: TOPS_2:61 for X, Y being non empty TopSpace for f being Function of X,Y for A being Subset of X st f is continuous & A is connected holds f .: A is connected proofend; theorem :: TOPS_2:62 for S, T being non empty TopSpace for f being Function of S,T for A being Subset of T st f is being_homeomorphism & A is connected holds f " A is connected proofend; begin theorem :: TOPS_2:63 for GX being non empty TopSpace st ( for x, y being Point of GX ex GY being non empty TopSpace 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 proofend; :: Added by AK, 2009.09.20 theorem Th64: :: TOPS_2:64 for X being TopStruct for F being Subset-Family of X holds ( F is open iff F c= the topology of X ) proofend; theorem :: TOPS_2:65 for X being TopStruct for F being Subset-Family of X holds ( F is closed iff F c= COMPLEMENT the topology of X ) proofend; registration let X be TopStruct ; cluster the topology of X -> open ; coherence the topology of X is open by Th64; cluster open for Element of bool (bool the carrier of X); existence ex b1 being Subset-Family of X st b1 is open proofend; end;