:: Compact Spaces
:: by Agata Darmochwa{\l}
::
:: Received September 19, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies PRE_TOPC, SUBSET_1, RCOMP_1, SETFAM_1, TARSKI, FINSET_1,
XBOOLE_0, CARD_5, RELAT_1, ZFMISC_1, FUNCT_1, STRUCT_0, ORDINAL2, TOPS_2,
FUNCT_4, COMPTS_1, PARTFUN1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_3, SETFAM_1, FINSET_1, DOMAIN_1, FUNCT_4, STRUCT_0,
PRE_TOPC, TOPS_2;
constructors SETFAM_1, DOMAIN_1, FUNCT_3, FINSET_1, TOPS_2, FUNCT_4, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, STRUCT_0, PRE_TOPC,
TOPS_1;
requirements SUBSET, BOOLE;
begin
reserve x, y, z for set,
T for TopStruct,
A for SubSpace of T,
P, Q for Subset of T;
definition
let T be TopStruct;
attr T is compact means
:: COMPTS_1:def 1
for F being Subset-Family of T st F is Cover
of T & F is open ex G being Subset-Family of T st G c= F & G is Cover of T & G
is finite;
end;
definition
let T be non empty TopSpace;
redefine attr T is regular means
:: COMPTS_1:def 2
for p being Point of T, P being Subset of T
st P <> {} & P is closed & p in P` ex W, V being Subset of T st W is open & V
is open & p in W & P c= V & W misses V;
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 ex P, Q being Subset of T st P is
open & Q is open & W c= P & V c= Q & P misses Q;
end;
notation
let T be TopStruct;
synonym T is Hausdorff for T is T_2;
end;
definition
let T be TopStruct, P be Subset of T;
attr P is compact means
:: COMPTS_1:def 4
for F being Subset-Family of T st F is Cover
of P & F is open ex G being Subset-Family of T st G c= F & G is Cover of P & G
is finite;
end;
registration
let T;
cluster empty -> compact for Subset of T;
end;
theorem :: COMPTS_1:1
T is compact iff [#]T is compact;
theorem :: COMPTS_1:2
Q c= [#] A implies (Q is compact iff for P being Subset of A st
P=Q holds P is compact );
theorem :: COMPTS_1:3
( P = {} implies (P is compact iff T|P is compact) ) & ( T is
TopSpace-like & P <> {} implies (P is compact iff T|P is compact) );
theorem :: 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 <> {};
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 = {} ex G being
Subset-Family of T st G <> {} & G c= F & G is finite & meet G = {};
reserve TS for TopSpace;
reserve PS, QS for Subset of TS;
theorem :: COMPTS_1:6
TS is T_2 implies for A being Subset of TS st A <> {} & A is
compact for p being Point of TS st p in A` ex PS,QS st PS is open & QS is open
& p in PS & A c= QS & PS misses QS;
theorem :: COMPTS_1:7
TS is T_2 & PS is compact implies PS is closed;
theorem :: COMPTS_1:8
T is compact & P is closed implies P is compact;
theorem :: COMPTS_1:9
PS is compact & QS c= PS & QS is closed implies QS is compact;
theorem :: COMPTS_1:10
P is compact & Q is compact implies P \/ Q is compact;
theorem :: COMPTS_1:11
TS is T_2 & PS is compact & QS is compact implies PS /\ QS is compact;
theorem :: COMPTS_1:12
for TS being non empty TopSpace holds TS is T_2 & TS is compact
implies TS is regular;
theorem :: COMPTS_1:13
for TS being non empty TopSpace holds TS is T_2 & TS is compact
implies TS is normal;
reserve S for non empty TopStruct;
reserve f for Function of T,S;
theorem :: COMPTS_1:14
T is compact & f is continuous & rng f = [#] S implies S is compact;
theorem :: COMPTS_1:15
f is continuous & rng f = [#] S & P is compact implies f.:P is compact;
reserve SS for non empty TopSpace;
reserve f for Function of TS,SS;
theorem :: COMPTS_1:16
TS is compact & SS is T_2 & rng f = [#] SS & f is continuous
implies for PS st PS is closed holds f.:PS is closed;
theorem :: COMPTS_1:17
TS is compact & SS is T_2 & rng f = [#]SS & f is
one-to-one & f is continuous implies f is being_homeomorphism;
definition
let D be set;
func 1TopSp D -> TopStruct equals
:: COMPTS_1:def 5
TopStruct (# D, [#] bool D #);
end;
registration
let D be set;
cluster 1TopSp D -> strict TopSpace-like;
end;
registration
let D be non empty set;
cluster 1TopSp D -> non empty;
end;
registration
let x be set;
cluster 1TopSp {x} -> T_2;
end;
registration
cluster T_2 non empty for TopSpace;
end;
registration
let T be T_2 non empty TopSpace;
cluster compact -> closed for Subset of T;
end;
registration
let A be finite set;
cluster 1TopSp A -> finite;
end;
registration
cluster non empty finite strict for TopSpace;
end;
registration
cluster finite -> compact for TopSpace;
end;
theorem :: COMPTS_1:18
for T being TopSpace st the carrier of T is finite holds T is compact;
registration
let T be TopSpace;
cluster finite -> compact for Subset of T;
end;
registration
let T be non empty TopSpace;
cluster non empty compact for Subset of T;
end;
:: comp. TOPMETR:3, 2008.07.06, A.T.
registration
cluster empty -> T_2 for TopStruct;
end;
registration
let T be T_2 TopStruct;
cluster -> T_2 for SubSpace of T;
end;
:: from BORSUK_1, 2008.07.07, A.T.
theorem :: COMPTS_1:19
for X being TopStruct for Y being SubSpace of X, A being Subset
of X, B being Subset of Y st A = B holds A is compact iff B is compact;
:: from TOPMETR2, 2008.07.07, A.T.
reserve T, S for non empty TopSpace,
p for Point of T;
theorem :: COMPTS_1:20
for T1,T2 being SubSpace of T,
f being Function of T1,S, 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;
theorem :: COMPTS_1:21
for T being non empty TopSpace, T1, T2 being SubSpace of T,
p1,p2 being Point of T
for f being Function of T1,S, 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;
begin :: Addenda, the 2009.03 revision, A.T.
registration
let S be TopStruct;
cluster the topology of S -> open;
end;
:: TOPGEN_2, A.T. 2009.03.15
registration
let T be TopSpace;
cluster open non empty for Subset-Family of T;
end;
theorem :: COMPTS_1:22
for T being non empty TopSpace, F being set holds F is open
Subset-Family of T iff F is open Subset-Family of the TopStruct of T;
theorem :: COMPTS_1:23
for T being non empty TopSpace, X being set holds
X is compact Subset of T iff X is compact Subset of the TopStruct of T;
theorem :: COMPTS_1:24
for X being set
for T1,T2 being SubSpace of T,
f being Function of T1,S, g being Function of T2,S
st ([#] T1) \/ ([#] T2) = [#] T & ([#] T1) /\ ([#] T2) = X &
T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous
& f|X tolerates g|X holds f+*g is continuous Function of T,S;