Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Compact Spaces

**by****Agata Darmochwal**- Received September 19, 1989
- MML identifier: COMPTS_1

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, BOOLE, MCART_1, FINSET_1, ORDERS_1, TARSKI, PRE_TOPC, SETFAM_1, SUBSET_1, ORDINAL2, TOPS_2, COMPTS_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, SETFAM_1, FINSET_1, ORDERS_1, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2; constructors FUNCT_3, FINSET_1, ORDERS_1, DOMAIN_1, TOPS_2, MEMBERED; clusters FUNCT_1, PRE_TOPC, STRUCT_0, RELSET_1, SUBSET_1, FINSET_1, MEMBERED, ZFMISC_1; requirements SUBSET, BOOLE; begin reserve x, y, z, X, Y, Z for set; reserve f for Function; scheme NonUniqBoundFuncEx { X() -> set, Y() -> set, P[set,set] }: ex f being Function st dom f = X() & rng f c= Y() & for x st x in X() holds P[x,f.x] provided for x st x in X() ex y st y in Y() & P[x,y]; scheme BiFuncEx{A()->set,B()->set,C()->set,P[set,set,set]}: ex f,g being Function st dom f = A() & dom g = A() & for x st x in A() holds P[x,f.x,g.x] provided x in A() implies ex y,z st y in B() & z in C() & P[x,y,z]; theorem :: COMPTS_1:1 Z is finite & Z c= rng f implies ex Y st Y c= dom f & Y is finite & f.:Y = Z; reserve T for TopStruct; reserve A for SubSpace of T; reserve P, Q for Subset of T; definition let T be 1-sorted, F be Subset-Family of T, P be Subset of T; pred F is_a_cover_of P means :: COMPTS_1:def 1 P c= union F; end; definition let F be set; attr F is centered means :: COMPTS_1:def 2 F <> {} & for G being set st G <> {} & G c= F & G is finite holds meet G <> {}; end; definition let T be TopStruct; attr T is compact means :: COMPTS_1:def 3 for F being Subset-Family of T st F is_a_cover_of T & F is open ex G being Subset-Family of T st G c= F & G is_a_cover_of T & G is finite; attr T is being_T2 means :: COMPTS_1:def 4 for p, q being Point of T st not p = q ex W, V being Subset of T st W is open & V is open & p in W & q in V & W misses V; synonym T is_T2; attr T is being_T3 means :: COMPTS_1:def 5 for p being Point of T, P being Subset of T st P <> {} & P is closed & not 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; synonym T is_T3; attr T is being_T4 means :: COMPTS_1:def 6 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; synonym T is_T4; end; definition let T be TopStruct, P be Subset of T; attr P is compact means :: COMPTS_1:def 7 for F being Subset-Family of T st F is_a_cover_of P & F is open ex G being Subset-Family of T st G c= F & G is_a_cover_of P & G is finite; end; canceled 7; theorem :: COMPTS_1:9 {}T is compact; theorem :: COMPTS_1:10 T is compact iff [#]T is compact; theorem :: COMPTS_1:11 Q c= [#] A implies (Q is compact iff (for P being Subset of A st P=Q holds P is compact)); theorem :: COMPTS_1:12 ( 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:13 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:14 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:15 TS is_T2 implies for A being Subset of TS st A <> {} & A is compact for p being Point of TS st not 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:16 TS is_T2 & PS is compact implies PS is closed; theorem :: COMPTS_1:17 T is compact & P is closed implies P is compact; theorem :: COMPTS_1:18 PS is compact & QS c= PS & QS is closed implies QS is compact; theorem :: COMPTS_1:19 P is compact & Q is compact implies P \/ Q is compact; theorem :: COMPTS_1:20 TS is_T2 & PS is compact & QS is compact implies PS /\ QS is compact; theorem :: COMPTS_1:21 TS is_T2 & TS is compact implies TS is_T3; theorem :: COMPTS_1:22 TS is_T2 & TS is compact implies TS is_T4; reserve S for non empty TopStruct; reserve f for map of T,S; theorem :: COMPTS_1:23 T is compact & f is continuous & rng f = [#] S implies S is compact; theorem :: COMPTS_1:24 f is continuous & rng f = [#] S & P is compact implies f.:P is compact; reserve SS for non empty TopSpace; reserve f for map of TS,SS; theorem :: COMPTS_1:25 TS is compact & SS is_T2 & rng f = [#] SS & f is continuous implies for PS st PS is closed holds f.:PS is closed; theorem :: COMPTS_1:26 TS is compact & SS is_T2 & dom f = [#]TS & rng f = [#]SS & f is one-to-one & f is continuous implies f is_homeomorphism;

Back to top