:: by Agata Darmochwa{\l}

::

:: Received September 19, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

let T be TopStruct ;

end;
attr T 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 );

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

:: 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 ) );

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;

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

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

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

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

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

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

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

definition

let T be TopStruct ;

let P be Subset of T;

end;
let P be Subset of T;

attr P 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 );

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

:: 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 ) );

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 ;

coherence

for b_{1} being Subset of T st b_{1} is empty holds

b_{1} is compact

end;
coherence

for b

b

proof 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 )

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 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 ) ) )

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 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 <> {} )

( T is compact iff for F being Subset-Family of T st F is centered & F is closed holds

meet F <> {} )

proof 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 = {} ) )

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

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

for PS, QS being Subset of TS st PS is compact & QS c= PS & QS is closed holds

QS is compact

proof 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

for P, Q being Subset of T st P is compact & Q is compact holds

P \/ Q is compact

proof 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

for PS, QS being Subset of TS st TS is T_2 & PS is compact & QS is compact holds

PS /\ QS is compact

proof 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

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

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

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

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

:: deftheorem defines 1TopSp COMPTS_1:def 5 :

for D being set holds 1TopSp D = TopStruct(# D,([#] (bool D)) #);

for D being set holds 1TopSp D = TopStruct(# D,([#] (bool D)) #);

registration
end;

registration
end;

registration
end;

registration
end;

registration

let T be non empty T_2 TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is compact holds

b_{1} is closed
by Th7;

end;
coherence

for b

b

registration

existence

ex b_{1} being TopSpace st

( not b_{1} is empty & b_{1} is finite & b_{1} is strict )

end;
ex b

( not b

proof end;

registration
end;

registration

let T be TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is finite holds

b_{1} is compact

end;
coherence

for b

b

proof end;

registration

let T be non empty TopSpace;

existence

ex b_{1} being Subset of T st

( not b_{1} is empty & b_{1} is compact )

end;
existence

ex b

( not b

proof end;

:: comp. TOPMETR:3, 2008.07.06, A.T.

registration
end;

registration
end;

:: from BORSUK_1, 2008.07.07, A.T.

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 )

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

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

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

begin

:: TOPGEN_2, A.T. 2009.03.15

registration

let T be TopSpace;

existence

ex b_{1} being Subset-Family of T st

( b_{1} is open & not b_{1} is empty )

end;
existence

ex b

( b

proof 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 #) )

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 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 #) )

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