Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

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

by
Artur Kornilowicz

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 *> & q1 = 0 & q2 = 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*p1,r*p2]|;

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 & p1 < q1 implies p1 < s1 & s1 < q1;

theorem :: TOPREAL6:38
s in LSeg(p,q) & s <> p & s <> q & p2 < q2 implies p2 < s2 & s2 < q2;

theorem :: TOPREAL6:39
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q1 < 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 q1 > 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 q2 > 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 q2 < 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: p1 < 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 q1-r < p1 & p1 < q1+r;

theorem :: TOPREAL6:48
e = q & p in Ball(e,r) implies q2-r < p2 & p2 < q2+r;

theorem :: TOPREAL6:49
p = e implies
product ((1,2) --> (].p1-r/sqrt 2,p1+r/sqrt 2.[,
].p2-r/sqrt 2,p2+r/sqrt 2.[))
c= Ball(e,r);

theorem :: TOPREAL6:50
p = e implies Ball(e,r) c= product((1,2)-->(].p1-r,p1+r.[,].p2-r,p2+r.[));

theorem :: TOPREAL6:51
P = Ball(e,r) & p = e implies proj1.:P = ].p1-r,p1+r.[;

theorem :: TOPREAL6:52
P = Ball(e,r) & p = e implies proj2.:P = ].p2-r,p2+r.[;

theorem :: TOPREAL6:53
D = Ball(e,r) & p = e implies W-bound D = p1 - r;

theorem :: TOPREAL6:54
D = Ball(e,r) & p = e implies E-bound D = p1 + r;

theorem :: TOPREAL6:55
D = Ball(e,r) & p = e implies S-bound D = p2 - r;

theorem :: TOPREAL6:56
D = Ball(e,r) & p = e implies N-bound D = p2 + 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 |[x1-2*a,x2]| 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;
`