Journal of Formalized Mathematics
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