:: COMPTS_1 semantic presentation begin definition let T be TopStruct ; attrT is compact means :Def1: :: COMPTS_1:def 1 for F being Subset-Family of T st F is Cover of T & F is open holds ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is finite ); end; :: deftheorem Def1 defines compact COMPTS_1:def_1_:_ for T being TopStruct holds ( T is compact iff for F being Subset-Family of T st F is Cover of T & F is open holds ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is finite ) ); definition let T be non empty TopSpace; redefine attr T is regular means :: COMPTS_1:def 2 for p being Point of T for P being Subset of T st P <> {} & P is closed & p in P ` holds ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ); compatibility ( T is regular iff for p being Point of T for P being Subset of T st P <> {} & P is closed & p in P ` holds ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ) ) proof thus ( T is regular implies for p being Point of T for P being Subset of T st P <> {} & P is closed & p in P ` holds ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ) ) by PRE_TOPC:def_11; ::_thesis: ( ( for p being Point of T for P being Subset of T st P <> {} & P is closed & p in P ` holds ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ) ) implies T is regular ) assume A1: for p being Point of T for P being Subset of T st P <> {} & P is closed & p in P ` holds ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ) ; ::_thesis: T is regular let p be Point of T; :: according to PRE_TOPC:def_11 ::_thesis: for b1 being Element of bool the carrier of T holds ( not b1 is closed or not p in b1 ` or ex b2, b3 being Element of bool the carrier of T st ( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) ) let P be Subset of T; ::_thesis: ( not P is closed or not p in P ` or ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) ) assume that A2: P is closed and A3: p in P ` ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) percases ( P = {} or P <> {} ) ; supposeA4: P = {} ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) take G1 = [#] T; ::_thesis: ex b1 being Element of bool the carrier of T st ( G1 is open & b1 is open & p in G1 & P c= b1 & G1 misses b1 ) take G2 = {} T; ::_thesis: ( G1 is open & G2 is open & p in G1 & P c= G2 & G1 misses G2 ) thus ( G1 is open & G2 is open ) ; ::_thesis: ( p in G1 & P c= G2 & G1 misses G2 ) thus p in G1 ; ::_thesis: ( P c= G2 & G1 misses G2 ) thus ( P c= G2 & G1 misses G2 ) by A4, XBOOLE_1:65; ::_thesis: verum end; suppose P <> {} ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) hence ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) by A1, A2, A3; ::_thesis: verum end; end; end; redefine attr T is normal means :: COMPTS_1:def 3 for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P, Q being Subset of T st ( P is open & Q is open & W c= P & V c= Q & P misses Q ); compatibility ( T is normal iff for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P, Q being Subset of T st ( P is open & Q is open & W c= P & V c= Q & P misses Q ) ) proof thus ( T is normal implies for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P, Q being Subset of T st ( P is open & Q is open & W c= P & V c= Q & P misses Q ) ) by PRE_TOPC:def_12; ::_thesis: ( ( for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P, Q being Subset of T st ( P is open & Q is open & W c= P & V c= Q & P misses Q ) ) implies T is normal ) assume A5: for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P, Q being Subset of T st ( P is open & Q is open & W c= P & V c= Q & P misses Q ) ; ::_thesis: T is normal let F1, F2 be Subset of T; :: according to PRE_TOPC:def_12 ::_thesis: ( not F1 is closed or not F2 is closed or not F1 misses F2 or ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) ) assume that A6: F1 is closed and A7: F2 is closed and A8: F1 misses F2 ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) percases ( F1 = {} or F2 = {} or ( F1 <> {} & F2 <> {} ) ) ; supposeA9: F1 = {} ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) take G1 = {} T; ::_thesis: ex b1 being Element of bool the carrier of T st ( G1 is open & b1 is open & F1 c= G1 & F2 c= b1 & G1 misses b1 ) take G2 = [#] T; ::_thesis: ( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 ) thus ( G1 is open & G2 is open ) ; ::_thesis: ( F1 c= G1 & F2 c= G2 & G1 misses G2 ) thus F1 c= G1 by A9; ::_thesis: ( F2 c= G2 & G1 misses G2 ) thus F2 c= G2 ; ::_thesis: G1 misses G2 thus G1 misses G2 by XBOOLE_1:65; ::_thesis: verum end; supposeA10: F2 = {} ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) take G1 = [#] T; ::_thesis: ex b1 being Element of bool the carrier of T st ( G1 is open & b1 is open & F1 c= G1 & F2 c= b1 & G1 misses b1 ) take G2 = {} T; ::_thesis: ( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 ) thus ( G1 is open & G2 is open ) ; ::_thesis: ( F1 c= G1 & F2 c= G2 & G1 misses G2 ) thus F1 c= G1 ; ::_thesis: ( F2 c= G2 & G1 misses G2 ) thus F2 c= G2 by A10; ::_thesis: G1 misses G2 thus G1 misses G2 by XBOOLE_1:65; ::_thesis: verum end; suppose ( F1 <> {} & F2 <> {} ) ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) hence ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) by A5, A6, A7, A8; ::_thesis: verum end; end; end; end; :: deftheorem defines regular COMPTS_1:def_2_:_ for T being non empty TopSpace holds ( T is regular iff for p being Point of T for P being Subset of T st P <> {} & P is closed & p in P ` holds ex W, V being Subset of T st ( W is open & V is open & p in W & P c= V & W misses V ) ); :: deftheorem defines normal COMPTS_1:def_3_:_ for T being non empty TopSpace holds ( T is normal iff for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds ex P, Q being Subset of T st ( P is open & Q is open & W c= P & V c= Q & P misses Q ) ); notation let T be TopStruct ; synonym Hausdorff T for T_2 ; end; definition let T be TopStruct ; let P be Subset of T; attrP is compact means :Def4: :: COMPTS_1:def 4 for F being Subset-Family of T st F is Cover of P & F is open holds ex G being Subset-Family of T st ( G c= F & G is Cover of P & G is finite ); end; :: deftheorem Def4 defines compact COMPTS_1:def_4_:_ for T being TopStruct for P being Subset of T holds ( P is compact iff for F being Subset-Family of T st F is Cover of P & F is open holds ex G being Subset-Family of T st ( G c= F & G is Cover of P & G is finite ) ); registration let T be TopStruct ; cluster empty -> compact for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is empty holds b1 is compact proof reconsider C = {} as Subset-Family of T by XBOOLE_1:2; let S be Subset of T; ::_thesis: ( S is empty implies S is compact ) assume S is empty ; ::_thesis: S is compact then A1: S c= union C by XBOOLE_1:2; let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of S & F is open implies ex G being Subset-Family of T st ( G c= F & G is Cover of S & G is finite ) ) assume that F is Cover of S and F is open ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of S & G is finite ) take C ; ::_thesis: ( C c= F & C is Cover of S & C is finite ) thus ( C c= F & C is Cover of S & C is finite ) by A1, SETFAM_1:def_11, XBOOLE_1:2; ::_thesis: verum end; end; theorem Th1: :: COMPTS_1:1 for T being TopStruct holds ( T is compact iff [#] T is compact ) proof let T be TopStruct ; ::_thesis: ( T is compact iff [#] T is compact ) thus ( T is compact implies [#] T is compact ) ::_thesis: ( [#] T is compact implies T is compact ) proof assume A1: T is compact ; ::_thesis: [#] T is compact let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of [#] T & F is open implies ex G being Subset-Family of T st ( G c= F & G is Cover of [#] T & G is finite ) ) assume that A2: F is Cover of [#] T and A3: F is open ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of [#] T & G is finite ) consider G being Subset-Family of T such that A4: G c= F and A5: G is Cover of T and A6: G is finite by A1, A2, A3, Def1; take G ; ::_thesis: ( G c= F & G is Cover of [#] T & G is finite ) thus ( G c= F & G is Cover of [#] T & G is finite ) by A4, A5, A6; ::_thesis: verum end; assume A7: [#] T is compact ; ::_thesis: T is compact let F be Subset-Family of T; :: according to COMPTS_1:def_1 ::_thesis: ( F is Cover of T & F is open implies ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is finite ) ) assume that A8: F is Cover of T and A9: F is open ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is finite ) consider G being Subset-Family of T such that A10: G c= F and A11: G is Cover of [#] T and A12: G is finite by A7, A8, A9, Def4; take G ; ::_thesis: ( G c= F & G is Cover of T & G is finite ) thus ( G c= F & G is Cover of T & G is finite ) by A10, A11, A12; ::_thesis: verum end; theorem Th2: :: COMPTS_1:2 for T being TopStruct for A being SubSpace of T for Q being Subset of T st Q c= [#] A holds ( Q is compact iff for P being Subset of A st P = Q holds P is compact ) proof let T be TopStruct ; ::_thesis: for A being SubSpace of T for Q being Subset of T st Q c= [#] A holds ( Q is compact iff for P being Subset of A st P = Q holds P is compact ) let A be SubSpace of T; ::_thesis: for Q being Subset of T st Q c= [#] A holds ( Q is compact iff for P being Subset of A st P = Q holds P is compact ) let Q be Subset of T; ::_thesis: ( Q c= [#] A implies ( Q is compact iff for P being Subset of A st P = Q holds P is compact ) ) [#] A c= [#] T by PRE_TOPC:def_4; then reconsider AA = [#] A as Subset of T ; assume A1: Q c= [#] A ; ::_thesis: ( Q is compact iff for P being Subset of A st P = Q holds P is compact ) then A2: Q /\ AA = Q by XBOOLE_1:28; thus ( Q is compact implies for P being Subset of A st P = Q holds P is compact ) ::_thesis: ( ( for P being Subset of A st P = Q holds P is compact ) implies Q is compact ) proof assume A3: Q is compact ; ::_thesis: for P being Subset of A st P = Q holds P is compact let P be Subset of A; ::_thesis: ( P = Q implies P is compact ) assume A4: P = Q ; ::_thesis: P is compact thus P is compact ::_thesis: verum proof let G be Subset-Family of A; :: according to COMPTS_1:def_4 ::_thesis: ( G is Cover of P & G is open implies ex G being Subset-Family of A st ( G c= G & G is Cover of P & G is finite ) ) set GG = G; assume that A5: G is Cover of P and A6: G is open ; ::_thesis: ex G being Subset-Family of A st ( G c= G & G is Cover of P & G is finite ) consider F being Subset-Family of T such that A7: F is open and A8: for AA being Subset of T st AA = [#] A holds G = F | AA by A6, TOPS_2:39; A9: Q c= union G by A4, A5, SETFAM_1:def_11; union (F | AA) c= union F by TOPS_2:34; then union G c= union F by A8; then Q c= union F by A9, XBOOLE_1:1; then F is Cover of Q by SETFAM_1:def_11; then consider F9 being Subset-Family of T such that A10: F9 c= F and A11: F9 is Cover of Q and A12: F9 is finite by A3, A7, Def4; F9 | AA c= bool ([#] (T | AA)) ; then reconsider G9 = F9 | AA as Subset-Family of A by PRE_TOPC:def_5; take G9 ; ::_thesis: ( G9 c= G & G9 is Cover of P & G9 is finite ) F9 | AA c= F | AA by A10, TOPS_2:30; hence G9 c= G by A8; ::_thesis: ( G9 is Cover of P & G9 is finite ) Q c= union F9 by A11, SETFAM_1:def_11; then P c= union G9 by A2, A4, TOPS_2:32; hence G9 is Cover of P by SETFAM_1:def_11; ::_thesis: G9 is finite thus G9 is finite by A12, TOPS_2:36; ::_thesis: verum end; end; thus ( ( for P being Subset of A st P = Q holds P is compact ) implies Q is compact ) ::_thesis: verum proof reconsider QQ = Q as Subset of A by A1; assume for P being Subset of A st P = Q holds P is compact ; ::_thesis: Q is compact then A13: QQ is compact ; thus Q is compact ::_thesis: verum proof let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of Q & F is open implies ex G being Subset-Family of T st ( G c= F & G is Cover of Q & G is finite ) ) set F9 = F; assume that A14: F is Cover of Q and A15: F is open ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of Q & G is finite ) consider f being Function such that A16: dom f = F and A17: rng f = F | AA and A18: for x being set st x in F holds for Q being Subset of T st Q = x holds f . x = Q /\ AA by TOPS_2:40; F | AA c= bool ([#] (T | AA)) ; then reconsider F9 = rng f as Subset-Family of A by A17, PRE_TOPC:def_5; A19: F9 is open proof let X be Subset of A; :: according to TOPS_2:def_1 ::_thesis: ( not X in F9 or X is open ) assume A20: X in F9 ; ::_thesis: X is open then reconsider Y = X as Subset of (T | AA) by A17; consider R being Subset of T such that A21: R in F and A22: R /\ AA = Y by A17, A20, TOPS_2:def_3; R is open by A15, A21, TOPS_2:def_1; then R in the topology of T by PRE_TOPC:def_2; then X in the topology of A by A22, PRE_TOPC:def_4; hence X is open by PRE_TOPC:def_2; ::_thesis: verum end; Q c= union F by A14, SETFAM_1:def_11; then QQ c= union F9 by A2, A17, TOPS_2:32; then F9 is Cover of QQ by SETFAM_1:def_11; then consider G being Subset-Family of A such that A23: G c= F9 and A24: G is Cover of QQ and A25: G is finite by A13, A19, Def4; consider X being set such that A26: X c= dom f and A27: X is finite and A28: f .: X = G by A23, A25, ORDERS_1:85; reconsider G9 = X as Subset-Family of T by A16, A26, TOPS_2:2; take G9 ; ::_thesis: ( G9 c= F & G9 is Cover of Q & G9 is finite ) Q c= union G9 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Q or x in union G9 ) assume A29: x in Q ; ::_thesis: x in union G9 QQ c= union G by A24, SETFAM_1:def_11; then consider Y being set such that A30: x in Y and A31: Y in G by A29, TARSKI:def_4; consider z being set such that A32: z in dom f and A33: z in X and A34: f . z = Y by A28, A31, FUNCT_1:def_6; reconsider Z = z as Subset of T by A16, A32; Y = Z /\ AA by A16, A18, A32, A34; then x in Z by A30, XBOOLE_0:def_4; hence x in union G9 by A33, TARSKI:def_4; ::_thesis: verum end; hence ( G9 c= F & G9 is Cover of Q & G9 is finite ) by A16, A26, A27, SETFAM_1:def_11; ::_thesis: verum end; end; end; theorem Th3: :: COMPTS_1:3 for T being TopStruct for P being Subset of T holds ( ( P = {} implies ( P is compact iff T | P is compact ) ) & ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) ) ) proof let T be TopStruct ; ::_thesis: for P being Subset of T holds ( ( P = {} implies ( P is compact iff T | P is compact ) ) & ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) ) ) let P be Subset of T; ::_thesis: ( ( P = {} implies ( P is compact iff T | P is compact ) ) & ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) ) ) A1: [#] (T | P) = P by PRE_TOPC:def_5; hence ( P = {} implies ( P is compact iff T | P is compact ) ) by Th1; ::_thesis: ( T is TopSpace-like & P <> {} implies ( P is compact iff T | P is compact ) ) assume that A2: T is TopSpace-like and A3: P <> {} ; ::_thesis: ( P is compact iff T | P is compact ) reconsider T9 = T as non empty TopSpace by A2, A3; reconsider P9 = P as non empty Subset of T9 by A3; A4: ( [#] (T9 | P9) is compact iff T9 | P9 is compact ) by Th1; hence ( P is compact implies T | P is compact ) by A1, Th2; ::_thesis: ( T | P is compact implies P is compact ) assume T | P is compact ; ::_thesis: P is compact then for Q being Subset of (T | P) st Q = P holds Q is compact by A4, PRE_TOPC:def_5; hence P is compact by A1, Th2; ::_thesis: verum end; theorem Th4: :: COMPTS_1:4 for T being non empty TopSpace holds ( T is compact iff for F being Subset-Family of T st F is centered & F is closed holds meet F <> {} ) proof let T be non empty TopSpace; ::_thesis: ( T is compact iff for F being Subset-Family of T st F is centered & F is closed holds meet F <> {} ) thus ( T is compact implies for F being Subset-Family of T st F is centered & F is closed holds meet F <> {} ) ::_thesis: ( ( for F being Subset-Family of T st F is centered & F is closed holds meet F <> {} ) implies T is compact ) proof assume A1: T is compact ; ::_thesis: for F being Subset-Family of T st F is centered & F is closed holds meet F <> {} let F be Subset-Family of T; ::_thesis: ( F is centered & F is closed implies meet F <> {} ) assume that A2: F is centered and A3: F is closed ; ::_thesis: meet F <> {} reconsider C = COMPLEMENT F as Subset-Family of T ; assume A4: meet F = {} ; ::_thesis: contradiction F <> {} by A2, FINSET_1:def_3; then union (COMPLEMENT F) = (meet F) ` by TOPS_2:7 .= [#] T by A4 ; then A5: COMPLEMENT F is Cover of T by SETFAM_1:def_11; COMPLEMENT F is open by A3, TOPS_2:9; then consider G9 being Subset-Family of T such that A6: G9 c= C and A7: G9 is Cover of T and A8: G9 is finite by A1, A5, Def1; set F9 = COMPLEMENT G9; A9: COMPLEMENT G9 is finite by A8, TOPS_2:8; A10: COMPLEMENT G9 c= F proof let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in COMPLEMENT G9 or X in F ) assume A11: X in COMPLEMENT G9 ; ::_thesis: X in F then reconsider X1 = X as Subset of T ; X1 ` in G9 by A11, SETFAM_1:def_7; then (X1 `) ` in F by A6, SETFAM_1:def_7; hence X in F ; ::_thesis: verum end; G9 <> {} by A7, TOPS_2:3; then A12: COMPLEMENT G9 <> {} by TOPS_2:5; meet (COMPLEMENT G9) = (union G9) ` by A7, TOPS_2:3, TOPS_2:6 .= ([#] T) \ ([#] T) by A7, SETFAM_1:45 .= {} by XBOOLE_1:37 ; hence contradiction by A2, A10, A9, A12, FINSET_1:def_3; ::_thesis: verum end; assume A13: for F being Subset-Family of T st F is centered & F is closed holds meet F <> {} ; ::_thesis: T is compact thus T is compact ::_thesis: verum proof let F be Subset-Family of T; :: according to COMPTS_1:def_1 ::_thesis: ( F is Cover of T & F is open implies ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is finite ) ) assume that A14: F is Cover of T and A15: F is open ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is finite ) reconsider G = COMPLEMENT F as Subset-Family of T ; A16: G is closed by A15, TOPS_2:10; F <> {} by A14, TOPS_2:3; then A17: G <> {} by TOPS_2:5; meet G = (union F) ` by A14, TOPS_2:3, TOPS_2:6 .= ([#] T) \ ([#] T) by A14, SETFAM_1:45 .= {} by XBOOLE_1:37 ; then not G is centered by A13, A16; then consider G9 being set such that A18: G9 <> {} and A19: G9 c= G and A20: G9 is finite and A21: meet G9 = {} by A17, FINSET_1:def_3; reconsider G9 = G9 as Subset-Family of T by A19, XBOOLE_1:1; take F9 = COMPLEMENT G9; ::_thesis: ( F9 c= F & F9 is Cover of T & F9 is finite ) thus F9 c= F ::_thesis: ( F9 is Cover of T & F9 is finite ) proof let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in F9 or A in F ) assume A22: A in F9 ; ::_thesis: A in F then reconsider A1 = A as Subset of T ; A1 ` in G9 by A22, SETFAM_1:def_7; then (A1 `) ` in F by A19, SETFAM_1:def_7; hence A in F ; ::_thesis: verum end; union F9 = (meet G9) ` by A18, TOPS_2:7 .= [#] T by A21 ; hence F9 is Cover of T by SETFAM_1:def_11; ::_thesis: F9 is finite thus F9 is finite by A20, TOPS_2:8; ::_thesis: verum end; end; theorem :: COMPTS_1:5 for T being non empty TopSpace holds ( T is compact iff for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds ex G being Subset-Family of T st ( G <> {} & G c= F & G is finite & meet G = {} ) ) proof let T be non empty TopSpace; ::_thesis: ( T is compact iff for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds ex G being Subset-Family of T st ( G <> {} & G c= F & G is finite & meet G = {} ) ) thus ( T is compact implies for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds ex G being Subset-Family of T st ( G <> {} & G c= F & G is finite & meet G = {} ) ) ::_thesis: ( ( for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds ex G being Subset-Family of T st ( G <> {} & G c= F & G is finite & meet G = {} ) ) implies T is compact ) proof assume A1: T is compact ; ::_thesis: for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds ex G being Subset-Family of T st ( G <> {} & G c= F & G is finite & meet G = {} ) let F be Subset-Family of T; ::_thesis: ( F <> {} & F is closed & meet F = {} implies ex G being Subset-Family of T st ( G <> {} & G c= F & G is finite & meet G = {} ) ) assume that A2: F <> {} and A3: F is closed and A4: meet F = {} ; ::_thesis: ex G being Subset-Family of T st ( G <> {} & G c= F & G is finite & meet G = {} ) not F is centered by A1, A3, A4, Th4; then consider G being set such that A5: G <> {} and A6: G c= F and A7: G is finite and A8: meet G = {} by A2, FINSET_1:def_3; reconsider G = G as Subset-Family of T by A6, XBOOLE_1:1; take G ; ::_thesis: ( G <> {} & G c= F & G is finite & meet G = {} ) thus ( G <> {} & G c= F & G is finite & meet G = {} ) by A5, A6, A7, A8; ::_thesis: verum end; assume A9: for F being Subset-Family of T st F <> {} & F is closed & meet F = {} holds ex G being Subset-Family of T st ( G <> {} & G c= F & G is finite & meet G = {} ) ; ::_thesis: T is compact for F being Subset-Family of T st F is centered & F is closed holds meet F <> {} proof let F be Subset-Family of T; ::_thesis: ( F is centered & F is closed implies meet F <> {} ) assume that A10: F is centered and A11: F is closed ; ::_thesis: meet F <> {} assume A12: meet F = {} ; ::_thesis: contradiction F <> {} by A10, FINSET_1:def_3; then ex G being Subset-Family of T st ( G <> {} & G c= F & G is finite & meet G = {} ) by A9, A11, A12; hence contradiction by A10, FINSET_1:def_3; ::_thesis: verum end; hence T is compact by Th4; ::_thesis: verum end; theorem Th6: :: COMPTS_1:6 for TS being TopSpace st TS is T_2 holds for A being Subset of TS st A <> {} & A is compact holds for p being Point of TS st p in A ` holds ex PS, QS being Subset of TS st ( PS is open & QS is open & p in PS & A c= QS & PS misses QS ) proof let TS be TopSpace; ::_thesis: ( TS is T_2 implies for A being Subset of TS st A <> {} & A is compact holds for p being Point of TS st p in A ` holds ex PS, QS being Subset of TS st ( PS is open & QS is open & p in PS & A c= QS & PS misses QS ) ) assume A1: TS is T_2 ; ::_thesis: for A being Subset of TS st A <> {} & A is compact holds for p being Point of TS st p in A ` holds ex PS, QS being Subset of TS st ( PS is open & QS is open & p in PS & A c= QS & PS misses QS ) let F be Subset of TS; ::_thesis: ( F <> {} & F is compact implies for p being Point of TS st p in F ` holds ex PS, QS being Subset of TS st ( PS is open & QS is open & p in PS & F c= QS & PS misses QS ) ) assume that A2: F <> {} and A3: F is compact ; ::_thesis: for p being Point of TS st p in F ` holds ex PS, QS being Subset of TS st ( PS is open & QS is open & p in PS & F c= QS & PS misses QS ) set z = the Element of F; let a be Point of TS; ::_thesis: ( a in F ` implies ex PS, QS being Subset of TS st ( PS is open & QS is open & a in PS & F c= QS & PS misses QS ) ) assume a in F ` ; ::_thesis: ex PS, QS being Subset of TS st ( PS is open & QS is open & a in PS & F c= QS & PS misses QS ) then A4: not a in F by XBOOLE_0:def_5; defpred S1[ set , set , set ] means ex PS, QS being Subset of TS st ( \$2 = PS & \$3 = QS & PS is open & QS is open & a in PS & \$1 in QS & PS /\ QS = {} ); A5: for x being set st x in F holds ex y, z being set st ( y in the topology of TS & z in the topology of TS & S1[x,y,z] ) proof let x be set ; ::_thesis: ( x in F implies ex y, z being set st ( y in the topology of TS & z in the topology of TS & S1[x,y,z] ) ) assume A6: x in F ; ::_thesis: ex y, z being set st ( y in the topology of TS & z in the topology of TS & S1[x,y,z] ) then reconsider p = x as Point of TS ; consider W, V being Subset of TS such that A7: W is open and A8: V is open and A9: a in W and A10: p in V and A11: W misses V by A1, A4, A6, PRE_TOPC:def_10; reconsider PS = W, QS = V as set ; take PS ; ::_thesis: ex z being set st ( PS in the topology of TS & z in the topology of TS & S1[x,PS,z] ) take QS ; ::_thesis: ( PS in the topology of TS & QS in the topology of TS & S1[x,PS,QS] ) thus ( PS in the topology of TS & QS in the topology of TS ) by A7, A8, PRE_TOPC:def_2; ::_thesis: S1[x,PS,QS] take W ; ::_thesis: ex QS being Subset of TS st ( PS = W & QS = QS & W is open & QS is open & a in W & x in QS & W /\ QS = {} ) take V ; ::_thesis: ( PS = W & QS = V & W is open & V is open & a in W & x in V & W /\ V = {} ) thus ( PS = W & QS = V & W is open & V is open & a in W & x in V & W /\ V = {} ) by A7, A8, A9, A10, A11, XBOOLE_0:def_7; ::_thesis: verum end; consider f, g being Function such that A12: ( dom f = F & dom g = F ) and A13: for x being set st x in F holds S1[x,f . x,g . x] from MCART_1:sch_1(A5); g .: F c= bool the carrier of TS proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: F or x in bool the carrier of TS ) assume x in g .: F ; ::_thesis: x in bool the carrier of TS then consider y being set such that y in dom g and A14: y in F and A15: g . y = x by FUNCT_1:def_6; ex PS, QS being Subset of TS st ( f . y = PS & g . y = QS & PS is open & QS is open & a in PS & y in QS & PS /\ QS = {} ) by A13, A14; hence x in bool the carrier of TS by A15; ::_thesis: verum end; then reconsider C = g .: F as Subset-Family of TS ; A16: C is open proof let G be Subset of TS; :: according to TOPS_2:def_1 ::_thesis: ( not G in C or G is open ) assume G in C ; ::_thesis: G is open then consider x being set such that x in dom g and A17: x in F and A18: G = g . x by FUNCT_1:def_6; ex PS, QS being Subset of TS st ( f . x = PS & g . x = QS & PS is open & QS is open & a in PS & x in QS & PS /\ QS = {} ) by A13, A17; hence G is open by A18; ::_thesis: verum end; F c= union C proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in union C ) assume A19: x in F ; ::_thesis: x in union C then consider PS, QS being Subset of TS such that f . x = PS and A20: g . x = QS and PS is open and QS is open and a in PS and A21: x in QS and PS /\ QS = {} by A13; QS in C by A12, A19, A20, FUNCT_1:def_6; hence x in union C by A21, TARSKI:def_4; ::_thesis: verum end; then C is Cover of F by SETFAM_1:def_11; then consider C9 being Subset-Family of TS such that A22: C9 c= C and A23: C9 is Cover of F and A24: C9 is finite by A3, A16, Def4; C9 c= rng g by A12, A22, RELAT_1:113; then consider H9 being set such that A25: H9 c= dom g and A26: H9 is finite and A27: g .: H9 = C9 by A24, ORDERS_1:85; f .: H9 c= bool the carrier of TS proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: H9 or x in bool the carrier of TS ) assume x in f .: H9 ; ::_thesis: x in bool the carrier of TS then consider y being set such that y in dom f and A28: y in H9 and A29: f . y = x by FUNCT_1:def_6; ex PS, QS being Subset of TS st ( f . y = PS & g . y = QS & PS is open & QS is open & a in PS & y in QS & PS /\ QS = {} ) by A12, A13, A25, A28; hence x in bool the carrier of TS by A29; ::_thesis: verum end; then reconsider B = f .: H9 as Subset-Family of TS ; take G0 = meet B; ::_thesis: ex QS being Subset of TS st ( G0 is open & QS is open & a in G0 & F c= QS & G0 misses QS ) take G1 = union C9; ::_thesis: ( G0 is open & G1 is open & a in G0 & F c= G1 & G0 misses G1 ) B is open proof let G be Subset of TS; :: according to TOPS_2:def_1 ::_thesis: ( not G in B or G is open ) assume G in B ; ::_thesis: G is open then consider x being set such that A30: x in dom f and x in H9 and A31: G = f . x by FUNCT_1:def_6; ex PS, QS being Subset of TS st ( f . x = PS & g . x = QS & PS is open & QS is open & a in PS & x in QS & PS /\ QS = {} ) by A12, A13, A30; hence G is open by A31; ::_thesis: verum end; hence G0 is open by A26, TOPS_2:20; ::_thesis: ( G1 is open & a in G0 & F c= G1 & G0 misses G1 ) thus G1 is open by A16, A22, TOPS_2:11, TOPS_2:19; ::_thesis: ( a in G0 & F c= G1 & G0 misses G1 ) A32: for G being set st G in B holds a in G proof let G be set ; ::_thesis: ( G in B implies a in G ) assume A33: G in B ; ::_thesis: a in G then reconsider G9 = G as Subset of TS ; consider x being set such that A34: x in dom f and x in H9 and A35: G9 = f . x by A33, FUNCT_1:def_6; ex PS, QS being Subset of TS st ( f . x = PS & g . x = QS & PS is open & QS is open & a in PS & x in QS & PS /\ QS = {} ) by A12, A13, A34; hence a in G by A35; ::_thesis: verum end; F c= union C9 by A23, SETFAM_1:def_11; then the Element of F in union C9 by A2, TARSKI:def_3; then consider D being set such that the Element of F in D and A36: D in C9 by TARSKI:def_4; reconsider D9 = D as Subset of TS by A36; consider y being set such that A37: y in dom g and A38: y in H9 and D9 = g . y by A27, A36, FUNCT_1:def_6; ex PS, QS being Subset of TS st ( f . y = PS & g . y = QS & PS is open & QS is open & a in PS & y in QS & PS /\ QS = {} ) by A12, A13, A37; then B <> {} by A12, A37, A38, FUNCT_1:def_6; hence a in G0 by A32, SETFAM_1:def_1; ::_thesis: ( F c= G1 & G0 misses G1 ) thus F c= G1 by A23, SETFAM_1:def_11; ::_thesis: G0 misses G1 thus G0 /\ G1 = {} :: according to XBOOLE_0:def_7 ::_thesis: verum proof set x = the Element of (meet B) /\ (union C9); assume A39: G0 /\ G1 <> {} ; ::_thesis: contradiction then A40: the Element of (meet B) /\ (union C9) in meet B by XBOOLE_0:def_4; the Element of (meet B) /\ (union C9) in union C9 by A39, XBOOLE_0:def_4; then consider A being set such that A41: the Element of (meet B) /\ (union C9) in A and A42: A in C9 by TARSKI:def_4; consider z being set such that A43: z in dom g and A44: z in H9 and A45: A = g . z by A27, A42, FUNCT_1:def_6; consider PS, QS being Subset of TS such that A46: f . z = PS and A47: g . z = QS and PS is open and QS is open and a in PS and z in QS and A48: PS /\ QS = {} by A12, A13, A43; PS in B by A12, A43, A44, A46, FUNCT_1:def_6; then the Element of (meet B) /\ (union C9) in PS by A40, SETFAM_1:def_1; hence contradiction by A41, A45, A47, A48, XBOOLE_0:def_4; ::_thesis: verum end; end; theorem Th7: :: COMPTS_1:7 for TS being TopSpace for PS being Subset of TS st TS is T_2 & PS is compact holds PS is closed proof let TS be TopSpace; ::_thesis: for PS being Subset of TS st TS is T_2 & PS is compact holds PS is closed let PS be Subset of TS; ::_thesis: ( TS is T_2 & PS is compact implies PS is closed ) assume that A1: TS is T_2 and A2: PS is compact ; ::_thesis: PS is closed percases ( PS = {} or PS <> {} ) ; suppose PS = {} ; ::_thesis: PS is closed hence PS is closed ; ::_thesis: verum end; supposeA3: PS <> {} ; ::_thesis: PS is closed now__::_thesis:_for_a_being_set_holds_ (_(_a_in_PS_`_implies_ex_Q_being_Subset_of_TS_st_ (_Q_is_open_&_Q_c=_PS_`_&_a_in_Q_)_)_&_(_ex_Q_being_Subset_of_TS_st_ (_Q_is_open_&_Q_c=_PS_`_&_a_in_Q_)_implies_a_in_PS_`_)_) let a be set ; ::_thesis: ( ( a in PS ` implies ex Q being Subset of TS st ( Q is open & Q c= PS ` & a in Q ) ) & ( ex Q being Subset of TS st ( Q is open & Q c= PS ` & a in Q ) implies a in PS ` ) ) thus ( a in PS ` implies ex Q being Subset of TS st ( Q is open & Q c= PS ` & a in Q ) ) ::_thesis: ( ex Q being Subset of TS st ( Q is open & Q c= PS ` & a in Q ) implies a in PS ` ) proof assume A4: a in PS ` ; ::_thesis: ex Q being Subset of TS st ( Q is open & Q c= PS ` & a in Q ) then reconsider p = a as Point of TS ; consider W, V being Subset of TS such that A5: W is open and V is open and A6: p in W and A7: PS c= V and A8: W misses V by A1, A2, A3, A4, Th6; take Q = W; ::_thesis: ( Q is open & Q c= PS ` & a in Q ) W misses (V `) ` by A8; then A9: W c= V ` by SUBSET_1:24; V ` c= PS ` by A7, SUBSET_1:12; hence ( Q is open & Q c= PS ` & a in Q ) by A5, A6, A9, XBOOLE_1:1; ::_thesis: verum end; thus ( ex Q being Subset of TS st ( Q is open & Q c= PS ` & a in Q ) implies a in PS ` ) ; ::_thesis: verum end; then PS ` is open by TOPS_1:25; hence PS is closed by TOPS_1:3; ::_thesis: verum end; end; end; theorem Th8: :: COMPTS_1:8 for T being TopStruct for P being Subset of T st T is compact & P is closed holds P is compact proof let T be TopStruct ; ::_thesis: for P being Subset of T st T is compact & P is closed holds P is compact let P be Subset of T; ::_thesis: ( T is compact & P is closed implies P is compact ) assume that A1: T is compact and A2: P is closed ; ::_thesis: P is compact reconsider pp = {(P `)} as Subset-Family of T ; let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of P & F is open implies ex G being Subset-Family of T st ( G c= F & G is Cover of P & G is finite ) ) assume that A3: F is Cover of P and A4: F is open ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of P & G is finite ) set FP = F \/ pp; A5: P ` is open by A2, TOPS_1:3; A6: F \/ pp is open proof let H be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not H in F \/ pp or H is open ) assume H in F \/ pp ; ::_thesis: H is open then ( H in F or H in {(P `)} ) by XBOOLE_0:def_3; hence H is open by A4, A5, TARSKI:def_1, TOPS_2:def_1; ::_thesis: verum end; reconsider M = {(P `)} as Subset-Family of T ; (F \/ {(P `)}) \ {(P `)} = F \ {(P `)} by XBOOLE_1:40; then A7: (F \/ {(P `)}) \ {(P `)} c= F by XBOOLE_1:36; P c= union F by A3, SETFAM_1:def_11; then P \/ (P `) c= (union F) \/ (P `) by XBOOLE_1:9; then [#] T c= (union F) \/ (P `) by PRE_TOPC:2; then [#] T = (union F) \/ (P `) by XBOOLE_0:def_10 .= (union F) \/ (union {(P `)}) by ZFMISC_1:25 .= union (F \/ {(P `)}) by ZFMISC_1:78 ; then F \/ pp is Cover of T by SETFAM_1:def_11; then consider G being Subset-Family of T such that A8: G c= F \/ pp and A9: G is Cover of T and A10: G is finite by A1, A6, Def1; reconsider G9 = G \ pp as Subset-Family of T ; take G9 ; ::_thesis: ( G9 c= F & G9 is Cover of P & G9 is finite ) G9 c= (F \/ {(P `)}) \ {(P `)} by A8, XBOOLE_1:33; hence G9 c= F by A7, XBOOLE_1:1; ::_thesis: ( G9 is Cover of P & G9 is finite ) (union G) \ (union M) = ([#] T) \ (union {(P `)}) by A9, SETFAM_1:45 .= (P `) ` by ZFMISC_1:25 .= P ; then P c= union G9 by TOPS_2:4; hence G9 is Cover of P by SETFAM_1:def_11; ::_thesis: G9 is finite thus G9 is finite by A10; ::_thesis: verum end; theorem Th9: :: COMPTS_1:9 for TS being TopSpace for PS, QS being Subset of TS st PS is compact & QS c= PS & QS is closed holds QS is compact proof let TS be TopSpace; ::_thesis: for PS, QS being Subset of TS st PS is compact & QS c= PS & QS is closed holds QS is compact let PS, QS be Subset of TS; ::_thesis: ( PS is compact & QS c= PS & QS is closed implies QS is compact ) assume that A1: PS is compact and A2: QS c= PS and A3: QS is closed ; ::_thesis: QS is compact percases ( PS = {} or PS <> {} ) ; suppose PS = {} ; ::_thesis: QS is compact hence QS is compact by A2; ::_thesis: verum end; suppose PS <> {} ; ::_thesis: QS is compact then TS | PS is compact by A1, Th3; then A4: for QQ being Subset of (TS | PS) st QQ = QS holds QQ is compact by A3, Th8, TOPS_2:26; PS = [#] (TS | PS) by PRE_TOPC:def_5; hence QS is compact by A2, A4, Th2; ::_thesis: verum end; end; end; theorem :: COMPTS_1:10 for T being TopStruct for P, Q being Subset of T st P is compact & Q is compact holds P \/ Q is compact proof let T be TopStruct ; ::_thesis: for P, Q being Subset of T st P is compact & Q is compact holds P \/ Q is compact let P, Q be Subset of T; ::_thesis: ( P is compact & Q is compact implies P \/ Q is compact ) assume that A1: P is compact and A2: Q is compact ; ::_thesis: P \/ Q is compact let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of P \/ Q & F is open implies ex G being Subset-Family of T st ( G c= F & G is Cover of P \/ Q & G is finite ) ) assume that A3: F is Cover of P \/ Q and A4: F is open ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of P \/ Q & G is finite ) A5: P \/ Q c= union F by A3, SETFAM_1:def_11; Q c= P \/ Q by XBOOLE_1:7; then Q c= union F by A5, XBOOLE_1:1; then F is Cover of Q by SETFAM_1:def_11; then consider G2 being Subset-Family of T such that A6: G2 c= F and A7: G2 is Cover of Q and A8: G2 is finite by A2, A4, Def4; A9: Q c= union G2 by A7, SETFAM_1:def_11; P c= P \/ Q by XBOOLE_1:7; then P c= union F by A5, XBOOLE_1:1; then F is Cover of P by SETFAM_1:def_11; then consider G1 being Subset-Family of T such that A10: G1 c= F and A11: G1 is Cover of P and A12: G1 is finite by A1, A4, Def4; reconsider G = G1 \/ G2 as Subset-Family of T ; take G ; ::_thesis: ( G c= F & G is Cover of P \/ Q & G is finite ) thus G c= F by A10, A6, XBOOLE_1:8; ::_thesis: ( G is Cover of P \/ Q & G is finite ) P c= union G1 by A11, SETFAM_1:def_11; then P \/ Q c= (union G1) \/ (union G2) by A9, XBOOLE_1:13; then P \/ Q c= union (G1 \/ G2) by ZFMISC_1:78; hence G is Cover of P \/ Q by SETFAM_1:def_11; ::_thesis: G is finite thus G is finite by A12, A8; ::_thesis: verum end; theorem :: COMPTS_1:11 for TS being TopSpace for PS, QS being Subset of TS st TS is T_2 & PS is compact & QS is compact holds PS /\ QS is compact proof let TS be TopSpace; ::_thesis: for PS, QS being Subset of TS st TS is T_2 & PS is compact & QS is compact holds PS /\ QS is compact let PS, QS be Subset of TS; ::_thesis: ( TS is T_2 & PS is compact & QS is compact implies PS /\ QS is compact ) assume that A1: TS is T_2 and A2: PS is compact and A3: QS is compact ; ::_thesis: PS /\ QS is compact A4: QS is closed by A1, A3, Th7; PS is closed by A1, A2, Th7; hence PS /\ QS is compact by A2, A4, Th9, XBOOLE_1:17; ::_thesis: verum end; theorem :: COMPTS_1:12 for TS being non empty TopSpace st TS is T_2 & TS is compact holds TS is regular proof let TS be non empty TopSpace; ::_thesis: ( TS is T_2 & TS is compact implies TS is regular ) assume that A1: TS is T_2 and A2: TS is compact ; ::_thesis: TS is regular let p be Point of TS; :: according to COMPTS_1:def_2 ::_thesis: for P being Subset of TS st P <> {} & P is closed & p in P ` holds ex W, V being Subset of TS st ( W is open & V is open & p in W & P c= V & W misses V ) let F be Subset of TS; ::_thesis: ( F <> {} & F is closed & p in F ` implies ex W, V being Subset of TS st ( W is open & V is open & p in W & F c= V & W misses V ) ) assume that A3: F <> {} and A4: F is closed and A5: p in F ` ; ::_thesis: ex W, V being Subset of TS st ( W is open & V is open & p in W & F c= V & W misses V ) thus ex W, V being Subset of TS st ( W is open & V is open & p in W & F c= V & W misses V ) by A1, A2, A3, A4, A5, Th6, Th8; ::_thesis: verum end; theorem :: COMPTS_1:13 for TS being non empty TopSpace st TS is T_2 & TS is compact holds TS is normal proof let TS be non empty TopSpace; ::_thesis: ( TS is T_2 & TS is compact implies TS is normal ) assume that A1: TS is T_2 and A2: TS is compact ; ::_thesis: TS is normal let A, B be Subset of TS; :: according to COMPTS_1:def_3 ::_thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex P, Q being Subset of TS st ( P is open & Q is open & A c= P & B c= Q & P misses Q ) ) assume that A3: A <> {} and A4: B <> {} and A5: A is closed and A6: B is closed and A7: A /\ B = {} ; :: according to XBOOLE_0:def_7 ::_thesis: ex P, Q being Subset of TS st ( P is open & Q is open & A c= P & B c= Q & P misses Q ) defpred S1[ set , set , set ] means ex P, Q being Subset of TS st ( \$2 = P & \$3 = Q & P is open & Q is open & \$1 in P & B c= Q & P /\ Q = {} ); A8: for x being set st x in A holds ex y, z being set st ( y in the topology of TS & z in the topology of TS & S1[x,y,z] ) proof let x be set ; ::_thesis: ( x in A implies ex y, z being set st ( y in the topology of TS & z in the topology of TS & S1[x,y,z] ) ) assume A9: x in A ; ::_thesis: ex y, z being set st ( y in the topology of TS & z in the topology of TS & S1[x,y,z] ) then reconsider p = x as Point of TS ; not p in B by A7, A9, XBOOLE_0:def_4; then p in B ` by SUBSET_1:29; then consider W, V being Subset of TS such that A10: W is open and A11: V is open and A12: p in W and A13: B c= V and A14: W misses V by A1, A2, A4, A6, Th6, Th8; reconsider X = W, Y = V as set ; take X ; ::_thesis: ex z being set st ( X in the topology of TS & z in the topology of TS & S1[x,X,z] ) take Y ; ::_thesis: ( X in the topology of TS & Y in the topology of TS & S1[x,X,Y] ) thus ( X in the topology of TS & Y in the topology of TS ) by A10, A11, PRE_TOPC:def_2; ::_thesis: S1[x,X,Y] W /\ V = {} by A14, XBOOLE_0:def_7; hence S1[x,X,Y] by A10, A11, A12, A13; ::_thesis: verum end; consider f, g being Function such that A15: ( dom f = A & dom g = A ) and A16: for x being set st x in A holds S1[x,f . x,g . x] from MCART_1:sch_1(A8); f .: A c= bool the carrier of TS proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f .: A or x in bool the carrier of TS ) assume x in f .: A ; ::_thesis: x in bool the carrier of TS then consider y being set such that y in dom f and A17: y in A and A18: f . y = x by FUNCT_1:def_6; ex P, Q being Subset of TS st ( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A16, A17; hence x in bool the carrier of TS by A18; ::_thesis: verum end; then reconsider Cf = f .: A as Subset-Family of TS ; A c= union Cf proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in union Cf ) assume A19: x in A ; ::_thesis: x in union Cf then consider P, Q being Subset of TS such that A20: f . x = P and g . x = Q and P is open and Q is open and A21: x in P and B c= Q and P /\ Q = {} by A16; P in Cf by A15, A19, A20, FUNCT_1:def_6; hence x in union Cf by A21, TARSKI:def_4; ::_thesis: verum end; then A22: Cf is Cover of A by SETFAM_1:def_11; A23: Cf is open proof let G be Subset of TS; :: according to TOPS_2:def_1 ::_thesis: ( not G in Cf or G is open ) assume G in Cf ; ::_thesis: G is open then consider x being set such that x in dom f and A24: x in A and A25: G = f . x by FUNCT_1:def_6; ex P, Q being Subset of TS st ( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A16, A24; hence G is open by A25; ::_thesis: verum end; A is compact by A2, A5, Th8; then consider C being Subset-Family of TS such that A26: C c= Cf and A27: C is Cover of A and A28: C is finite by A22, A23, Def4; set z = the Element of A; A c= union C by A27, SETFAM_1:def_11; then the Element of A in union C by A3, TARSKI:def_3; then consider D being set such that the Element of A in D and A29: D in C by TARSKI:def_4; C c= rng f by A15, A26, RELAT_1:113; then consider H9 being set such that A30: H9 c= dom f and A31: H9 is finite and A32: f .: H9 = C by A28, ORDERS_1:85; g .: H9 c= bool the carrier of TS proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in g .: H9 or x in bool the carrier of TS ) assume x in g .: H9 ; ::_thesis: x in bool the carrier of TS then consider y being set such that y in dom g and A33: y in H9 and A34: g . y = x by FUNCT_1:def_6; ex P, Q being Subset of TS st ( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A15, A16, A30, A33; hence x in bool the carrier of TS by A34; ::_thesis: verum end; then reconsider Bk = g .: H9 as Subset-Family of TS ; consider y being set such that A35: y in dom f and A36: y in H9 and D = f . y by A32, A29, FUNCT_1:def_6; A37: for X being set st X in Bk holds B c= X proof let X be set ; ::_thesis: ( X in Bk implies B c= X ) assume A38: X in Bk ; ::_thesis: B c= X then reconsider X9 = X as Subset of TS ; consider x being set such that A39: x in dom g and x in H9 and A40: X9 = g . x by A38, FUNCT_1:def_6; ex P, Q being Subset of TS st ( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A15, A16, A39; hence B c= X by A40; ::_thesis: verum end; take W = union C; ::_thesis: ex Q being Subset of TS st ( W is open & Q is open & A c= W & B c= Q & W misses Q ) take V = meet Bk; ::_thesis: ( W is open & V is open & A c= W & B c= V & W misses V ) thus W is open by A23, A26, TOPS_2:11, TOPS_2:19; ::_thesis: ( V is open & A c= W & B c= V & W misses V ) Bk is open proof let G be Subset of TS; :: according to TOPS_2:def_1 ::_thesis: ( not G in Bk or G is open ) assume G in Bk ; ::_thesis: G is open then consider x being set such that A41: x in dom g and x in H9 and A42: G = g . x by FUNCT_1:def_6; ex P, Q being Subset of TS st ( f . x = P & g . x = Q & P is open & Q is open & x in P & B c= Q & P /\ Q = {} ) by A15, A16, A41; hence G is open by A42; ::_thesis: verum end; hence V is open by A31, TOPS_2:20; ::_thesis: ( A c= W & B c= V & W misses V ) thus A c= W by A27, SETFAM_1:def_11; ::_thesis: ( B c= V & W misses V ) ex P, Q being Subset of TS st ( f . y = P & g . y = Q & P is open & Q is open & y in P & B c= Q & P /\ Q = {} ) by A15, A16, A35; then Bk <> {} by A15, A35, A36, FUNCT_1:def_6; hence B c= V by A37, SETFAM_1:5; ::_thesis: W misses V thus W /\ V = {} :: according to XBOOLE_0:def_7 ::_thesis: verum proof set x = the Element of (union C) /\ (meet Bk); assume A43: W /\ V <> {} ; ::_thesis: contradiction then A44: the Element of (union C) /\ (meet Bk) in meet Bk by XBOOLE_0:def_4; the Element of (union C) /\ (meet Bk) in union C by A43, XBOOLE_0:def_4; then consider D being set such that A45: the Element of (union C) /\ (meet Bk) in D and A46: D in C by TARSKI:def_4; consider z being set such that A47: z in dom f and A48: z in H9 and A49: D = f . z by A32, A46, FUNCT_1:def_6; consider P, Q being Subset of TS such that A50: f . z = P and A51: g . z = Q and P is open and Q is open and z in P and B c= Q and A52: P /\ Q = {} by A15, A16, A47; Q in Bk by A15, A47, A48, A51, FUNCT_1:def_6; then the Element of (union C) /\ (meet Bk) in Q by A44, SETFAM_1:def_1; hence contradiction by A45, A49, A50, A52, XBOOLE_0:def_4; ::_thesis: verum end; end; theorem :: COMPTS_1:14 for T being TopStruct for S being non empty TopStruct for f being Function of T,S st T is compact & f is continuous & rng f = [#] S holds S is compact proof let T be TopStruct ; ::_thesis: for S being non empty TopStruct for f being Function of T,S st T is compact & f is continuous & rng f = [#] S holds S is compact let S be non empty TopStruct ; ::_thesis: for f being Function of T,S st T is compact & f is continuous & rng f = [#] S holds S is compact let f be Function of T,S; ::_thesis: ( T is compact & f is continuous & rng f = [#] S implies S is compact ) assume A1: T is compact ; ::_thesis: ( not f is continuous or not rng f = [#] S or S is compact ) [#] T c= dom f by FUNCT_2:def_1; then A2: [#] T c= f " (f .: ([#] T)) by FUNCT_1:76; assume that A3: f is continuous and A4: rng f = [#] S ; ::_thesis: S is compact let F be Subset-Family of S; :: according to COMPTS_1:def_1 ::_thesis: ( F is Cover of S & F is open implies ex G being Subset-Family of S st ( G c= F & G is Cover of S & G is finite ) ) assume that A5: F is Cover of S and A6: F is open ; ::_thesis: ex G being Subset-Family of S st ( G c= F & G is Cover of S & G is finite ) set F1 = F; reconsider G = (" f) .: F as Subset-Family of T by TOPS_2:42; union G = f " (union F) by A4, FUNCT_3:26 .= f " (rng f) by A4, A5, SETFAM_1:45 .= f " (f .: (dom f)) by RELAT_1:113 .= f " (f .: ([#] T)) by FUNCT_2:def_1 ; then A7: G is Cover of T by A2, SETFAM_1:def_11; A8: (.: f) .: ((.: f) " F) c= F by FUNCT_1:75; (.: f) .: ((" f) .: F) c= (.: f) .: ((.: f) " F) by FUNCT_3:29, RELAT_1:123; then A9: (.: f) .: G c= F by A8, XBOOLE_1:1; G is open by A3, A6, TOPS_2:47; then consider G9 being Subset-Family of T such that A10: G9 c= G and A11: G9 is Cover of T and A12: G9 is finite by A1, A7, Def1; reconsider F9 = (.: f) .: G9 as Subset-Family of S ; take F9 ; ::_thesis: ( F9 c= F & F9 is Cover of S & F9 is finite ) (.: f) .: G9 c= (.: f) .: G by A10, RELAT_1:123; hence F9 c= F by A9, XBOOLE_1:1; ::_thesis: ( F9 is Cover of S & F9 is finite ) dom f = [#] T by FUNCT_2:def_1; then union F9 = f .: (union G9) by FUNCT_3:14 .= f .: ([#] T) by A11, SETFAM_1:45 .= f .: (dom f) by FUNCT_2:def_1 .= [#] S by A4, RELAT_1:113 ; hence F9 is Cover of S by SETFAM_1:def_11; ::_thesis: F9 is finite thus F9 is finite by A12; ::_thesis: verum end; theorem Th15: :: COMPTS_1:15 for T being TopStruct for P being Subset of T for S being non empty TopStruct for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds f .: P is compact proof let T be TopStruct ; ::_thesis: for P being Subset of T for S being non empty TopStruct for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds f .: P is compact let P be Subset of T; ::_thesis: for S being non empty TopStruct for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds f .: P is compact let S be non empty TopStruct ; ::_thesis: for f being Function of T,S st f is continuous & rng f = [#] S & P is compact holds f .: P is compact let f be Function of T,S; ::_thesis: ( f is continuous & rng f = [#] S & P is compact implies f .: P is compact ) assume that A1: f is continuous and A2: rng f = [#] S and A3: P is compact ; ::_thesis: f .: P is compact let F be Subset-Family of S; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of f .: P & F is open implies ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) ) assume that A4: F is Cover of f .: P and A5: F is open ; ::_thesis: ex G being Subset-Family of S st ( G c= F & G is Cover of f .: P & G is finite ) reconsider G = (" f) .: F as Subset-Family of T by TOPS_2:42; f .: P c= union F by A4, SETFAM_1:def_11; then A6: f " (f .: P) c= f " (union F) by RELAT_1:143; P c= [#] T ; then P c= dom f by FUNCT_2:def_1; then A7: P c= f " (f .: P) by FUNCT_1:76; union G = f " (union F) by A2, FUNCT_3:26; then P c= union G by A6, A7, XBOOLE_1:1; then A8: G is Cover of P by SETFAM_1:def_11; G is open by A1, A5, TOPS_2:47; then consider G9 being Subset-Family of T such that A9: G9 c= G and A10: G9 is Cover of P and A11: G9 is finite by A3, A8, Def4; reconsider F9 = (.: f) .: G9 as Subset-Family of S ; take F9 ; ::_thesis: ( F9 c= F & F9 is Cover of f .: P & F9 is finite ) A12: (.: f) .: ((.: f) " F) c= F by FUNCT_1:75; (.: f) .: ((" f) .: F) c= (.: f) .: ((.: f) " F) by FUNCT_3:29, RELAT_1:123; then A13: (.: f) .: G c= F by A12, XBOOLE_1:1; (.: f) .: G9 c= (.: f) .: G by A9, RELAT_1:123; hence F9 c= F by A13, XBOOLE_1:1; ::_thesis: ( F9 is Cover of f .: P & F9 is finite ) A14: P c= union G9 by A10, SETFAM_1:def_11; dom f = [#] T by FUNCT_2:def_1; then union F9 = f .: (union G9) by FUNCT_3:14; then f .: P c= union F9 by A14, RELAT_1:123; hence F9 is Cover of f .: P by SETFAM_1:def_11; ::_thesis: F9 is finite thus F9 is finite by A11; ::_thesis: verum end; theorem Th16: :: COMPTS_1:16 for TS being TopSpace for SS being non empty TopSpace for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is continuous holds for PS being Subset of TS st PS is closed holds f .: PS is closed proof let TS be TopSpace; ::_thesis: for SS being non empty TopSpace for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is continuous holds for PS being Subset of TS st PS is closed holds f .: PS is closed let SS be non empty TopSpace; ::_thesis: for f being Function of TS,SS st TS is compact & SS is T_2 & rng f = [#] SS & f is continuous holds for PS being Subset of TS st PS is closed holds f .: PS is closed let f be Function of TS,SS; ::_thesis: ( TS is compact & SS is T_2 & rng f = [#] SS & f is continuous implies for PS being Subset of TS st PS is closed holds f .: PS is closed ) assume that A1: TS is compact and A2: SS is T_2 and A3: rng f = [#] SS and A4: f is continuous ; ::_thesis: for PS being Subset of TS st PS is closed holds f .: PS is closed let PS be Subset of TS; ::_thesis: ( PS is closed implies f .: PS is closed ) assume PS is closed ; ::_thesis: f .: PS is closed then PS is compact by A1, Th8; hence f .: PS is closed by A2, A3, A4, Th7, Th15; ::_thesis: verum end; theorem :: COMPTS_1:17 for TS being TopSpace for SS being non empty TopSpace for f being Function of TS,SS st TS is compact & SS is T_2 & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous holds f is being_homeomorphism proof let TS be TopSpace; ::_thesis: for SS being non empty TopSpace for f being Function of TS,SS st TS is compact & SS is T_2 & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous holds f is being_homeomorphism let SS be non empty TopSpace; ::_thesis: for f being Function of TS,SS st TS is compact & SS is T_2 & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous holds f is being_homeomorphism let f be Function of TS,SS; ::_thesis: ( TS is compact & SS is T_2 & dom f = [#] TS & rng f = [#] SS & f is one-to-one & f is continuous implies f is being_homeomorphism ) assume that A1: TS is compact and A2: SS is T_2 and A3: dom f = [#] TS and A4: rng f = [#] SS and A5: f is one-to-one and A6: f is continuous ; ::_thesis: f is being_homeomorphism for P being Subset of TS holds ( P is closed iff f .: P is closed ) proof let P be Subset of TS; ::_thesis: ( P is closed iff f .: P is closed ) dom f = [#] TS by FUNCT_2:def_1; then A7: P c= f " (f .: P) by FUNCT_1:76; thus ( P is closed implies f .: P is closed ) by A1, A2, A4, A6, Th16; ::_thesis: ( f .: P is closed implies P is closed ) assume f .: P is closed ; ::_thesis: P is closed then A8: f " (f .: P) is closed by A6, PRE_TOPC:def_6; f " (f .: P) c= P by A5, FUNCT_1:82; hence P is closed by A8, A7, XBOOLE_0:def_10; ::_thesis: verum end; hence f is being_homeomorphism by A3, A4, A5, TOPS_2:58; ::_thesis: verum end; definition let D be set ; func 1TopSp D -> TopStruct equals :: COMPTS_1:def 5 TopStruct(# D,([#] (bool D)) #); coherence TopStruct(# D,([#] (bool D)) #) is TopStruct ; end; :: deftheorem defines 1TopSp COMPTS_1:def_5_:_ for D being set holds 1TopSp D = TopStruct(# D,([#] (bool D)) #); registration let D be set ; cluster 1TopSp D -> strict TopSpace-like ; coherence ( 1TopSp D is strict & 1TopSp D is TopSpace-like ) proof thus 1TopSp D is strict ; ::_thesis: 1TopSp D is TopSpace-like set T = 1TopSp D; A1: for X being Subset-Family of (1TopSp D) st X c= the topology of (1TopSp D) holds union X in the topology of (1TopSp D) ; A2: for p, q being Subset of (1TopSp D) st p in the topology of (1TopSp D) & q in the topology of (1TopSp D) holds p /\ q in the topology of (1TopSp D) ; D in bool D by ZFMISC_1:def_1; hence 1TopSp D is TopSpace-like by A1, A2, PRE_TOPC:def_1; ::_thesis: verum end; end; registration let D be non empty set ; cluster 1TopSp D -> non empty ; coherence not 1TopSp D is empty ; end; registration let x be set ; cluster 1TopSp {x} -> T_2 ; coherence 1TopSp {x} is Hausdorff proof let p, q be Point of (1TopSp {x}); :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of (1TopSp {x}) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) assume A1: p <> q ; ::_thesis: ex b1, b2 being Element of bool the carrier of (1TopSp {x}) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) p = x by TARSKI:def_1; hence ex b1, b2 being Element of bool the carrier of (1TopSp {x}) st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) by A1, TARSKI:def_1; ::_thesis: verum end; end; registration cluster non empty TopSpace-like T_2 for TopStruct ; existence ex b1 being TopSpace st ( b1 is T_2 & not b1 is empty ) proof take 1TopSp {{}} ; ::_thesis: ( 1TopSp {{}} is T_2 & not 1TopSp {{}} is empty ) thus ( 1TopSp {{}} is T_2 & not 1TopSp {{}} is empty ) ; ::_thesis: verum end; end; registration let T be non empty T_2 TopSpace; cluster compact -> closed for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is compact holds b1 is closed by Th7; end; registration let A be finite set ; cluster 1TopSp A -> finite ; coherence 1TopSp A is finite ; end; registration cluster non empty finite strict TopSpace-like for TopStruct ; existence ex b1 being TopSpace st ( not b1 is empty & b1 is finite & b1 is strict ) proof take 1TopSp {{}} ; ::_thesis: ( not 1TopSp {{}} is empty & 1TopSp {{}} is finite & 1TopSp {{}} is strict ) thus ( not 1TopSp {{}} is empty & 1TopSp {{}} is finite & 1TopSp {{}} is strict ) ; ::_thesis: verum end; end; registration cluster finite TopSpace-like -> compact for TopStruct ; coherence for b1 being TopSpace st b1 is finite holds b1 is compact proof let T be TopSpace; ::_thesis: ( T is finite implies T is compact ) assume A1: the carrier of T is finite ; :: according to STRUCT_0:def_11 ::_thesis: T is compact let F be Subset-Family of T; :: according to COMPTS_1:def_1 ::_thesis: ( F is Cover of T & F is open implies ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is finite ) ) assume that A2: F is Cover of T and F is open ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of T & G is finite ) take F ; ::_thesis: ( F c= F & F is Cover of T & F is finite ) thus ( F c= F & F is Cover of T ) by A2; ::_thesis: F is finite thus F is finite by A1; ::_thesis: verum end; end; theorem Th18: :: COMPTS_1:18 for T being TopSpace st the carrier of T is finite holds T is compact proof let T be TopSpace; ::_thesis: ( the carrier of T is finite implies T is compact ) assume the carrier of T is finite ; ::_thesis: T is compact then T is finite ; hence T is compact ; ::_thesis: verum end; registration let T be TopSpace; cluster finite -> compact for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is finite holds b1 is compact proof let A be Subset of T; ::_thesis: ( A is finite implies A is compact ) assume A is finite ; ::_thesis: A is compact then reconsider B = A as finite Subset of T ; [#] (T | B) = B by PRE_TOPC:def_5; then A1: T | B is compact by Th18; ( B = {} or B <> {} ) ; hence A is compact by A1, Th3; ::_thesis: verum end; end; registration let T be non empty TopSpace; cluster non empty compact for Element of bool the carrier of T; existence ex b1 being Subset of T st ( not b1 is empty & b1 is compact ) proof set A = the non empty finite Subset of T; take the non empty finite Subset of T ; ::_thesis: ( not the non empty finite Subset of T is empty & the non empty finite Subset of T is compact ) thus ( not the non empty finite Subset of T is empty & the non empty finite Subset of T is compact ) ; ::_thesis: verum end; end; registration cluster empty -> T_2 for TopStruct ; coherence for b1 being TopStruct st b1 is empty holds b1 is T_2 proof let T be TopStruct ; ::_thesis: ( T is empty implies T is T_2 ) assume A1: T is empty ; ::_thesis: T is T_2 let p, q be Point of T; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) thus ( p = q or ex b1, b2 being Element of bool the carrier of T st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) by A1, STRUCT_0:def_10; ::_thesis: verum end; end; registration let T be T_2 TopStruct ; cluster -> T_2 for SubSpace of T; coherence for b1 being SubSpace of T holds b1 is T_2 proof let A be SubSpace of T; ::_thesis: A is T_2 percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: A is T_2 hence A is T_2 ; ::_thesis: verum end; supposeA1: not A is empty ; ::_thesis: A is T_2 let p, q be Point of A; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of A st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) ) assume A2: not p = q ; ::_thesis: ex b1, b2 being Element of bool the carrier of A st ( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) [#] A c= [#] T by PRE_TOPC:def_4; then not T is empty by A1; then reconsider p9 = p, q9 = q as Point of T by A1, PRE_TOPC:25; consider W, V being Subset of T such that A3: W is open and A4: V is open and A5: p9 in W and A6: q9 in V and A7: W misses V by A2, PRE_TOPC:def_10; reconsider W9 = W /\ ([#] A), V9 = V /\ ([#] A) as Subset of A ; V in the topology of T by A4, PRE_TOPC:def_2; then A8: V9 in the topology of A by PRE_TOPC:def_4; take W9 ; ::_thesis: ex b1 being Element of bool the carrier of A st ( W9 is open & b1 is open & p in W9 & q in b1 & W9 misses b1 ) take V9 ; ::_thesis: ( W9 is open & V9 is open & p in W9 & q in V9 & W9 misses V9 ) W in the topology of T by A3, PRE_TOPC:def_2; then W9 in the topology of A by PRE_TOPC:def_4; hence ( W9 is open & V9 is open ) by A8, PRE_TOPC:def_2; ::_thesis: ( p in W9 & q in V9 & W9 misses V9 ) thus ( p in W9 & q in V9 ) by A1, A5, A6, XBOOLE_0:def_4; ::_thesis: W9 misses V9 A9: W /\ V = {} by A7, XBOOLE_0:def_7; W9 /\ V9 = (W /\ (V /\ ([#] A))) /\ ([#] A) by XBOOLE_1:16 .= {} /\ ([#] A) by A9, XBOOLE_1:16 .= {} ; hence W9 misses V9 by XBOOLE_0:def_7; ::_thesis: verum end; end; end; end; theorem Th19: :: COMPTS_1:19 for X being TopStruct for Y being SubSpace of X for A being Subset of X for B being Subset of Y st A = B holds ( A is compact iff B is compact ) proof let X be TopStruct ; ::_thesis: for Y being SubSpace of X for A being Subset of X for B being Subset of Y st A = B holds ( A is compact iff B is compact ) let Y be SubSpace of X; ::_thesis: for A being Subset of X for B being Subset of Y st A = B holds ( A is compact iff B is compact ) let A be Subset of X; ::_thesis: for B being Subset of Y st A = B holds ( A is compact iff B is compact ) let B be Subset of Y; ::_thesis: ( A = B implies ( A is compact iff B is compact ) ) assume A1: A = B ; ::_thesis: ( A is compact iff B is compact ) A2: B c= [#] Y ; hence ( A is compact implies B is compact ) by A1, Th2; ::_thesis: ( B is compact implies A is compact ) assume B is compact ; ::_thesis: A is compact then for P being Subset of Y st P = A holds P is compact by A1; hence A is compact by A1, A2, Th2; ::_thesis: verum end; theorem :: COMPTS_1:20 for T, S being non empty TopSpace for p being Point of T for T1, T2 being SubSpace of T for f being Function of T1,S for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds f +* g is continuous Function of T,S proof let T, S be non empty TopSpace; ::_thesis: for p being Point of T for T1, T2 being SubSpace of T for f being Function of T1,S for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds f +* g is continuous Function of T,S let p be Point of T; ::_thesis: for T1, T2 being SubSpace of T for f being Function of T1,S for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds f +* g is continuous Function of T,S let T1, T2 be SubSpace of T; ::_thesis: for f being Function of T1,S for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds f +* g is continuous Function of T,S let f be Function of T1,S; ::_thesis: for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p holds f +* g is continuous Function of T,S let g be Function of T2,S; ::_thesis: ( ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p = g . p implies f +* g is continuous Function of T,S ) assume that A1: ([#] T1) \/ ([#] T2) = [#] T and A2: ([#] T1) /\ ([#] T2) = {p} and A3: T1 is compact and A4: T2 is compact and A5: T is T_2 and A6: f is continuous and A7: g is continuous and A8: f . p = g . p ; ::_thesis: f +* g is continuous Function of T,S set h = f +* g; A9: dom g = [#] T2 by FUNCT_2:def_1; rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; then A10: rng (f +* g) c= the carrier of S by XBOOLE_1:1; A11: dom f = [#] T1 by FUNCT_2:def_1; then dom (f +* g) = the carrier of T by A1, A9, FUNCT_4:def_1; then reconsider h = f +* g as Function of T,S by A10, FUNCT_2:def_1, RELSET_1:4; for P being Subset of S st P is closed holds h " P is closed proof let P be Subset of S; ::_thesis: ( P is closed implies h " P is closed ) [#] T1 c= [#] T by A1, XBOOLE_1:7; then reconsider P1 = f " P as Subset of T by XBOOLE_1:1; [#] T2 c= [#] T by A1, XBOOLE_1:7; then reconsider P2 = g " P as Subset of T by XBOOLE_1:1; A12: dom h = (dom f) \/ (dom g) by FUNCT_4:def_1; A13: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(h_"_P)_/\_([#]_T2)_implies_x_in_g_"_P_)_&_(_x_in_g_"_P_implies_x_in_(h_"_P)_/\_([#]_T2)_)_) let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) ) thus ( x in (h " P) /\ ([#] T2) implies x in g " P ) ::_thesis: ( x in g " P implies x in (h " P) /\ ([#] T2) ) proof assume A14: x in (h " P) /\ ([#] T2) ; ::_thesis: x in g " P then x in h " P by XBOOLE_0:def_4; then A15: h . x in P by FUNCT_1:def_7; g . x = h . x by A9, A14, FUNCT_4:13; hence x in g " P by A9, A14, A15, FUNCT_1:def_7; ::_thesis: verum end; assume A16: x in g " P ; ::_thesis: x in (h " P) /\ ([#] T2) then A17: x in dom g by FUNCT_1:def_7; g . x in P by A16, FUNCT_1:def_7; then A18: h . x in P by A17, FUNCT_4:13; x in dom h by A12, A17, XBOOLE_0:def_3; then x in h " P by A18, FUNCT_1:def_7; hence x in (h " P) /\ ([#] T2) by A16, XBOOLE_0:def_4; ::_thesis: verum end; A19: for x being set st x in [#] T1 holds h . x = f . x proof let x be set ; ::_thesis: ( x in [#] T1 implies h . x = f . x ) assume A20: x in [#] T1 ; ::_thesis: h . x = f . x now__::_thesis:_h_._x_=_f_._x percases ( x in [#] T2 or not x in [#] T2 ) ; supposeA21: x in [#] T2 ; ::_thesis: h . x = f . x then x in ([#] T1) /\ ([#] T2) by A20, XBOOLE_0:def_4; then x = p by A2, TARSKI:def_1; hence h . x = f . x by A8, A9, A21, FUNCT_4:13; ::_thesis: verum end; suppose not x in [#] T2 ; ::_thesis: h . x = f . x hence h . x = f . x by A9, FUNCT_4:11; ::_thesis: verum end; end; end; hence h . x = f . x ; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(h_"_P)_/\_([#]_T1)_implies_x_in_f_"_P_)_&_(_x_in_f_"_P_implies_x_in_(h_"_P)_/\_([#]_T1)_)_) let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) ) thus ( x in (h " P) /\ ([#] T1) implies x in f " P ) ::_thesis: ( x in f " P implies x in (h " P) /\ ([#] T1) ) proof assume A22: x in (h " P) /\ ([#] T1) ; ::_thesis: x in f " P then x in h " P by XBOOLE_0:def_4; then A23: h . x in P by FUNCT_1:def_7; f . x = h . x by A19, A22; hence x in f " P by A11, A22, A23, FUNCT_1:def_7; ::_thesis: verum end; assume A24: x in f " P ; ::_thesis: x in (h " P) /\ ([#] T1) then x in dom f by FUNCT_1:def_7; then A25: x in dom h by A12, XBOOLE_0:def_3; f . x in P by A24, FUNCT_1:def_7; then h . x in P by A19, A24; then x in h " P by A25, FUNCT_1:def_7; hence x in (h " P) /\ ([#] T1) by A24, XBOOLE_0:def_4; ::_thesis: verum end; then A26: (h " P) /\ ([#] T1) = f " P by TARSKI:1; assume A27: P is closed ; ::_thesis: h " P is closed then f " P is closed by A6, PRE_TOPC:def_6; then f " P is compact by A3, Th8; then A28: P1 is compact by Th19; g " P is closed by A7, A27, PRE_TOPC:def_6; then g " P is compact by A4, Th8; then A29: P2 is compact by Th19; h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A11, A9, A12, RELAT_1:132, XBOOLE_1:28 .= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ; then h " P = (f " P) \/ (g " P) by A26, A13, TARSKI:1; hence h " P is closed by A5, A28, A29; ::_thesis: verum end; hence f +* g is continuous Function of T,S by PRE_TOPC:def_6; ::_thesis: verum end; theorem :: COMPTS_1:21 for S, T being non empty TopSpace for T1, T2 being SubSpace of T for p1, p2 being Point of T for f being Function of T1,S for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds f +* g is continuous Function of T,S proof let S, T be non empty TopSpace; ::_thesis: for T1, T2 being SubSpace of T for p1, p2 being Point of T for f being Function of T1,S for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds f +* g is continuous Function of T,S let T1, T2 be SubSpace of T; ::_thesis: for p1, p2 being Point of T for f being Function of T1,S for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds f +* g is continuous Function of T,S let p1, p2 be Point of T; ::_thesis: for f being Function of T1,S for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds f +* g is continuous Function of T,S let f be Function of T1,S; ::_thesis: for g being Function of T2,S st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 holds f +* g is continuous Function of T,S let g be Function of T2,S; ::_thesis: ( ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = {p1,p2} & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & f . p1 = g . p1 & f . p2 = g . p2 implies f +* g is continuous Function of T,S ) assume that A1: ([#] T1) \/ ([#] T2) = [#] T and A2: ([#] T1) /\ ([#] T2) = {p1,p2} and A3: T1 is compact and A4: T2 is compact and A5: T is T_2 and A6: f is continuous and A7: g is continuous and A8: f . p1 = g . p1 and A9: f . p2 = g . p2 ; ::_thesis: f +* g is continuous Function of T,S set h = f +* g; A10: dom g = [#] T2 by FUNCT_2:def_1; rng (f +* g) c= (rng f) \/ (rng g) by FUNCT_4:17; then A11: rng (f +* g) c= the carrier of S by XBOOLE_1:1; A12: dom f = [#] T1 by FUNCT_2:def_1; then dom (f +* g) = the carrier of T by A1, A10, FUNCT_4:def_1; then reconsider h = f +* g as Function of T,S by A11, FUNCT_2:def_1, RELSET_1:4; for P being Subset of S st P is closed holds h " P is closed proof let P be Subset of S; ::_thesis: ( P is closed implies h " P is closed ) [#] T1 c= [#] T by A1, XBOOLE_1:7; then reconsider P1 = f " P as Subset of T by XBOOLE_1:1; [#] T2 c= [#] T by A1, XBOOLE_1:7; then reconsider P2 = g " P as Subset of T by XBOOLE_1:1; A13: dom h = (dom f) \/ (dom g) by FUNCT_4:def_1; A14: now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(h_"_P)_/\_([#]_T2)_implies_x_in_g_"_P_)_&_(_x_in_g_"_P_implies_x_in_(h_"_P)_/\_([#]_T2)_)_) let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T2) implies x in g " P ) & ( x in g " P implies x in (h " P) /\ ([#] T2) ) ) thus ( x in (h " P) /\ ([#] T2) implies x in g " P ) ::_thesis: ( x in g " P implies x in (h " P) /\ ([#] T2) ) proof assume A15: x in (h " P) /\ ([#] T2) ; ::_thesis: x in g " P then x in h " P by XBOOLE_0:def_4; then A16: h . x in P by FUNCT_1:def_7; g . x = h . x by A10, A15, FUNCT_4:13; hence x in g " P by A10, A15, A16, FUNCT_1:def_7; ::_thesis: verum end; assume A17: x in g " P ; ::_thesis: x in (h " P) /\ ([#] T2) then A18: x in dom g by FUNCT_1:def_7; g . x in P by A17, FUNCT_1:def_7; then A19: h . x in P by A18, FUNCT_4:13; x in dom h by A13, A18, XBOOLE_0:def_3; then x in h " P by A19, FUNCT_1:def_7; hence x in (h " P) /\ ([#] T2) by A17, XBOOLE_0:def_4; ::_thesis: verum end; A20: for x being set st x in [#] T1 holds h . x = f . x proof let x be set ; ::_thesis: ( x in [#] T1 implies h . x = f . x ) assume A21: x in [#] T1 ; ::_thesis: h . x = f . x now__::_thesis:_h_._x_=_f_._x percases ( x in [#] T2 or not x in [#] T2 ) ; supposeA22: x in [#] T2 ; ::_thesis: h . x = f . x then A23: x in ([#] T1) /\ ([#] T2) by A21, XBOOLE_0:def_4; now__::_thesis:_h_._x_=_f_._x percases ( x = p1 or x = p2 ) by A2, A23, TARSKI:def_2; suppose x = p1 ; ::_thesis: h . x = f . x hence h . x = f . x by A8, A10, A22, FUNCT_4:13; ::_thesis: verum end; suppose x = p2 ; ::_thesis: h . x = f . x hence h . x = f . x by A9, A10, A22, FUNCT_4:13; ::_thesis: verum end; end; end; hence h . x = f . x ; ::_thesis: verum end; suppose not x in [#] T2 ; ::_thesis: h . x = f . x hence h . x = f . x by A10, FUNCT_4:11; ::_thesis: verum end; end; end; hence h . x = f . x ; ::_thesis: verum end; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(h_"_P)_/\_([#]_T1)_implies_x_in_f_"_P_)_&_(_x_in_f_"_P_implies_x_in_(h_"_P)_/\_([#]_T1)_)_) let x be set ; ::_thesis: ( ( x in (h " P) /\ ([#] T1) implies x in f " P ) & ( x in f " P implies x in (h " P) /\ ([#] T1) ) ) thus ( x in (h " P) /\ ([#] T1) implies x in f " P ) ::_thesis: ( x in f " P implies x in (h " P) /\ ([#] T1) ) proof assume A24: x in (h " P) /\ ([#] T1) ; ::_thesis: x in f " P then x in h " P by XBOOLE_0:def_4; then A25: h . x in P by FUNCT_1:def_7; f . x = h . x by A20, A24; hence x in f " P by A12, A24, A25, FUNCT_1:def_7; ::_thesis: verum end; assume A26: x in f " P ; ::_thesis: x in (h " P) /\ ([#] T1) then x in dom f by FUNCT_1:def_7; then A27: x in dom h by A13, XBOOLE_0:def_3; f . x in P by A26, FUNCT_1:def_7; then h . x in P by A20, A26; then x in h " P by A27, FUNCT_1:def_7; hence x in (h " P) /\ ([#] T1) by A26, XBOOLE_0:def_4; ::_thesis: verum end; then A28: (h " P) /\ ([#] T1) = f " P by TARSKI:1; assume A29: P is closed ; ::_thesis: h " P is closed then f " P is closed by A6, PRE_TOPC:def_6; then f " P is compact by A3, Th8; then A30: P1 is compact by Th19; g " P is closed by A7, A29, PRE_TOPC:def_6; then g " P is compact by A4, Th8; then A31: P2 is compact by Th19; h " P = (h " P) /\ (([#] T1) \/ ([#] T2)) by A12, A10, A13, RELAT_1:132, XBOOLE_1:28 .= ((h " P) /\ ([#] T1)) \/ ((h " P) /\ ([#] T2)) by XBOOLE_1:23 ; then h " P = (f " P) \/ (g " P) by A28, A14, TARSKI:1; hence h " P is closed by A5, A30, A31; ::_thesis: verum end; hence f +* g is continuous Function of T,S by PRE_TOPC:def_6; ::_thesis: verum end; begin registration let S be TopStruct ; cluster the topology of S -> open ; coherence the topology of S is open proof let P be Subset of S; :: according to TOPS_2:def_1 ::_thesis: ( not P in the topology of S or P is open ) thus ( not P in the topology of S or P is open ) by PRE_TOPC:def_2; ::_thesis: verum end; end; registration let T be TopSpace; cluster non empty open for Element of bool (bool the carrier of T); existence ex b1 being Subset-Family of T st ( b1 is open & not b1 is empty ) proof take the topology of T ; ::_thesis: ( the topology of T is open & not the topology of T is empty ) thus ( the topology of T is open & not the topology of T is empty ) ; ::_thesis: verum end; end; theorem Th22: :: COMPTS_1:22 for T being non empty TopSpace for F being set holds ( F is open Subset-Family of T iff F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ) proof let T be non empty TopSpace; ::_thesis: for F being set holds ( F is open Subset-Family of T iff F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ) let F be set ; ::_thesis: ( F is open Subset-Family of T iff F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ) thus ( F is open Subset-Family of T implies F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ) ::_thesis: ( F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) implies F is open Subset-Family of T ) proof assume A1: F is open Subset-Family of T ; ::_thesis: F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) then reconsider F = F as Subset-Family of TopStruct(# the carrier of T, the topology of T #) ; F is open proof let P be Subset of TopStruct(# the carrier of T, the topology of T #); :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open ) assume P in F ; ::_thesis: P is open then P is open Subset of T by A1, TOPS_2:def_1; hence P is open by PRE_TOPC:30; ::_thesis: verum end; hence F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: verum end; assume A2: F is open Subset-Family of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: F is open Subset-Family of T then reconsider F = F as Subset-Family of T ; F is open proof let P be Subset of T; :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open ) assume P in F ; ::_thesis: P is open then P is open Subset of TopStruct(# the carrier of T, the topology of T #) by A2, TOPS_2:def_1; hence P is open by PRE_TOPC:30; ::_thesis: verum end; hence F is open Subset-Family of T ; ::_thesis: verum end; theorem :: COMPTS_1:23 for T being non empty TopSpace for X being set holds ( X is compact Subset of T iff X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ) proof let T be non empty TopSpace; ::_thesis: for X being set holds ( X is compact Subset of T iff X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ) let X be set ; ::_thesis: ( X is compact Subset of T iff X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ) thus ( X is compact Subset of T implies X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ) ::_thesis: ( X is compact Subset of TopStruct(# the carrier of T, the topology of T #) implies X is compact Subset of T ) proof assume A1: X is compact Subset of T ; ::_thesis: X is compact Subset of TopStruct(# the carrier of T, the topology of T #) then reconsider Z = X as Subset of TopStruct(# the carrier of T, the topology of T #) ; Z is compact proof let F be Subset-Family of TopStruct(# the carrier of T, the topology of T #); :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of Z & F is open implies ex G being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st ( G c= F & G is Cover of Z & G is finite ) ) assume that A2: F is Cover of Z and A3: F is open ; ::_thesis: ex G being Subset-Family of TopStruct(# the carrier of T, the topology of T #) st ( G c= F & G is Cover of Z & G is finite ) reconsider FF = F as Subset-Family of T ; FF is open by A3, Th22; then consider G being Subset-Family of TopStruct(# the carrier of T, the topology of T #) such that A4: G c= FF and A5: G is Cover of X and A6: G is finite by A1, A2, Def4; take G ; ::_thesis: ( G c= F & G is Cover of Z & G is finite ) thus ( G c= F & G is Cover of Z & G is finite ) by A4, A5, A6; ::_thesis: verum end; hence X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: verum end; assume A7: X is compact Subset of TopStruct(# the carrier of T, the topology of T #) ; ::_thesis: X is compact Subset of T then reconsider Z = X as Subset of T ; Z is compact proof let F be Subset-Family of T; :: according to COMPTS_1:def_4 ::_thesis: ( F is Cover of Z & F is open implies ex G being Subset-Family of T st ( G c= F & G is Cover of Z & G is finite ) ) assume that A8: F is Cover of Z and A9: F is open ; ::_thesis: ex G being Subset-Family of T st ( G c= F & G is Cover of Z & G is finite ) reconsider FF = F as Subset-Family of TopStruct(# the carrier of T, the topology of T #) ; FF is open by A9, Th22; then consider G being Subset-Family of T such that A10: G c= FF and A11: G is Cover of X and A12: G is finite by A7, A8, Def4; take G ; ::_thesis: ( G c= F & G is Cover of Z & G is finite ) thus ( G c= F & G is Cover of Z & G is finite ) by A10, A11, A12; ::_thesis: verum end; hence X is compact Subset of T ; ::_thesis: verum end;