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