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 )

P is compact ) implies Q is compact ) :: thesis: verum

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

thus
( ( for P being Subset of A st P = Q holds
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

end;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;

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;

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;( 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;

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;

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

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

end;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

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;

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

end;( 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

Q c= union F
by A14, SETFAM_1:def 11;
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;

then R in the topology of T ;

then X in the topology of A by A22, PRE_TOPC:def 4;

hence X is open ; :: thesis: verum

end;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;

then R in the topology of T ;

then X in the topology of A by A22, PRE_TOPC:def 4;

hence X is open ; :: thesis: verum

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;

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

hence
( G9 c= F & G9 is Cover of Q & G9 is finite )
by A16, A26, A27, SETFAM_1:def 11; :: thesis: verum
let x be object ; :: 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 object 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;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 object 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