Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

### Compactness of the Bounded Closed Subsets of $\cal E^2_\rm T$

**by****Artur Kornilowicz**- Received February 19, 1999
- MML identifier: TOPREAL6

- [ Mizar article, MML identifier index ]

environ vocabulary ARYTM, METRIC_1, PRE_TOPC, EUCLID, SQUARE_1, ARYTM_1, ARYTM_3, RELAT_1, ABSVALUE, FINSEQ_2, FINSEQ_1, FUNCT_1, GROUP_1, RVSUM_1, RCOMP_1, ORDINAL2, SEQ_2, LATTICES, FINSET_1, PCOMPS_1, RELAT_2, SUBSET_1, BOOLE, CONNSP_1, COMPTS_1, T_0TOPSP, TOPS_2, SETFAM_1, TARSKI, CARD_3, FUNCOP_1, CAT_1, COMPLEX1, RLVECT_1, MCART_1, TOPREAL1, PSCOMP_1, JORDAN1, SPPOL_1, TOPREAL4, TOPREAL2, SPRECT_1, FUNCT_5, JORDAN2C, SEQ_1, TOPMETR, CONNSP_2, TOPS_1, BORSUK_1, PARTFUN1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_3, BINOP_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, SQUARE_1, NAT_1, ABSVALUE, BINARITH, CQC_LANG, FUNCT_4, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, GROUP_1, METRIC_1, TBSP_1, FINSEQ_1, FINSEQ_2, RVSUM_1, NEWTON, CARD_3, FINSEQ_4, RCOMP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, CONNSP_2, COMPTS_1, BORSUK_1, PCOMPS_1, EUCLID, WEIERSTR, TOPMETR, TOPREAL1, TOPREAL2, T_0TOPSP, JORDAN1, TOPREAL4, PSCOMP_1, SPPOL_1, JGRAPH_1, SPRECT_1, JORDAN2C; constructors BINARITH, BORSUK_3, CARD_4, COMPTS_1, CONNSP_1, FINSEQOP, FINSEQ_4, GOBOARD9, JORDAN1, JORDAN2C, LIMFUNC1, PSCOMP_1, RCOMP_1, REAL_1, REALSET1, SPPOL_1, SPRECT_1, TBSP_1, TOPGRP_1, TOPREAL2, TOPREAL4, TOPS_1, TOPS_2, WAYBEL_3, WEIERSTR, CQC_LANG, TOPRNS_1, MEMBERED, PARTFUN1; clusters SUBSET_1, XREAL_0, BORSUK_1, BORSUK_3, FUNCT_4, EUCLID, FINSET_1, GOBOARD9, METRIC_1, PCOMPS_1, PRE_TOPC, PSCOMP_1, RCOMP_1, RELSET_1, SPRECT_1, SPRECT_2, STRUCT_0, TEX_4, TOPGRP_1, TOPMETR, TOPS_1, WAYBEL_2, WAYBEL12, YELLOW13, ARYTM_3, SQUARE_1, FINSEQ_5, MEMBERED, ZFMISC_1, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin :: Real numbers reserve a, b for real number, r for Real, i, j, n for Nat, M for non empty MetrSpace, p, q, s for Point of TOP-REAL 2, e for Point of Euclid 2, w for Point of Euclid n, z for Point of M, A, B for Subset of TOP-REAL n, P for Subset of TOP-REAL 2, D for non empty Subset of TOP-REAL 2; canceled 5; theorem :: TOPREAL6:6 0 <= a & 0 <= b implies sqrt(a+b) <= sqrt a + sqrt b; theorem :: TOPREAL6:7 0 <= a & a <= b implies abs(a) <= abs(b); theorem :: TOPREAL6:8 b <= a & a <= 0 implies abs(a) <= abs(b); theorem :: TOPREAL6:9 Product(0|->r) = 1; theorem :: TOPREAL6:10 Product(1|->r) = r; theorem :: TOPREAL6:11 Product(2|->r) = r * r; theorem :: TOPREAL6:12 Product((n+1)|->r) = (Product(n|->r))*r; theorem :: TOPREAL6:13 j <> 0 & r = 0 iff Product(j|->r) = 0; theorem :: TOPREAL6:14 r <> 0 & j <= i implies Product((i-'j)|->r) = Product(i|->r) / Product(j|->r); theorem :: TOPREAL6:15 r <> 0 & j <= i implies r|^(i-'j) = r|^i / r|^j; reserve a, b for Real; theorem :: TOPREAL6:16 sqr <*a,b*> = <*a^2,b^2*>; theorem :: TOPREAL6:17 for F being FinSequence of REAL st i in dom abs F & a = F.i holds (abs F).i = abs(a); theorem :: TOPREAL6:18 abs <*a,b*> = <*abs(a),abs(b)*>; theorem :: TOPREAL6:19 for a, b, c, d being real number st a <= b & c <= d holds abs(b-a) + abs(d-c) = (b-a) + (d-c); theorem :: TOPREAL6:20 for a, r being real number holds r > 0 implies a in ].a-r,a+r.[; theorem :: TOPREAL6:21 for a, r being real number holds r >= 0 implies a in [.a-r,a+r.]; theorem :: TOPREAL6:22 for a, b being real number holds a < b implies inf ].a,b.[ = a & sup ].a,b.[ = b; canceled; theorem :: TOPREAL6:24 for A being bounded Subset of REAL holds A c= [.inf A,sup A.]; begin :: Topological preliminaries definition let T be TopStruct, A be finite Subset of T; cluster T|A -> finite; end; definition cluster finite non empty strict TopSpace; end; definition let T be TopStruct; cluster empty -> connected Subset of T; end; definition let T be TopSpace; cluster finite -> compact Subset of T; end; theorem :: TOPREAL6:25 for S, T being TopSpace st S, T are_homeomorphic & S is connected holds T is connected; theorem :: TOPREAL6:26 for T being TopSpace, F being finite Subset-Family of T st for X being Subset of T st X in F holds X is compact holds union F is compact; begin canceled 2; theorem :: TOPREAL6:29 for A, B, C, D, a, b being set st A c= B & C c= D holds product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D)); theorem :: TOPREAL6:30 for A, B being Subset of REAL holds product ((1,2) --> (A,B)) is Subset of TOP-REAL 2; theorem :: TOPREAL6:31 |.|[0,a]|.| = abs(a) & |.|[a,0]|.| = abs(a); theorem :: TOPREAL6:32 for p being Point of Euclid 2, q being Point of TOP-REAL 2 st p = 0.REAL 2 & p = q holds q = <* 0,0 *> & q`1 = 0 & q`2 = 0; theorem :: TOPREAL6:33 for p, q being Point of Euclid 2, z being Point of TOP-REAL 2 st p = 0.REAL 2 & q = z holds dist(p,q) = |.z.|; theorem :: TOPREAL6:34 r*p = |[r*p`1,r*p`2]|; theorem :: TOPREAL6:35 s = (1-r)*p + r*q & s <> p & 0 <= r implies 0 < r; theorem :: TOPREAL6:36 s = (1-r)*p + r*q & s <> q & r <= 1 implies r < 1; theorem :: TOPREAL6:37 s in LSeg(p,q) & s <> p & s <> q & p`1 < q`1 implies p`1 < s`1 & s`1 < q`1; theorem :: TOPREAL6:38 s in LSeg(p,q) & s <> p & s <> q & p`2 < q`2 implies p`2 < s`2 & s`2 < q`2; theorem :: TOPREAL6:39 for p being Point of TOP-REAL 2 ex q being Point of TOP-REAL 2 st q`1 < W-bound D & p <> q; theorem :: TOPREAL6:40 for p being Point of TOP-REAL 2 ex q being Point of TOP-REAL 2 st q`1 > E-bound D & p <> q; theorem :: TOPREAL6:41 for p being Point of TOP-REAL 2 ex q being Point of TOP-REAL 2 st q`2 > N-bound D & p <> q; theorem :: TOPREAL6:42 for p being Point of TOP-REAL 2 ex q being Point of TOP-REAL 2 st q`2 < S-bound D & p <> q; definition cluster convex non empty -> connected Subset of TOP-REAL 2; cluster non horizontal -> non empty Subset of TOP-REAL 2; cluster non vertical -> non empty Subset of TOP-REAL 2; cluster being_Region -> open connected Subset of TOP-REAL 2; cluster open connected -> being_Region Subset of TOP-REAL 2; end; definition cluster empty -> horizontal Subset of TOP-REAL 2; cluster empty -> vertical Subset of TOP-REAL 2; end; definition cluster non empty convex Subset of TOP-REAL 2; end; definition let a, b be Point of TOP-REAL 2; cluster LSeg(a,b) -> convex connected; end; definition cluster R^2-unit_square -> connected; end; definition cluster being_simple_closed_curve -> connected compact Subset of TOP-REAL 2; end; theorem :: TOPREAL6:43 :: SPRECT_3:26 LSeg(NE-corner P,SE-corner P) c= L~SpStSeq P; theorem :: TOPREAL6:44 LSeg(SW-corner P,SE-corner P) c= L~SpStSeq P; theorem :: TOPREAL6:45 LSeg(SW-corner P,NW-corner P) c= L~SpStSeq P; theorem :: TOPREAL6:46 for C being Subset of TOP-REAL 2 holds {p where p is Point of TOP-REAL 2: p`1 < W-bound C} is non empty convex connected Subset of TOP-REAL 2; begin :: Balls as subsets of TOP-REAL n theorem :: TOPREAL6:47 e = q & p in Ball(e,r) implies q`1-r < p`1 & p`1 < q`1+r; theorem :: TOPREAL6:48 e = q & p in Ball(e,r) implies q`2-r < p`2 & p`2 < q`2+r; theorem :: TOPREAL6:49 p = e implies product ((1,2) --> (].p`1-r/sqrt 2,p`1+r/sqrt 2.[, ].p`2-r/sqrt 2,p`2+r/sqrt 2.[)) c= Ball(e,r); theorem :: TOPREAL6:50 p = e implies Ball(e,r) c= product((1,2)-->(].p`1-r,p`1+r.[,].p`2-r,p`2+r.[)); theorem :: TOPREAL6:51 P = Ball(e,r) & p = e implies proj1.:P = ].p`1-r,p`1+r.[; theorem :: TOPREAL6:52 P = Ball(e,r) & p = e implies proj2.:P = ].p`2-r,p`2+r.[; theorem :: TOPREAL6:53 D = Ball(e,r) & p = e implies W-bound D = p`1 - r; theorem :: TOPREAL6:54 D = Ball(e,r) & p = e implies E-bound D = p`1 + r; theorem :: TOPREAL6:55 D = Ball(e,r) & p = e implies S-bound D = p`2 - r; theorem :: TOPREAL6:56 D = Ball(e,r) & p = e implies N-bound D = p`2 + r; theorem :: TOPREAL6:57 D = Ball(e,r) implies D is non horizontal; theorem :: TOPREAL6:58 D = Ball(e,r) implies D is non vertical; theorem :: TOPREAL6:59 for f being Point of Euclid 2, x being Point of TOP-REAL 2 st x in Ball(f,a) holds not |[x`1-2*a,x`2]| in Ball(f,a); theorem :: TOPREAL6:60 for X being non empty compact Subset of TOP-REAL 2, p being Point of Euclid 2 st p = 0.REAL 2 & a > 0 holds X c= Ball(p, abs(E-bound X)+abs(N-bound X)+abs(W-bound X)+abs(S-bound X)+a); theorem :: TOPREAL6:61 for M being Reflexive symmetric triangle (non empty MetrStruct), z being Point of M holds r < 0 implies Sphere(z,r) = {}; theorem :: TOPREAL6:62 for M being Reflexive discerning (non empty MetrStruct), z being Point of M holds Sphere(z,0) = {z}; theorem :: TOPREAL6:63 for M being Reflexive symmetric triangle (non empty MetrStruct), z being Point of M holds r < 0 implies cl_Ball(z,r) = {}; theorem :: TOPREAL6:64 cl_Ball(z,0) = {z}; theorem :: TOPREAL6:65 for A being Subset of TopSpaceMetr M st A = cl_Ball(z,r) holds A is closed; theorem :: TOPREAL6:66 A = cl_Ball(w,r) implies A is closed; theorem :: TOPREAL6:67 cl_Ball(z,r) is bounded; theorem :: TOPREAL6:68 for A being Subset of TopSpaceMetr M st A = Sphere(z,r) holds A is closed; theorem :: TOPREAL6:69 A = Sphere(w,r) implies A is closed; theorem :: TOPREAL6:70 Sphere(z,r) is bounded; theorem :: TOPREAL6:71 A is Bounded implies Cl A is Bounded; theorem :: TOPREAL6:72 for M being non empty MetrStruct holds M is bounded iff for X being Subset of M holds X is bounded; theorem :: TOPREAL6:73 for M being Reflexive symmetric triangle (non empty MetrStruct), X, Y being Subset of M st the carrier of M = X \/ Y & M is non bounded & X is bounded holds Y is non bounded; theorem :: TOPREAL6:74 for X, Y being Subset of TOP-REAL n st n >= 1 & the carrier of TOP-REAL n = X \/ Y & X is Bounded holds Y is non Bounded; canceled; theorem :: TOPREAL6:76 A is Bounded & B is Bounded implies A \/ B is Bounded; begin :: Topological properties of real numbers subsets definition let X be non empty Subset of REAL; cluster Cl X -> non empty; end; definition let D be bounded_below Subset of REAL; cluster Cl D -> bounded_below; end; definition let D be bounded_above Subset of REAL; cluster Cl D -> bounded_above; end; theorem :: TOPREAL6:77 for D being non empty bounded_below Subset of REAL holds inf D = inf Cl D; theorem :: TOPREAL6:78 for D being non empty bounded_above Subset of REAL holds sup D = sup Cl D; definition cluster R^1 -> being_T2; end; theorem :: TOPREAL6:79 for A being Subset of REAL, B being Subset of R^1 st A = B holds A is closed iff B is closed; theorem :: TOPREAL6:80 for A being Subset of REAL, B being Subset of R^1 st A = B holds Cl A = Cl B ; theorem :: TOPREAL6:81 for A being Subset of REAL, B being Subset of R^1 st A = B holds A is compact iff B is compact; definition cluster finite -> compact Subset of REAL; end; definition let a, b be real number; cluster [.a,b.] -> compact; end; theorem :: TOPREAL6:82 for a, b being real number holds a <> b iff Cl ].a,b.[ = [.a,b.]; definition cluster non empty finite bounded Subset of REAL; end; theorem :: TOPREAL6:83 for T being TopStruct, f being RealMap of T, g being map of T, R^1 st f = g holds f is continuous iff g is continuous; theorem :: TOPREAL6:84 for A, B being Subset of REAL, f being map of [:R^1,R^1:], TOP-REAL 2 st for x, y being Real holds f. [x,y] = <*x,y*> holds f.:[:A,B:] = product ((1,2) --> (A,B)); theorem :: TOPREAL6:85 for f being map of [:R^1,R^1:], TOP-REAL 2 st for x, y being Real holds f. [x,y] = <*x,y*> holds f is_homeomorphism; theorem :: TOPREAL6:86 [:R^1,R^1:], TOP-REAL 2 are_homeomorphic; begin :: Bounded subsets theorem :: TOPREAL6:87 for A, B being compact Subset of REAL holds product ((1,2) --> (A,B)) is compact Subset of TOP-REAL 2; theorem :: TOPREAL6:88 P is Bounded closed implies P is compact; theorem :: TOPREAL6:89 P is Bounded implies for g being continuous RealMap of TOP-REAL 2 holds Cl(g.:P) c= g.:Cl P; theorem :: TOPREAL6:90 proj1.:Cl P c= Cl(proj1.:P); theorem :: TOPREAL6:91 proj2.:Cl P c= Cl(proj2.:P); theorem :: TOPREAL6:92 P is Bounded implies Cl(proj1.:P) = proj1.:Cl P; theorem :: TOPREAL6:93 P is Bounded implies Cl(proj2.:P) = proj2.:Cl P; theorem :: TOPREAL6:94 D is Bounded implies W-bound D = W-bound Cl D; theorem :: TOPREAL6:95 D is Bounded implies E-bound D = E-bound Cl D; theorem :: TOPREAL6:96 D is Bounded implies N-bound D = N-bound Cl D; theorem :: TOPREAL6:97 D is Bounded implies S-bound D = S-bound Cl D;

Back to top