:: TOPS_2 semantic presentation begin 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 proof let T be 1-sorted ; ::_thesis: for F being Subset-Family of T for X being set st X c= F holds X is Subset-Family of T let F be Subset-Family of T; ::_thesis: for X being set st X c= F holds X is Subset-Family of T let X be set ; ::_thesis: ( X c= F implies X is Subset-Family of T ) assume A1: X c= F ; ::_thesis: X is Subset-Family of T X c= bool the carrier of T proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in bool the carrier of T ) assume y in X ; ::_thesis: y in bool the carrier of T then y in F by A1; hence y in bool the carrier of T ; ::_thesis: verum end; hence X is Subset-Family of T ; ::_thesis: verum end; 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 <> {} proof let T be non empty 1-sorted ; ::_thesis: for F being Subset-Family of T st F is Cover of T holds F <> {} let F be Subset-Family of T; ::_thesis: ( F is Cover of T implies F <> {} ) set x = the Element of union F; assume F is Cover of T ; ::_thesis: F <> {} then union F = the carrier of T by SETFAM_1:45; then ex A being set st ( the Element of union F in A & A in F ) by TARSKI:def_4; hence F <> {} ; ::_thesis: verum end; 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) proof let T be 1-sorted ; ::_thesis: for F, G being Subset-Family of T holds (union F) \ (union G) c= union (F \ G) let F, G be Subset-Family of T; ::_thesis: (union F) \ (union G) c= union (F \ G) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (union F) \ (union G) or x in union (F \ G) ) assume A1: x in (union F) \ (union G) ; ::_thesis: x in union (F \ G) then x in union F by XBOOLE_0:def_5; then consider A being set such that A2: x in A and A3: A in F by TARSKI:def_4; not x in union G by A1, XBOOLE_0:def_5; then not A in G by A2, TARSKI:def_4; then A in F \ G by A3, XBOOLE_0:def_5; hence x in union (F \ G) by A2, TARSKI:def_4; ::_thesis: verum end; theorem :: TOPS_2:5 for T being set for F being Subset-Family of T holds ( F <> {} iff COMPLEMENT F <> {} ) proof let T be set ; ::_thesis: for F being Subset-Family of T holds ( F <> {} iff COMPLEMENT F <> {} ) let F be Subset-Family of T; ::_thesis: ( F <> {} iff COMPLEMENT F <> {} ) thus ( F <> {} implies COMPLEMENT F <> {} ) by SETFAM_1:32; ::_thesis: ( COMPLEMENT F <> {} implies F <> {} ) assume COMPLEMENT F <> {} ; ::_thesis: F <> {} then COMPLEMENT (COMPLEMENT F) <> {} by SETFAM_1:32; hence F <> {} ; ::_thesis: verum end; theorem Th6: :: TOPS_2:6 for T being set for F being Subset-Family of T st F <> {} holds meet (COMPLEMENT F) = (union F) ` proof let T be set ; ::_thesis: for F being Subset-Family of T st F <> {} holds meet (COMPLEMENT F) = (union F) ` let F be Subset-Family of T; ::_thesis: ( F <> {} implies meet (COMPLEMENT F) = (union F) ` ) assume F <> {} ; ::_thesis: meet (COMPLEMENT F) = (union F) ` then meet (COMPLEMENT F) = ([#] T) \ (union F) by SETFAM_1:33; hence meet (COMPLEMENT F) = (union F) ` ; ::_thesis: verum end; theorem Th7: :: TOPS_2:7 for T being set for F being Subset-Family of T st F <> {} holds union (COMPLEMENT F) = (meet F) ` proof let T be set ; ::_thesis: for F being Subset-Family of T st F <> {} holds union (COMPLEMENT F) = (meet F) ` let F be Subset-Family of T; ::_thesis: ( F <> {} implies union (COMPLEMENT F) = (meet F) ` ) assume F <> {} ; ::_thesis: union (COMPLEMENT F) = (meet F) ` then union (COMPLEMENT F) = ([#] T) \ (meet F) by SETFAM_1:34 .= T \ (meet F) ; hence union (COMPLEMENT F) = (meet F) ` ; ::_thesis: verum end; Lm1: for T being 1-sorted for F being Subset-Family of T st COMPLEMENT F is finite holds F is finite proof let T be 1-sorted ; ::_thesis: for F being Subset-Family of T st COMPLEMENT F is finite holds F is finite let F be Subset-Family of T; ::_thesis: ( COMPLEMENT F is finite implies F is finite ) defpred S1[ set , set ] means for X being Subset of T st X = \$1 holds \$2 = X ` ; A1: for x being set st x in COMPLEMENT F holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in COMPLEMENT F implies ex y being set st S1[x,y] ) assume x in COMPLEMENT F ; ::_thesis: ex y being set st S1[x,y] then reconsider X = x as Subset of T ; reconsider y = X ` as set ; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider f being Function such that A2: dom f = COMPLEMENT F and A3: for x being set st x in COMPLEMENT F holds S1[x,f . x] from CLASSES1:sch_1(A1); for x being set holds ( x in rng f iff x in F ) proof let x be set ; ::_thesis: ( x in rng f iff x in F ) hereby ::_thesis: ( x in F implies x in rng f ) assume x in rng f ; ::_thesis: x in F then consider y being set such that A4: y in dom f and A5: x = f . y by FUNCT_1:def_3; reconsider Y = y as Subset of T by A2, A4; Y ` in F by A2, A4, SETFAM_1:def_7; hence x in F by A2, A3, A4, A5; ::_thesis: verum end; assume A6: x in F ; ::_thesis: x in rng f then reconsider X = x as Subset of T ; A7: (X `) ` = X ; then X ` in COMPLEMENT F by A6, SETFAM_1:def_7; then A8: f . (X `) = (X `) ` by A3; X ` in dom f by A2, A6, A7, SETFAM_1:def_7; hence x in rng f by A8, FUNCT_1:def_3; ::_thesis: verum end; then rng f = F by TARSKI:1; then A9: f .: (COMPLEMENT F) = F by A2, RELAT_1:113; assume COMPLEMENT F is finite ; ::_thesis: F is finite hence F is finite by A9, FINSET_1:5; ::_thesis: verum end; 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 ) proof let T be 1-sorted ; ::_thesis: for F being Subset-Family of T holds ( COMPLEMENT F is finite iff F is finite ) let F be Subset-Family of T; ::_thesis: ( COMPLEMENT F is finite iff F is finite ) thus ( COMPLEMENT F is finite implies F is finite ) by Lm1; ::_thesis: ( F is finite implies COMPLEMENT F is finite ) assume F is finite ; ::_thesis: COMPLEMENT F is finite then COMPLEMENT (COMPLEMENT F) is finite ; hence COMPLEMENT F is finite by Lm1; ::_thesis: verum end; 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 ) proof let T be TopStruct ; ::_thesis: for F being Subset-Family of T holds ( F is closed iff COMPLEMENT F is open ) let F be Subset-Family of T; ::_thesis: ( F is closed iff COMPLEMENT F is open ) thus ( F is closed implies COMPLEMENT F is open ) ::_thesis: ( COMPLEMENT F is open implies F is closed ) proof assume A1: F is closed ; ::_thesis: COMPLEMENT F is open let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( P in COMPLEMENT F implies P is open ) assume P in COMPLEMENT F ; ::_thesis: P is open then P ` in F by SETFAM_1:def_7; then P ` is closed by A1, Def2; hence P is open by TOPS_1:4; ::_thesis: verum end; assume A2: COMPLEMENT F is open ; ::_thesis: F is closed let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( P in F implies P is closed ) assume A3: P in F ; ::_thesis: P is closed (P `) ` = P ; then P ` in COMPLEMENT F by A3, SETFAM_1:def_7; then P ` is open by A2, Def1; hence P is closed by TOPS_1:3; ::_thesis: verum end; theorem :: TOPS_2:10 for T being TopStruct for F being Subset-Family of T holds ( F is open iff COMPLEMENT F is closed ) proof let T be TopStruct ; ::_thesis: for F being Subset-Family of T holds ( F is open iff COMPLEMENT F is closed ) let F be Subset-Family of T; ::_thesis: ( F is open iff COMPLEMENT F is closed ) F = COMPLEMENT (COMPLEMENT F) ; hence ( F is open iff COMPLEMENT F is closed ) by Th9; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F c= G & G is open holds F is open let F, G be Subset-Family of T; ::_thesis: ( F c= G & G is open implies F is open ) assume A1: ( F c= G & G is open ) ; ::_thesis: F is open let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( P in F implies P is open ) assume P in F ; ::_thesis: P is open hence P is open by A1, Def1; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F c= G & G is closed holds F is closed let F, G be Subset-Family of T; ::_thesis: ( F c= G & G is closed implies F is closed ) assume A1: ( F c= G & G is closed ) ; ::_thesis: F is closed let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( P in F implies P is closed ) assume P in F ; ::_thesis: P is closed hence P is closed by A1, Def2; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is open & G is open holds F \/ G is open let F, G be Subset-Family of T; ::_thesis: ( F is open & G is open implies F \/ G is open ) assume A1: ( F is open & G is open ) ; ::_thesis: F \/ G is open let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( P in F \/ G implies P is open ) assume P in F \/ G ; ::_thesis: P is open then ( P in F or P in G ) by XBOOLE_0:def_3; hence P is open by A1, Def1; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is open holds F /\ G is open let F, G be Subset-Family of T; ::_thesis: ( F is open implies F /\ G is open ) assume A1: F is open ; ::_thesis: F /\ G is open let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( P in F /\ G implies P is open ) assume P in F /\ G ; ::_thesis: P is open then P in F by XBOOLE_0:def_4; hence P is open by A1, Def1; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is open holds F \ G is open let F, G be Subset-Family of T; ::_thesis: ( F is open implies F \ G is open ) assume A1: F is open ; ::_thesis: F \ G is open let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( P in F \ G implies P is open ) assume P in F \ G ; ::_thesis: P is open then P in F by XBOOLE_0:def_5; hence P is open by A1, Def1; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is closed & G is closed holds F \/ G is closed let F, G be Subset-Family of T; ::_thesis: ( F is closed & G is closed implies F \/ G is closed ) assume A1: ( F is closed & G is closed ) ; ::_thesis: F \/ G is closed let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( P in F \/ G implies P is closed ) assume P in F \/ G ; ::_thesis: P is closed then ( P in F or P in G ) by XBOOLE_0:def_3; hence P is closed by A1, Def2; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is closed holds F /\ G is closed let F, G be Subset-Family of T; ::_thesis: ( F is closed implies F /\ G is closed ) assume A1: F is closed ; ::_thesis: F /\ G is closed let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( P in F /\ G implies P is closed ) assume P in F /\ G ; ::_thesis: P is closed then P in F by XBOOLE_0:def_4; hence P is closed by A1, Def2; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for F, G being Subset-Family of T st F is closed holds F \ G is closed let F, G be Subset-Family of T; ::_thesis: ( F is closed implies F \ G is closed ) assume A1: F is closed ; ::_thesis: F \ G is closed let P be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( P in F \ G implies P is closed ) assume P in F \ G ; ::_thesis: P is closed then P in F by XBOOLE_0:def_5; hence P is closed by A1, Def2; ::_thesis: verum end; 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 proof let GX be TopSpace; ::_thesis: for W being Subset-Family of GX st W is open holds union W is open let W be Subset-Family of GX; ::_thesis: ( W is open implies union W is open ) assume A1: W is open ; ::_thesis: union W is open W c= the topology of GX proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in W or x in the topology of GX ) assume A2: x in W ; ::_thesis: x in the topology of GX then reconsider X = x as Subset of GX ; X is open by A1, A2, Def1; hence x in the topology of GX by PRE_TOPC:def_2; ::_thesis: verum end; then union W in the topology of GX by PRE_TOPC:def_1; hence union W is open by PRE_TOPC:def_2; ::_thesis: verum end; 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 proof let GX be TopSpace; ::_thesis: for W being Subset-Family of GX st W is open & W is finite holds meet W is open let W be Subset-Family of GX; ::_thesis: ( W is open & W is finite implies meet W is open ) assume that A1: W is open and A2: W is finite ; ::_thesis: meet W is open consider p being FinSequence such that A3: rng p = W by A2, FINSEQ_1:52; consider n being Nat such that A4: dom p = Seg n by FINSEQ_1:def_2; defpred S1[ Nat] means for Z being Subset-Family of GX st Z = p .: (Seg \$1) & \$1 <= n & 1 <= n holds meet Z is open ; A5: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: for Z being Subset-Family of GX st Z = p .: (Seg k) & k <= n & 1 <= n holds meet Z is open ; ::_thesis: S1[k + 1] let Z be Subset-Family of GX; ::_thesis: ( Z = p .: (Seg (k + 1)) & k + 1 <= n & 1 <= n implies meet Z is open ) assume A7: Z = p .: (Seg (k + 1)) ; ::_thesis: ( not k + 1 <= n or not 1 <= n or meet Z is open ) assume that A8: k + 1 <= n and A9: 1 <= n ; ::_thesis: meet Z is open A10: now__::_thesis:_(_0_<_k_implies_meet_Z_is_open_) reconsider G2 = Im (p,(k + 1)) as Subset-Family of GX by A3, Th2, RELAT_1:111; reconsider G1 = p .: (Seg k) as Subset-Family of GX by A3, Th2, RELAT_1:111; assume A11: 0 < k ; ::_thesis: meet Z is open k + 1 <= n + 1 by A8, NAT_1:12; then k <= n by XREAL_1:6; then Seg k c= dom p by A4, FINSEQ_1:5; then A12: G1 <> {} by A11, RELAT_1:119; k + 1 <= n + 1 by A8, NAT_1:12; then k <= n by XREAL_1:6; then A13: meet G1 is open by A6, A9; ( 0 <= k & 0 + 1 = 1 ) by NAT_1:2; then 1 <= k + 1 by XREAL_1:7; then A14: k + 1 in dom p by A4, A8, FINSEQ_1:1; then G2 = {(p . (k + 1))} by FUNCT_1:59; then A15: meet G2 = p . (k + 1) by SETFAM_1:10; {(k + 1)} c= dom p by A14, ZFMISC_1:31; then A16: G2 <> {} by RELAT_1:119; p . (k + 1) in W by A3, A14, FUNCT_1:def_3; then A17: meet G2 is open by A1, A15, Def1; p .: (Seg (k + 1)) = p .: ((Seg k) \/ {(k + 1)}) by FINSEQ_1:9 .= (p .: (Seg k)) \/ (p .: {(k + 1)}) by RELAT_1:120 ; then meet Z = (meet G1) /\ (meet G2) by A7, A12, A16, SETFAM_1:9; hence meet Z is open by A13, A17, TOPS_1:11; ::_thesis: verum end; now__::_thesis:_(_k_=_0_implies_meet_Z_is_open_) assume A18: k = 0 ; ::_thesis: meet Z is open then A19: 1 in dom p by A4, A8, FINSEQ_1:1; then Im (p,1) = {(p . 1)} by FUNCT_1:59; then meet Z = p . 1 by A7, A18, FINSEQ_1:2, SETFAM_1:10; then meet Z in W by A3, A19, FUNCT_1:def_3; hence meet Z is open by A1, Def1; ::_thesis: verum end; hence meet Z is open by A10, NAT_1:3; ::_thesis: verum end; A20: S1[ 0 ] proof let Z be Subset-Family of GX; ::_thesis: ( Z = p .: (Seg 0) & 0 <= n & 1 <= n implies meet Z is open ) assume that A21: Z = p .: (Seg 0) and 0 <= n ; ::_thesis: ( not 1 <= n or meet Z is open ) A22: {} in the topology of GX by PRE_TOPC:1; meet Z = {} by A21, SETFAM_1:1; hence ( not 1 <= n or meet Z is open ) by A22, PRE_TOPC:def_2; ::_thesis: verum end; A23: for k being Nat holds S1[k] from NAT_1:sch_2(A20, A5); A24: now__::_thesis:_(_1_<=_n_implies_meet_W_is_open_) assume A25: 1 <= n ; ::_thesis: meet W is open W = p .: (Seg n) by A3, A4, RELAT_1:113; hence meet W is open by A23, A25; ::_thesis: verum end; A26: now__::_thesis:_(_n_=_0_implies_meet_W_is_open_) assume n = 0 ; ::_thesis: meet W is open then Seg n = {} ; then W = p .: {} by A3, A4, RELAT_1:113; then A27: meet W = {} by SETFAM_1:1; {} in the topology of GX by PRE_TOPC:1; hence meet W is open by A27, PRE_TOPC:def_2; ::_thesis: verum end; now__::_thesis:_(_n_<>_0_implies_1_<=_n_) assume n <> 0 ; ::_thesis: 1 <= n then A28: 0 < n by NAT_1:3; 1 = 0 + 1 ; hence 1 <= n by A28, NAT_1:13; ::_thesis: verum end; hence meet W is open by A24, A26; ::_thesis: verum end; 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 proof let GX be TopSpace; ::_thesis: for W being Subset-Family of GX st W is closed & W is finite holds union W is closed let W be Subset-Family of GX; ::_thesis: ( W is closed & W is finite implies union W is closed ) reconsider C = COMPLEMENT W as Subset-Family of GX ; assume ( W is closed & W is finite ) ; ::_thesis: union W is closed then ( COMPLEMENT W is open & COMPLEMENT W is finite ) by Th8, Th9; then A1: meet C is open by Th20; now__::_thesis:_(_W_<>_{}_implies_union_W_is_closed_) assume W <> {} ; ::_thesis: union W is closed then meet (COMPLEMENT W) = (union W) ` by Th6; hence union W is closed by A1, TOPS_1:3; ::_thesis: verum end; hence union W is closed by ZFMISC_1:2; ::_thesis: verum end; theorem :: TOPS_2:22 for GX being TopSpace for W being Subset-Family of GX st W is closed holds meet W is closed proof let GX be TopSpace; ::_thesis: for W being Subset-Family of GX st W is closed holds meet W is closed let W be Subset-Family of GX; ::_thesis: ( W is closed implies meet W is closed ) reconsider C = COMPLEMENT W as Subset-Family of GX ; assume W is closed ; ::_thesis: meet W is closed then COMPLEMENT W is open by Th9; then A1: union C is open by Th19; A2: now__::_thesis:_(_W_<>_{}_implies_meet_W_is_closed_) assume W <> {} ; ::_thesis: meet W is closed then union (COMPLEMENT W) = (meet W) ` by Th7; hence meet W is closed by A1, TOPS_1:3; ::_thesis: verum end; now__::_thesis:_(_W_=_{}_implies_meet_W_is_closed_) assume W = {} ; ::_thesis: meet W is closed then meet W = {} GX by SETFAM_1:def_1; hence meet W is closed ; ::_thesis: verum end; hence meet W is closed by A2; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for A being SubSpace of T for F being Subset-Family of A holds F is Subset-Family of T let A be SubSpace of T; ::_thesis: for F being Subset-Family of A holds F is Subset-Family of T let F be Subset-Family of A; ::_thesis: F is Subset-Family of T [#] A c= [#] T by PRE_TOPC:def_4; then bool the carrier of A c= bool the carrier of T by ZFMISC_1:67; hence F is Subset-Family of T by XBOOLE_1:1; ::_thesis: verum end; 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 ) ) proof let T be TopStruct ; ::_thesis: 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 ) ) let A be SubSpace of T; ::_thesis: for B being Subset of A holds ( B is open iff ex C being Subset of T st ( C is open & C /\ ([#] A) = B ) ) let B be Subset of A; ::_thesis: ( B is open iff ex C being Subset of T st ( C is open & C /\ ([#] A) = B ) ) hereby ::_thesis: ( ex C being Subset of T st ( C is open & C /\ ([#] A) = B ) implies B is open ) assume B is open ; ::_thesis: ex C being Subset of T st ( C is open & C /\ ([#] A) = B ) then B in the topology of A by PRE_TOPC:def_2; then consider C being Subset of T such that A1: ( C in the topology of T & C /\ ([#] A) = B ) by PRE_TOPC:def_4; reconsider C = C as Subset of T ; take C = C; ::_thesis: ( C is open & C /\ ([#] A) = B ) thus ( C is open & C /\ ([#] A) = B ) by A1, PRE_TOPC:def_2; ::_thesis: verum end; given C being Subset of T such that A2: C is open and A3: C /\ ([#] A) = B ; ::_thesis: B is open C in the topology of T by A2, PRE_TOPC:def_2; then B in the topology of A by A3, PRE_TOPC:def_4; hence B is open by PRE_TOPC:def_2; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: 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 let Q be Subset of T; ::_thesis: for A being SubSpace of T st Q is open holds for P being Subset of A st P = Q holds P is open let A be SubSpace of T; ::_thesis: ( Q is open implies for P being Subset of A st P = Q holds P is open ) assume A1: Q is open ; ::_thesis: for P being Subset of A st P = Q holds P is open let P be Subset of A; ::_thesis: ( P = Q implies P is open ) assume P = Q ; ::_thesis: P is open then Q /\ ([#] A) = P by XBOOLE_1:28; hence P is open by A1, Th24; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: 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 let Q be Subset of T; ::_thesis: for A being SubSpace of T st Q is closed holds for P being Subset of A st P = Q holds P is closed let A be SubSpace of T; ::_thesis: ( Q is closed implies for P being Subset of A st P = Q holds P is closed ) assume A1: Q is closed ; ::_thesis: for P being Subset of A st P = Q holds P is closed let P be Subset of A; ::_thesis: ( P = Q implies P is closed ) assume P = Q ; ::_thesis: P is closed then Q /\ ([#] A) = P by XBOOLE_1:28; hence P is closed by A1, PRE_TOPC:13; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: 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 let F be Subset-Family of T; ::_thesis: 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 let A be SubSpace of T; ::_thesis: ( F is open implies for G being Subset-Family of A st G = F holds G is open ) assume A1: F is open ; ::_thesis: for G being Subset-Family of A st G = F holds G is open let G be Subset-Family of A; ::_thesis: ( G = F implies G is open ) assume A2: G = F ; ::_thesis: G is open let P be Subset of A; :: according to TOPS_2:def_1 ::_thesis: ( P in G implies P is open ) assume A3: P in G ; ::_thesis: P is open reconsider PP = P as Subset of T by PRE_TOPC:11; PP is open by A1, A2, A3, Def1; hence P is open by Th25; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: 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 let F be Subset-Family of T; ::_thesis: 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 let A be SubSpace of T; ::_thesis: ( F is closed implies for G being Subset-Family of A st G = F holds G is closed ) assume A1: F is closed ; ::_thesis: for G being Subset-Family of A st G = F holds G is closed let G be Subset-Family of A; ::_thesis: ( G = F implies G is closed ) assume A2: G = F ; ::_thesis: G is closed let P be Subset of A; :: according to TOPS_2:def_2 ::_thesis: ( P in G implies P is closed ) assume A3: P in G ; ::_thesis: P is closed reconsider PP = P as Subset of T by PRE_TOPC:11; PP is closed by A1, A2, A3, Def2; hence P is closed by Th26; ::_thesis: verum end; theorem Th29: :: TOPS_2:29 for T being TopStruct for M, N being Subset of T holds M /\ N is Subset of (T | N) proof let T be TopStruct ; ::_thesis: for M, N being Subset of T holds M /\ N is Subset of (T | N) let M, N be Subset of T; ::_thesis: M /\ N is Subset of (T | N) M /\ N c= N by XBOOLE_1:17; then M /\ N c= [#] (T | N) by PRE_TOPC:def_5; hence M /\ N is Subset of (T | N) ; ::_thesis: verum end; 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 ) ) proof thus ex G being Subset-Family of (T | P) st for Q being Subset of (T | P) holds ( Q in G iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ::_thesis: verum proof defpred S1[ Subset of (T | P)] means ex R being Subset of T st ( R in F & R /\ P = \$1 ); ex G being Subset-Family of (T | P) st for Q being Subset of (T | P) holds ( Q in G iff S1[Q] ) from SUBSET_1:sch_3(); hence ex G being Subset-Family of (T | P) st for Q being Subset of (T | P) holds ( Q in G iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ; ::_thesis: verum end; end; 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 proof thus for G, H being Subset-Family of (T | P) st ( for Q being Subset of (T | P) holds ( Q in G iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds ( Q in H iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ) holds G = H ::_thesis: verum proof let G, H be Subset-Family of (T | P); ::_thesis: ( ( for Q being Subset of (T | P) holds ( Q in G iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ) & ( for Q being Subset of (T | P) holds ( Q in H iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ) implies G = H ) assume that A1: for Q being Subset of (T | P) holds ( Q in G iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) and A2: for Q being Subset of (T | P) holds ( Q in H iff ex R being Subset of T st ( R in F & R /\ P = Q ) ) ; ::_thesis: G = H for x being set holds ( x in G iff x in H ) proof let x be set ; ::_thesis: ( x in G iff x in H ) hereby ::_thesis: ( x in H implies x in G ) assume A3: x in G ; ::_thesis: x in H then reconsider X = x as Subset of (T | P) ; ex R being Subset of T st ( R in F & R /\ P = X ) by A1, A3; hence x in H by A2; ::_thesis: verum end; assume A4: x in H ; ::_thesis: x in G then reconsider X = x as Subset of (T | P) ; ex R being Subset of T st ( R in F & R /\ P = X ) by A2, A4; hence x in G by A1; ::_thesis: verum end; hence G = H by TARSKI:1; ::_thesis: verum end; end; 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 proof let T be TopStruct ; ::_thesis: for M being Subset of T for F, G being Subset-Family of T st F c= G holds F | M c= G | M let M be Subset of T; ::_thesis: for F, G being Subset-Family of T st F c= G holds F | M c= G | M let F, G be Subset-Family of T; ::_thesis: ( F c= G implies F | M c= G | M ) assume A1: F c= G ; ::_thesis: F | M c= G | M let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F | M or x in G | M ) assume A2: x in F | M ; ::_thesis: x in G | M then reconsider X = x as Subset of (T | M) ; ex R being Subset of T st ( R in F & R /\ M = X ) by A2, Def3; hence x in G | M by A1, Def3; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for Q, M being Subset of T for F being Subset-Family of T st Q in F holds Q /\ M in F | M let Q, M be Subset of T; ::_thesis: for F being Subset-Family of T st Q in F holds Q /\ M in F | M let F be Subset-Family of T; ::_thesis: ( Q in F implies Q /\ M in F | M ) reconsider QQ = Q /\ M as Subset of (T | M) by Th29; A1: Q /\ M = QQ ; assume Q in F ; ::_thesis: Q /\ M in F | M hence Q /\ M in F | M by A1, Def3; ::_thesis: verum end; 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) proof let T be TopStruct ; ::_thesis: 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) let Q, M be Subset of T; ::_thesis: for F being Subset-Family of T st Q c= union F holds Q /\ M c= union (F | M) let F be Subset-Family of T; ::_thesis: ( Q c= union F implies Q /\ M c= union (F | M) ) assume A1: Q c= union F ; ::_thesis: Q /\ M c= union (F | M) now__::_thesis:_(_M_<>_{}_implies_Q_/\_M_c=_union_(F_|_M)_) assume M <> {} ; ::_thesis: Q /\ M c= union (F | M) thus Q /\ M c= union (F | M) ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q /\ M or x in union (F | M) ) assume A2: x in Q /\ M ; ::_thesis: x in union (F | M) then x in Q by XBOOLE_0:def_4; then consider Z being set such that A3: x in Z and A4: Z in F by A1, TARSKI:def_4; reconsider ZZ = Z as Subset of T by A4; ZZ /\ M in F | M by A4, Th31; then reconsider ZP = ZZ /\ M as Subset of (T | M) ; A5: ZP in F | M by A4, Th31; x in M by A2, XBOOLE_0:def_4; then x in ZP by A3, XBOOLE_0:def_4; hence x in union (F | M) by A5, TARSKI:def_4; ::_thesis: verum end; end; hence Q /\ M c= union (F | M) by XBOOLE_1:2; ::_thesis: verum end; 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) proof let T be TopStruct ; ::_thesis: for M being Subset of T for F being Subset-Family of T st M c= union F holds M = union (F | M) let M be Subset of T; ::_thesis: for F being Subset-Family of T st M c= union F holds M = union (F | M) let F be Subset-Family of T; ::_thesis: ( M c= union F implies M = union (F | M) ) assume A1: M c= union F ; ::_thesis: M = union (F | M) for x being set holds ( x in M iff x in union (F | M) ) proof let x be set ; ::_thesis: ( x in M iff x in union (F | M) ) hereby ::_thesis: ( x in union (F | M) implies x in M ) assume A2: x in M ; ::_thesis: x in union (F | M) then consider A being set such that A3: x in A and A4: A in F by A1, TARSKI:def_4; reconsider A9 = A as Subset of T by A4; A /\ M c= M by XBOOLE_1:17; then A /\ M c= [#] (T | M) by PRE_TOPC:def_5; then reconsider B = A9 /\ M as Subset of (T | M) ; A5: B in F | M by A4, Def3; x in A /\ M by A2, A3, XBOOLE_0:def_4; hence x in union (F | M) by A5, TARSKI:def_4; ::_thesis: verum end; assume x in union (F | M) ; ::_thesis: x in M then consider A being set such that A6: x in A and A7: A in F | M by TARSKI:def_4; reconsider B = A as Subset of (T | M) by A7; ex R being Subset of T st ( R in F & R /\ M = B ) by A7, Def3; hence x in M by A6, XBOOLE_0:def_4; ::_thesis: verum end; hence M = union (F | M) by TARSKI:1; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for M being Subset of T for F being Subset-Family of T holds union (F | M) c= union F let M be Subset of T; ::_thesis: for F being Subset-Family of T holds union (F | M) c= union F let F be Subset-Family of T; ::_thesis: union (F | M) c= union F let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union (F | M) or x in union F ) assume x in union (F | M) ; ::_thesis: x in union F then consider A being set such that A1: x in A and A2: A in F | M by TARSKI:def_4; reconsider Q = A as Subset of (T | M) by A2; consider R being Subset of T such that A3: R in F and A4: R /\ M = Q by A2, Def3; x in R by A1, A4, XBOOLE_0:def_4; hence x in union F by A3, TARSKI:def_4; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for M being Subset of T for F being Subset-Family of T st M c= union (F | M) holds M c= union F let M be Subset of T; ::_thesis: for F being Subset-Family of T st M c= union (F | M) holds M c= union F let F be Subset-Family of T; ::_thesis: ( M c= union (F | M) implies M c= union F ) assume A1: M c= union (F | M) ; ::_thesis: M c= union F union (F | M) c= union F by Th34; hence M c= union F by A1, XBOOLE_1:1; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for M being Subset of T for F being Subset-Family of T st F is finite holds F | M is finite let M be Subset of T; ::_thesis: for F being Subset-Family of T st F is finite holds F | M is finite let F be Subset-Family of T; ::_thesis: ( F is finite implies F | M is finite ) defpred S1[ set , set ] means for X being Subset of T st X = \$1 holds \$2 = X /\ M; A1: for x being set st x in F holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in F implies ex y being set st S1[x,y] ) assume x in F ; ::_thesis: ex y being set st S1[x,y] then reconsider X = x as Subset of T ; reconsider y = X /\ M as set ; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider f being Function such that A2: dom f = F and A3: for x being set st x in F holds S1[x,f . x] from CLASSES1:sch_1(A1); for x being set holds ( x in rng f iff x in F | M ) proof let x be set ; ::_thesis: ( x in rng f iff x in F | M ) hereby ::_thesis: ( x in F | M implies x in rng f ) assume x in rng f ; ::_thesis: x in F | M then consider y being set such that A4: y in dom f and A5: x = f . y by FUNCT_1:def_3; reconsider Y = y as Subset of T by A2, A4; Y /\ M c= M by XBOOLE_1:17; then Y /\ M c= [#] (T | M) by PRE_TOPC:def_5; then reconsider X = f . y as Subset of (T | M) by A2, A3, A4; f . y = Y /\ M by A2, A3, A4; then X in F | M by A2, A4, Def3; hence x in F | M by A5; ::_thesis: verum end; assume A6: x in F | M ; ::_thesis: x in rng f then reconsider X = x as Subset of (T | M) ; consider R being Subset of T such that A7: R in F and A8: R /\ M = X by A6, Def3; f . R = R /\ M by A3, A7; hence x in rng f by A2, A7, A8, FUNCT_1:def_3; ::_thesis: verum end; then rng f = F | M by TARSKI:1; then A9: f .: F = F | M by A2, RELAT_1:113; assume F is finite ; ::_thesis: F | M is finite hence F | M is finite by A9, FINSET_1:5; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for M being Subset of T for F being Subset-Family of T st F is open holds F | M is open let M be Subset of T; ::_thesis: for F being Subset-Family of T st F is open holds F | M is open let F be Subset-Family of T; ::_thesis: ( F is open implies F | M is open ) assume A1: F is open ; ::_thesis: F | M is open let Q be Subset of (T | M); :: according to TOPS_2:def_1 ::_thesis: ( Q in F | M implies Q is open ) assume Q in F | M ; ::_thesis: Q is open then consider R being Subset of T such that A2: R in F and A3: R /\ M = Q by Def3; reconsider R = R as Subset of T ; A4: Q = R /\ ([#] (T | M)) by A3, PRE_TOPC:def_5; R is open by A1, A2, Def1; hence Q is open by A4, Th24; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for M being Subset of T for F being Subset-Family of T st F is closed holds F | M is closed let M be Subset of T; ::_thesis: for F being Subset-Family of T st F is closed holds F | M is closed let F be Subset-Family of T; ::_thesis: ( F is closed implies F | M is closed ) assume A1: F is closed ; ::_thesis: F | M is closed let Q be Subset of (T | M); :: according to TOPS_2:def_2 ::_thesis: ( Q in F | M implies Q is closed ) assume Q in F | M ; ::_thesis: Q is closed then consider R being Subset of T such that A2: R in F and A3: R /\ M = Q by Def3; reconsider R = R as Subset of T ; A4: Q = R /\ ([#] (T | M)) by A3, PRE_TOPC:def_5; R is closed by A1, A2, Def2; hence Q is closed by A4, PRE_TOPC:13; ::_thesis: verum end; 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 ) ) proof let T be TopStruct ; ::_thesis: 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 ) ) let A be SubSpace of T; ::_thesis: 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 ) ) let F be Subset-Family of A; ::_thesis: ( F is open implies ex G being Subset-Family of T st ( G is open & ( for AA being Subset of T st AA = [#] A holds F = G | AA ) ) ) assume A1: F is open ; ::_thesis: ex G being Subset-Family of T st ( G is open & ( for AA being Subset of T st AA = [#] A holds F = G | AA ) ) [#] A c= [#] T by PRE_TOPC:def_4; then reconsider At = [#] A as Subset of T ; defpred S1[ Subset of T] means ex X1 being Subset of T st ( X1 = \$1 & X1 is open & \$1 /\ At in F ); consider G being Subset-Family of T such that A2: for X being Subset of T holds ( X in G iff S1[X] ) from SUBSET_1:sch_3(); take G ; ::_thesis: ( G is open & ( for AA being Subset of T st AA = [#] A holds F = G | AA ) ) thus G is open ::_thesis: for AA being Subset of T st AA = [#] A holds F = G | AA proof let H be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( H in G implies H is open ) assume H in G ; ::_thesis: H is open then ex X1 being Subset of T st ( X1 = H & X1 is open & H /\ At in F ) by A2; hence H is open ; ::_thesis: verum end; let AA be Subset of T; ::_thesis: ( AA = [#] A implies F = G | AA ) assume A3: AA = [#] A ; ::_thesis: F = G | AA then F c= bool AA ; then F c= bool ([#] (T | AA)) by PRE_TOPC:def_5; then reconsider FF = F as Subset-Family of (T | AA) ; for X being Subset of (T | AA) holds ( X in FF iff ex X9 being Subset of T st ( X9 in G & X9 /\ AA = X ) ) proof let X be Subset of (T | AA); ::_thesis: ( X in FF iff ex X9 being Subset of T st ( X9 in G & X9 /\ AA = X ) ) thus ( X in FF implies ex X9 being Subset of T st ( X9 in G & X9 /\ AA = X ) ) ::_thesis: ( ex X9 being Subset of T st ( X9 in G & X9 /\ AA = X ) implies X in FF ) proof assume A4: X in FF ; ::_thesis: ex X9 being Subset of T st ( X9 in G & X9 /\ AA = X ) then reconsider XX = X as Subset of A ; XX is open by A1, A4, Def1; then consider Y being Subset of T such that A5: ( Y is open & Y /\ ([#] A) = XX ) by Th24; take Y ; ::_thesis: ( Y in G & Y /\ AA = X ) thus ( Y in G & Y /\ AA = X ) by A2, A3, A4, A5; ::_thesis: verum end; given X9 being Subset of T such that A6: X9 in G and A7: X9 /\ AA = X ; ::_thesis: X in FF ex X1 being Subset of T st ( X1 = X9 & X1 is open & X9 /\ At in F ) by A2, A6; hence X in FF by A3, A7; ::_thesis: verum end; hence F = G | AA by Def3; ::_thesis: verum end; 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 ) ) proof let T be TopStruct ; ::_thesis: 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 ) ) let P be Subset of T; ::_thesis: 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 ) ) let F be Subset-Family of T; ::_thesis: 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 ) ) defpred S1[ set , set ] means for Q being Subset of T st Q = \$1 holds \$2 = Q /\ P; A1: for x being set st x in F holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in F implies ex y being set st S1[x,y] ) assume x in F ; ::_thesis: ex y being set st S1[x,y] then reconsider Q = x as Subset of T ; reconsider y = Q /\ P as set ; take y ; ::_thesis: S1[x,y] thus S1[x,y] ; ::_thesis: verum end; consider f being Function such that A2: dom f = F and A3: for x being set st x in F holds S1[x,f . x] from CLASSES1:sch_1(A1); take f ; ::_thesis: ( 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 ) ) thus dom f = F by A2; ::_thesis: ( 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 ) ) for x being set holds ( x in rng f iff x in F | P ) proof let x be set ; ::_thesis: ( x in rng f iff x in F | P ) hereby ::_thesis: ( x in F | P implies x in rng f ) assume x in rng f ; ::_thesis: x in F | P then consider y being set such that A4: y in dom f and A5: f . y = x by FUNCT_1:def_3; reconsider Y = y as Subset of T by A2, A4; Y /\ P c= P by XBOOLE_1:17; then Y /\ P c= [#] (T | P) by PRE_TOPC:def_5; then reconsider X = x as Subset of (T | P) by A2, A3, A4, A5; X = Y /\ P by A2, A3, A4, A5; hence x in F | P by A2, A4, Def3; ::_thesis: verum end; assume A6: x in F | P ; ::_thesis: x in rng f then reconsider X = x as Subset of (T | P) ; consider Q being Subset of T such that A7: Q in F and A8: Q /\ P = X by A6, Def3; reconsider p = Q as set ; f . p = x by A3, A7, A8; hence x in rng f by A2, A7, FUNCT_1:def_3; ::_thesis: verum end; hence rng f = F | P by TARSKI:1; ::_thesis: for x being set st x in F holds for Q being Subset of T st Q = x holds f . x = Q /\ P thus for x being set st x in F holds for Q being Subset of T st Q = x holds f . x = Q /\ P by A3; ::_thesis: verum end; 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 proof let X, Y be 1-sorted ; ::_thesis: for f being Function of X,Y st ( [#] Y = {} implies [#] X = {} ) holds f " ([#] Y) = [#] X let f be Function of X,Y; ::_thesis: ( ( [#] Y = {} implies [#] X = {} ) implies f " ([#] Y) = [#] X ) assume A1: ( [#] Y = {} implies [#] X = {} ) ; ::_thesis: f " ([#] Y) = [#] X f " (rng f) = dom f by RELAT_1:134 .= [#] X by A1, FUNCT_2:def_1 ; then [#] X c= f " ([#] Y) by RELAT_1:143; hence f " ([#] Y) = [#] X by XBOOLE_0:def_10; ::_thesis: verum end; 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 proof let T be 1-sorted ; ::_thesis: 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 let S be non empty 1-sorted ; ::_thesis: for f being Function of T,S for H being Subset-Family of S holds (" f) .: H is Subset-Family of T let f be Function of T,S; ::_thesis: for H being Subset-Family of S holds (" f) .: H is Subset-Family of T let H be Subset-Family of S; ::_thesis: (" f) .: H is Subset-Family of T ( (" f) .: H c= rng (" f) & rng (" f) c= bool (dom f) ) by FUNCT_3:22, RELAT_1:111; then (" f) .: H c= bool (dom f) by XBOOLE_1:1; hence (" f) .: H is Subset-Family of T by FUNCT_2:def_1; ::_thesis: verum end; 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 ) proof let X, Y be TopStruct ; ::_thesis: 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 ) let f be Function of X,Y; ::_thesis: ( ( [#] Y = {} implies [#] X = {} ) implies ( f is continuous iff for P being Subset of Y st P is open holds f " P is open ) ) assume A1: ( [#] Y = {} implies [#] X = {} ) ; ::_thesis: ( f is continuous iff for P being Subset of Y st P is open holds f " P is open ) hereby ::_thesis: ( ( for P being Subset of Y st P is open holds f " P is open ) implies f is continuous ) assume A2: f is continuous ; ::_thesis: for P1 being Subset of Y st P1 is open holds f " P1 is open let P1 be Subset of Y; ::_thesis: ( P1 is open implies f " P1 is open ) assume P1 is open ; ::_thesis: f " P1 is open then P1 ` is closed by TOPS_1:4; then A3: f " (P1 `) is closed by A2, PRE_TOPC:def_6; f " (P1 `) = (f " ([#] Y)) \ (f " P1) by FUNCT_1:69 .= ([#] X) \ (f " P1) by A1, Th41 .= (f " P1) ` ; hence f " P1 is open by A3, TOPS_1:4; ::_thesis: verum end; assume A4: for P1 being Subset of Y st P1 is open holds f " P1 is open ; ::_thesis: f is continuous let P1 be Subset of Y; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f " P1 is closed ) assume P1 is closed ; ::_thesis: f " P1 is closed then P1 ` is open by TOPS_1:3; then A5: f " (P1 `) is open by A4; f " (P1 `) = (f " ([#] Y)) \ (f " P1) by FUNCT_1:69 .= ([#] X) \ (f " P1) by A1, Th41 .= (f " P1) ` ; hence f " P1 is closed by A5, TOPS_1:3; ::_thesis: verum end; 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) ) proof let T, S be TopSpace; ::_thesis: 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) ) let f be Function of T,S; ::_thesis: ( f is continuous iff for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) ) hereby ::_thesis: ( ( for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) ) implies f is continuous ) assume A1: f is continuous ; ::_thesis: for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) let P1 be Subset of S; ::_thesis: Cl (f " P1) c= f " (Cl P1) Cl (Cl P1) = Cl P1 ; then Cl P1 is closed by PRE_TOPC:22; then A2: f " (Cl P1) is closed by A1, PRE_TOPC:def_6; f " P1 c= f " (Cl P1) by PRE_TOPC:18, RELAT_1:143; then Cl (f " P1) c= Cl (f " (Cl P1)) by PRE_TOPC:19; hence Cl (f " P1) c= f " (Cl P1) by A2, PRE_TOPC:22; ::_thesis: verum end; assume A3: for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) ; ::_thesis: f is continuous let P1 be Subset of S; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f " P1 is closed ) assume P1 is closed ; ::_thesis: f " P1 is closed then Cl P1 = P1 by PRE_TOPC:22; then ( f " P1 c= Cl (f " P1) & Cl (f " P1) c= f " P1 ) by A3, PRE_TOPC:18; then f " P1 = Cl (f " P1) by XBOOLE_0:def_10; hence f " P1 is closed by PRE_TOPC:22; ::_thesis: verum end; 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) ) proof let T be TopSpace; ::_thesis: 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) ) let S be non empty TopSpace; ::_thesis: 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) ) let f be Function of T,S; ::_thesis: ( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) ) hereby ::_thesis: ( ( for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) ) implies f is continuous ) assume A1: f is continuous ; ::_thesis: for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) let P be Subset of T; ::_thesis: f .: (Cl P) c= Cl (f .: P) P c= [#] T ; then P c= dom f by FUNCT_2:def_1; then A2: Cl P c= Cl (f " (f .: P)) by FUNCT_1:76, PRE_TOPC:19; Cl (f " (f .: P)) c= f " (Cl (f .: P)) by A1, Th44; then Cl P c= f " (Cl (f .: P)) by A2, XBOOLE_1:1; then A3: f .: (Cl P) c= f .: (f " (Cl (f .: P))) by RELAT_1:123; f .: (f " (Cl (f .: P))) c= Cl (f .: P) by FUNCT_1:75; hence f .: (Cl P) c= Cl (f .: P) by A3, XBOOLE_1:1; ::_thesis: verum end; assume A4: for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) ; ::_thesis: f is continuous now__::_thesis:_for_P1_being_Subset_of_S_holds_Cl_(f_"_P1)_c=_f_"_(Cl_P1) let P1 be Subset of S; ::_thesis: Cl (f " P1) c= f " (Cl P1) Cl (f " P1) c= [#] T ; then Cl (f " P1) c= dom f by FUNCT_2:def_1; then A5: Cl (f " P1) c= f " (f .: (Cl (f " P1))) by FUNCT_1:76; ( f .: (Cl (f " P1)) c= Cl (f .: (f " P1)) & Cl (f .: (f " P1)) c= Cl P1 ) by A4, FUNCT_1:75, PRE_TOPC:19; then f .: (Cl (f " P1)) c= Cl P1 by XBOOLE_1:1; then f " (f .: (Cl (f " P1))) c= f " (Cl P1) by RELAT_1:143; hence Cl (f " P1) c= f " (Cl P1) by A5, XBOOLE_1:1; ::_thesis: verum end; hence f is continuous by Th44; ::_thesis: verum end; 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 proof let T, V be TopStruct ; ::_thesis: 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 let S be non empty TopStruct ; ::_thesis: 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 let f be Function of T,S; ::_thesis: for g being Function of S,V st f is continuous & g is continuous holds g * f is continuous let g be Function of S,V; ::_thesis: ( f is continuous & g is continuous implies g * f is continuous ) assume that A1: f is continuous and A2: g is continuous ; ::_thesis: g * f is continuous let P be Subset of V; :: according to PRE_TOPC:def_6 ::_thesis: ( not P is closed or (g * f) " P is closed ) assume P is closed ; ::_thesis: (g * f) " P is closed then ( (g * f) " P = f " (g " P) & g " P is closed ) by A2, PRE_TOPC:def_6, RELAT_1:146; hence (g * f) " P is closed by A1, PRE_TOPC:def_6; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: 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 let S be non empty TopStruct ; ::_thesis: 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 let f be Function of T,S; ::_thesis: 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 let H be Subset-Family of S; ::_thesis: ( f is continuous & H is open implies for F being Subset-Family of T st F = (" f) .: H holds F is open ) assume that A1: f is continuous and A2: H is open ; ::_thesis: for F being Subset-Family of T st F = (" f) .: H holds F is open let F be Subset-Family of T; ::_thesis: ( F = (" f) .: H implies F is open ) assume A3: F = (" f) .: H ; ::_thesis: F is open let X be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( X in F implies X is open ) assume X in F ; ::_thesis: X is open then consider y being set such that A4: y in dom (" f) and A5: y in H and A6: X = (" f) . y by A3, FUNCT_1:def_6; reconsider Y = y as Subset of S by A5; A7: X = f " Y by A4, A6, FUNCT_3:21; A8: ( [#] S = {} implies [#] T = {} ) ; Y is open by A2, A5, Def1; hence X is open by A1, A8, A7, Th43; ::_thesis: verum end; 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 proof let T, S be TopStruct ; ::_thesis: 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 let f be Function of T,S; ::_thesis: 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 let H be Subset-Family of S; ::_thesis: ( f is continuous & H is closed implies for F being Subset-Family of T st F = (" f) .: H holds F is closed ) assume that A1: f is continuous and A2: H is closed ; ::_thesis: for F being Subset-Family of T st F = (" f) .: H holds F is closed let F be Subset-Family of T; ::_thesis: ( F = (" f) .: H implies F is closed ) assume A3: F = (" f) .: H ; ::_thesis: F is closed let X be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( X in F implies X is closed ) assume X in F ; ::_thesis: X is closed then consider y being set such that A4: y in dom (" f) and A5: y in H and A6: X = (" f) . y by A3, FUNCT_1:def_6; reconsider Y = y as Subset of S by A5; A7: X = f " Y by A4, A6, FUNCT_3:21; Y is closed by A2, A5, Def2; hence X is closed by A1, A7, PRE_TOPC:def_6; ::_thesis: verum end; 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 proof rng f = [#] T by A1, FUNCT_2:def_3; hence f " is Function of T,S by A1, FUNCT_2:25; ::_thesis: verum end; 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 ) proof let T be 1-sorted ; ::_thesis: 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 ) let S be non empty 1-sorted ; ::_thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds ( dom (f ") = [#] S & rng (f ") = [#] T ) let f be Function of T,S; ::_thesis: ( rng f = [#] S & f is one-to-one implies ( dom (f ") = [#] S & rng (f ") = [#] T ) ) assume that A1: rng f = [#] S and A2: f is one-to-one ; ::_thesis: ( dom (f ") = [#] S & rng (f ") = [#] T ) A3: f is onto by A1, FUNCT_2:def_3; hence dom (f ") = dom (f ") by A2, Def4 .= [#] S by A1, A2, FUNCT_1:32 ; ::_thesis: rng (f ") = [#] T thus rng (f ") = rng (f ") by A2, A3, Def4 .= dom f by A2, FUNCT_1:33 .= [#] T by FUNCT_2:def_1 ; ::_thesis: verum end; 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 proof let T, S be 1-sorted ; ::_thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds f " is one-to-one let f be Function of T,S; ::_thesis: ( rng f = [#] S & f is one-to-one implies f " is one-to-one ) assume that A1: rng f = [#] S and A2: f is one-to-one ; ::_thesis: f " is one-to-one A3: f is onto by A1, FUNCT_2:def_3; f " is one-to-one by A2; hence f " is one-to-one by A2, A3, Def4; ::_thesis: verum end; 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 proof let T be 1-sorted ; ::_thesis: 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 let S be non empty 1-sorted ; ::_thesis: for f being Function of T,S st rng f = [#] S & f is one-to-one holds (f ") " = f let f be Function of T,S; ::_thesis: ( rng f = [#] S & f is one-to-one implies (f ") " = f ) assume that A1: rng f = [#] S and A2: f is one-to-one ; ::_thesis: (f ") " = f A3: f is onto by A1, FUNCT_2:def_3; f = (f ") " by A2, FUNCT_1:43; then A4: f = (f ") " by A3, A2, Def4; A5: f " is one-to-one by A1, A2, Th50; rng (f ") = [#] T by A1, A2, Th49; then f " is onto by FUNCT_2:def_3; hence (f ") " = f by A4, A5, Def4; ::_thesis: verum end; 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) ) proof let T, S be 1-sorted ; ::_thesis: 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) ) let f be Function of T,S; ::_thesis: ( rng f = [#] S & f is one-to-one implies ( (f ") * f = id (dom f) & f * (f ") = id (rng f) ) ) assume that A1: rng f = [#] S and A2: f is one-to-one ; ::_thesis: ( (f ") * f = id (dom f) & f * (f ") = id (rng f) ) A3: f is onto by A1, FUNCT_2:def_3; ( (f ") * f = id (dom f) & f * (f ") = id (rng f) ) by A2, FUNCT_1:39; hence ( (f ") * f = id (dom f) & f * (f ") = id (rng f) ) by A2, A3, Def4; ::_thesis: verum end; 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 ") proof let T be 1-sorted ; ::_thesis: 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 ") let S, V be non empty 1-sorted ; ::_thesis: 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 ") let f be Function of T,S; ::_thesis: 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 ") let g be Function of S,V; ::_thesis: ( rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one implies (g * f) " = (f ") * (g ") ) assume that A1: rng f = [#] S and A2: f is one-to-one ; ::_thesis: ( not dom g = [#] S or not rng g = [#] V or not g is one-to-one or (g * f) " = (f ") * (g ") ) assume that A3: dom g = [#] S and A4: rng g = [#] V and A5: g is one-to-one ; ::_thesis: (g * f) " = (f ") * (g ") A6: ( f is onto & g is onto ) by A1, A4, FUNCT_2:def_3; rng (g * f) = [#] V by A1, A3, A4, RELAT_1:28; then g * f is onto by FUNCT_2:def_3; then A7: (g * f) " = (g * f) " by A2, A5, Def4; A8: f " = f " by A2, A6, Def4; g " = g " by A5, A6, Def4; hence (g * f) " = (f ") * (g ") by A2, A5, A8, A7, FUNCT_1:44; ::_thesis: verum end; 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 proof let T, S be 1-sorted ; ::_thesis: 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 let f be Function of T,S; ::_thesis: for P being Subset of T st rng f = [#] S & f is one-to-one holds f .: P = (f ") " P let P be Subset of T; ::_thesis: ( rng f = [#] S & f is one-to-one implies f .: P = (f ") " P ) assume that A1: rng f = [#] S and A2: f is one-to-one ; ::_thesis: f .: P = (f ") " P A3: f is onto by A1, FUNCT_2:def_3; f .: P = (f ") " P by A2, FUNCT_1:84; hence f .: P = (f ") " P by A2, A3, Def4; ::_thesis: verum end; 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 proof let T, S be 1-sorted ; ::_thesis: 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 let f be Function of T,S; ::_thesis: for P1 being Subset of S st rng f = [#] S & f is one-to-one holds f " P1 = (f ") .: P1 let P1 be Subset of S; ::_thesis: ( rng f = [#] S & f is one-to-one implies f " P1 = (f ") .: P1 ) assume rng f = [#] S ; ::_thesis: ( not f is one-to-one or f " P1 = (f ") .: P1 ) then A1: f is onto by FUNCT_2:def_3; assume A2: f is one-to-one ; ::_thesis: f " P1 = (f ") .: P1 f " P1 = (f ") .: P1 by A2, FUNCT_1:85; hence f " P1 = (f ") .: P1 by A1, A2, Def4; ::_thesis: verum end; 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 proof let T be TopStruct ; ::_thesis: for S being non empty TopStruct for f being Function of T,S st f is being_homeomorphism holds f " is being_homeomorphism let S be non empty TopStruct ; ::_thesis: for f being Function of T,S st f is being_homeomorphism holds f " is being_homeomorphism let f be Function of T,S; ::_thesis: ( f is being_homeomorphism implies f " is being_homeomorphism ) assume A1: f is being_homeomorphism ; ::_thesis: f " is being_homeomorphism then A2: ( rng f = [#] S & f is one-to-one ) by Def5; hence ( dom (f ") = [#] S & rng (f ") = [#] T ) by Th49; :: according to TOPS_2:def_5 ::_thesis: ( f " is one-to-one & f " is continuous & (f ") " is continuous ) thus f " is one-to-one by A2, Th50; ::_thesis: ( f " is continuous & (f ") " is continuous ) thus f " is continuous by A1, Def5; ::_thesis: (f ") " is continuous f is continuous by A1, Def5; hence (f ") " is continuous by A2, Th51; ::_thesis: verum end; 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 proof let T, S, V be non empty TopStruct ; ::_thesis: 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 let f be Function of T,S; ::_thesis: for g being Function of S,V st f is being_homeomorphism & g is being_homeomorphism holds g * f is being_homeomorphism let g be Function of S,V; ::_thesis: ( f is being_homeomorphism & g is being_homeomorphism implies g * f is being_homeomorphism ) assume that A1: f is being_homeomorphism and A2: g is being_homeomorphism ; ::_thesis: g * f is being_homeomorphism A3: ( rng f = [#] S & dom g = [#] S ) by A1, A2, Def5; A4: rng g = [#] V by A2, Def5; dom f = [#] T by A1, Def5; hence ( dom (g * f) = [#] T & rng (g * f) = [#] V ) by A3, A4, RELAT_1:27, RELAT_1:28; :: according to TOPS_2:def_5 ::_thesis: ( g * f is one-to-one & g * f is continuous & (g * f) " is continuous ) A5: ( f is one-to-one & g is one-to-one ) by A1, A2, Def5; hence g * f is one-to-one ; ::_thesis: ( g * f is continuous & (g * f) " is continuous ) ( f is continuous & g is continuous ) by A1, A2, Def5; hence g * f is continuous by Th46; ::_thesis: (g * f) " is continuous ( f " is continuous & g " is continuous ) by A1, A2, Def5; then (f ") * (g ") is continuous by Th46; hence (g * f) " is continuous by A3, A4, A5, Th53; ::_thesis: verum end; 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 ) ) ) ) proof let T be TopStruct ; ::_thesis: 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 ) ) ) ) let S be non empty TopStruct ; ::_thesis: 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 ) ) ) ) let f be Function of T,S; ::_thesis: ( 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 ) ) ) ) hereby ::_thesis: ( 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 ) ) implies f is being_homeomorphism ) assume A1: f is being_homeomorphism ; ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds ( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) ) ) ) hence A2: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by Def5; ::_thesis: for P being Subset of T holds ( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) ) let P be Subset of T; ::_thesis: ( ( P is closed implies f .: P is closed ) & ( f .: P is closed implies P is closed ) ) A3: f " is continuous by A1, Def5; hereby ::_thesis: ( f .: P is closed implies P is closed ) assume A4: P is closed ; ::_thesis: f .: P is closed f is onto by A2, FUNCT_2:def_3; then (f ") " P = (f ") " P by A2, Def4 .= f .: P by A2, FUNCT_1:84 ; hence f .: P is closed by A3, A4, PRE_TOPC:def_6; ::_thesis: verum end; assume A5: f .: P is closed ; ::_thesis: P is closed f is continuous by A1, Def5; then A6: f " (f .: P) is closed by A5, PRE_TOPC:def_6; dom f = [#] T by FUNCT_2:def_1; then A7: P c= f " (f .: P) by FUNCT_1:76; f " (f .: P) c= P by A2, FUNCT_1:82; hence P is closed by A6, A7, XBOOLE_0:def_10; ::_thesis: verum end; assume that A8: dom f = [#] T and A9: rng f = [#] S and A10: f is one-to-one ; ::_thesis: ( ex P being Subset of T st ( ( P is closed implies f .: P is closed ) implies ( f .: P is closed & not P is closed ) ) or f is being_homeomorphism ) assume A11: for P being Subset of T holds ( P is closed iff f .: P is closed ) ; ::_thesis: f is being_homeomorphism A12: f is continuous proof let B be Subset of S; :: according to PRE_TOPC:def_6 ::_thesis: ( not B is closed or f " B is closed ) assume A13: B is closed ; ::_thesis: f " B is closed set D = f " B; B = f .: (f " B) by A9, FUNCT_1:77; hence f " B is closed by A11, A13; ::_thesis: verum end; f " is continuous proof let B be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not B is closed or (f ") " B is closed ) assume A14: B is closed ; ::_thesis: (f ") " B is closed f is onto by A9, FUNCT_2:def_3; then (f ") " B = (f ") " B by A10, Def4 .= f .: B by A10, FUNCT_1:84 ; hence (f ") " B is closed by A11, A14; ::_thesis: verum end; hence f is being_homeomorphism by A8, A9, A10, A12, Def5; ::_thesis: verum end; 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) ) ) ) proof let T be non empty TopSpace; ::_thesis: 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) ) ) ) let S be TopSpace; ::_thesis: 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) ) ) ) let f be Function of T,S; ::_thesis: ( 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) ) ) ) hereby ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) implies f is being_homeomorphism ) assume A1: f is being_homeomorphism ; ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) hence A2: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by Def5; ::_thesis: for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) let P1 be Subset of S; ::_thesis: f " (Cl P1) = Cl (f " P1) f is continuous by A1, Def5; then A3: Cl (f " P1) c= f " (Cl P1) by Th44; f " is continuous by A1, Def5; then A4: (f ") .: (Cl P1) c= Cl ((f ") .: P1) by Th45; ( f " (Cl P1) = (f ") .: (Cl P1) & f " P1 = (f ") .: P1 ) by A2, Th55; hence f " (Cl P1) = Cl (f " P1) by A3, A4, XBOOLE_0:def_10; ::_thesis: verum end; assume that A5: dom f = [#] T and A6: ( rng f = [#] S & f is one-to-one ) ; ::_thesis: ( ex P1 being Subset of S st not f " (Cl P1) = Cl (f " P1) or f is being_homeomorphism ) assume A7: for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ; ::_thesis: f is being_homeomorphism thus ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by A5, A6; :: according to TOPS_2:def_5 ::_thesis: ( f is continuous & f " is continuous ) for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) by A7; hence f is continuous by Th44; ::_thesis: f " is continuous now__::_thesis:_for_P1_being_Subset_of_S_holds_(f_")_.:_(Cl_P1)_c=_Cl_((f_")_.:_P1) let P1 be Subset of S; ::_thesis: (f ") .: (Cl P1) c= Cl ((f ") .: P1) ( (f ") .: (Cl P1) = f " (Cl P1) & (f ") .: P1 = f " P1 ) by A6, Th55; hence (f ") .: (Cl P1) c= Cl ((f ") .: P1) by A7; ::_thesis: verum end; hence f " is continuous by Th45; ::_thesis: verum end; 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) ) ) ) proof let T be TopSpace; ::_thesis: 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) ) ) ) let S be non empty TopSpace; ::_thesis: 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) ) ) ) let f be Function of T,S; ::_thesis: ( 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) ) ) ) hereby ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) implies f is being_homeomorphism ) assume A1: f is being_homeomorphism ; ::_thesis: ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) hence A2: ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by Def5; ::_thesis: for P being Subset of T holds f .: (Cl P) = Cl (f .: P) let P be Subset of T; ::_thesis: f .: (Cl P) = Cl (f .: P) f is continuous by A1, Def5; then A3: f .: (Cl P) c= Cl (f .: P) by Th45; f " is continuous by A1, Def5; then A4: Cl ((f ") " P) c= (f ") " (Cl P) by Th44; ( (f ") " P = f .: P & (f ") " (Cl P) = f .: (Cl P) ) by A2, Th54; hence f .: (Cl P) = Cl (f .: P) by A3, A4, XBOOLE_0:def_10; ::_thesis: verum end; assume that A5: dom f = [#] T and A6: ( rng f = [#] S & f is one-to-one ) ; ::_thesis: ( ex P being Subset of T st not f .: (Cl P) = Cl (f .: P) or f is being_homeomorphism ) assume A7: for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ; ::_thesis: f is being_homeomorphism thus ( dom f = [#] T & rng f = [#] S & f is one-to-one ) by A5, A6; :: according to TOPS_2:def_5 ::_thesis: ( f is continuous & f " is continuous ) for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) by A7; hence f is continuous by Th45; ::_thesis: f " is continuous now__::_thesis:_for_P_being_Subset_of_T_holds_Cl_((f_")_"_P)_c=_(f_")_"_(Cl_P) let P be Subset of T; ::_thesis: Cl ((f ") " P) c= (f ") " (Cl P) ( (f ") " P = f .: P & (f ") " (Cl P) = f .: (Cl P) ) by A6, Th54; hence Cl ((f ") " P) c= (f ") " (Cl P) by A7; ::_thesis: verum end; hence f " is continuous by Th44; ::_thesis: verum end; 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 proof let X, Y be non empty TopSpace; ::_thesis: 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 let f be Function of X,Y; ::_thesis: for A being Subset of X st f is continuous & A is connected holds f .: A is connected let A be Subset of X; ::_thesis: ( f is continuous & A is connected implies f .: A is connected ) assume A1: f is continuous ; ::_thesis: ( not A is connected or f .: A is connected ) assume A2: A is connected ; ::_thesis: f .: A is connected assume not f .: A is connected ; ::_thesis: contradiction then consider P, Q being Subset of Y such that A3: f .: A = P \/ Q and A4: P,Q are_separated and A5: P <> {} Y and A6: Q <> {} Y by CONNSP_1:15; reconsider P1 = f " P, Q1 = f " Q as Subset of X ; set P2 = P1 /\ A; set Q2 = Q1 /\ A; set y = the Element of P; the Element of P in f .: A by A3, A5, XBOOLE_0:def_3; then consider x being set such that A7: x in dom f and A8: x in A and A9: the Element of P = f . x by FUNCT_1:def_6; x in f " P by A5, A7, A9, FUNCT_1:def_7; then A10: P1 /\ A <> {} by A8, XBOOLE_0:def_4; A11: the carrier of X = dom f by FUNCT_2:def_1; P misses Cl Q by A4, CONNSP_1:def_1; then A12: ( (f " P) /\ (f " (Cl Q)) = f " (P /\ (Cl Q)) & f " (P /\ (Cl Q)) = f " ({} Y) ) by FUNCT_1:68, XBOOLE_0:def_7; Cl Q1 c= f " (Cl Q) by A1, Th44; then P1 /\ (Cl Q1) = {} by A12, XBOOLE_1:3, XBOOLE_1:26; then A13: P1 misses Cl Q1 by XBOOLE_0:def_7; Cl P misses Q by A4, CONNSP_1:def_1; then A14: ( (f " (Cl P)) /\ (f " Q) = f " ((Cl P) /\ Q) & f " ((Cl P) /\ Q) = f " ({} Y) ) by FUNCT_1:68, XBOOLE_0:def_7; Cl P1 c= f " (Cl P) by A1, Th44; then (Cl P1) /\ Q1 = {} X by A14, XBOOLE_1:3, XBOOLE_1:26; then Cl P1 misses Q1 by XBOOLE_0:def_7; then A15: P1,Q1 are_separated by A13, CONNSP_1:def_1; set z = the Element of Q; the Element of Q in P \/ Q by A6, XBOOLE_0:def_3; then consider x1 being set such that A16: x1 in dom f and A17: x1 in A and A18: the Element of Q = f . x1 by A3, FUNCT_1:def_6; x1 in f " Q by A6, A16, A18, FUNCT_1:def_7; then A19: Q1 /\ A <> {} by A17, XBOOLE_0:def_4; f " (f .: A) = (f " P) \/ (f " Q) by A3, RELAT_1:140; then A20: A = (P1 \/ Q1) /\ A by A11, FUNCT_1:76, XBOOLE_1:28 .= (P1 /\ A) \/ (Q1 /\ A) by XBOOLE_1:23 ; ( P1 /\ A c= P1 & Q1 /\ A c= Q1 ) by XBOOLE_1:17; then ex P3, Q3 being Subset of X st ( A = P3 \/ Q3 & P3,Q3 are_separated & P3 <> {} X & Q3 <> {} X ) by A15, A20, A10, A19, CONNSP_1:7; hence contradiction by A2, CONNSP_1:15; ::_thesis: verum end; 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 proof let S, T be non empty TopSpace; ::_thesis: 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 let f be Function of S,T; ::_thesis: for A being Subset of T st f is being_homeomorphism & A is connected holds f " A is connected let A be Subset of T; ::_thesis: ( f is being_homeomorphism & A is connected implies f " A is connected ) assume that A1: f is being_homeomorphism and A2: A is connected ; ::_thesis: f " A is connected f " is continuous by A1, Def5; then A3: (f ") .: A is connected by A2, Th61; ( rng f = [#] T & f is one-to-one ) by A1, Def5; hence f " A is connected by A3, Th55; ::_thesis: verum end; 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 proof let GX be non empty TopSpace; ::_thesis: ( ( 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 ) ) ) implies GX is connected ) assume A1: 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 ) ) ; ::_thesis: GX is connected for A, B being Subset of GX st [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open holds A meets B proof let A, B be Subset of GX; ::_thesis: ( [#] GX = A \/ B & A <> {} GX & B <> {} GX & A is open & B is open implies A meets B ) assume that A2: [#] GX = A \/ B and A3: A <> {} GX and A4: B <> {} GX and A5: ( A is open & B is open ) ; ::_thesis: A meets B set v = the Element of B; set u = the Element of A; reconsider y = the Element of B as Point of GX by A2, A4, XBOOLE_0:def_3; reconsider x = the Element of A as Point of GX by A2, A3, XBOOLE_0:def_3; consider GY being non empty TopSpace such that A6: GY is connected and A7: ex f being Function of GY,GX st ( f is continuous & x in rng f & y in rng f ) by A1; consider f being Function of GY,GX such that A8: f is continuous and A9: x in rng f and A10: y in rng f by A7; f " ([#] GX) = [#] GY by Th41; then A11: (f " A) \/ (f " B) = [#] GY by A2, RELAT_1:140; (rng f) /\ B <> {} by A4, A10, XBOOLE_0:def_4; then rng f meets B by XBOOLE_0:def_7; then A12: f " B <> {} GY by RELAT_1:138; (rng f) /\ A <> {} by A3, A9, XBOOLE_0:def_4; then rng f meets A by XBOOLE_0:def_7; then A13: f " A <> {} GY by RELAT_1:138; [#] GX <> {} ; then ( f " A is open & f " B is open ) by A5, A8, Th43; then f " A meets f " B by A6, A11, A13, A12, CONNSP_1:11; then (f " A) /\ (f " B) <> {} by XBOOLE_0:def_7; then f " (A /\ B) <> {} by FUNCT_1:68; then rng f meets A /\ B by RELAT_1:138; then ex u1 being set st ( u1 in rng f & u1 in A /\ B ) by XBOOLE_0:3; hence A meets B by XBOOLE_0:4; ::_thesis: verum end; hence GX is connected by CONNSP_1:11; ::_thesis: verum end; 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 ) proof let X be TopStruct ; ::_thesis: for F being Subset-Family of X holds ( F is open iff F c= the topology of X ) let F be Subset-Family of X; ::_thesis: ( F is open iff F c= the topology of X ) thus ( F is open implies F c= the topology of X ) ::_thesis: ( F c= the topology of X implies F is open ) proof assume A1: F is open ; ::_thesis: F c= the topology of X let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in F or A in the topology of X ) assume A2: A in F ; ::_thesis: A in the topology of X then reconsider A = A as Subset of X ; A is open by A1, A2, Def1; hence A in the topology of X by PRE_TOPC:def_2; ::_thesis: verum end; assume A3: F c= the topology of X ; ::_thesis: F is open let A be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( A in F implies A is open ) thus ( A in F implies A is open ) by A3, PRE_TOPC:def_2; ::_thesis: verum end; 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 ) proof let X be TopStruct ; ::_thesis: for F being Subset-Family of X holds ( F is closed iff F c= COMPLEMENT the topology of X ) let F be Subset-Family of X; ::_thesis: ( F is closed iff F c= COMPLEMENT the topology of X ) thus ( F is closed implies F c= COMPLEMENT the topology of X ) ::_thesis: ( F c= COMPLEMENT the topology of X implies F is closed ) proof assume A1: F is closed ; ::_thesis: F c= COMPLEMENT the topology of X let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in F or A in COMPLEMENT the topology of X ) assume A2: A in F ; ::_thesis: A in COMPLEMENT the topology of X then reconsider A = A as Subset of X ; A is closed by A1, A2, Def2; then A ` is open by TOPS_1:3; then A ` in the topology of X by PRE_TOPC:def_2; hence A in COMPLEMENT the topology of X by SETFAM_1:def_7; ::_thesis: verum end; assume A3: F c= COMPLEMENT the topology of X ; ::_thesis: F is closed let A be Subset of X; :: according to TOPS_2:def_2 ::_thesis: ( A in F implies A is closed ) assume A in F ; ::_thesis: A is closed then A ` in the topology of X by A3, SETFAM_1:def_7; then A ` is open by PRE_TOPC:def_2; hence A is closed by TOPS_1:3; ::_thesis: verum end; 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 proof take the topology of X ; ::_thesis: the topology of X is open thus the topology of X is open ; ::_thesis: verum end; end;