:: Compactness of the Bounded Closed Subsets of TOP-REAL 2
:: by Artur Korni{\l}owicz
::
:: Received February 19, 1999
:: Copyright (c) 1999-2018 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 NUMBERS, REAL_1, SUBSET_1, XBOOLE_0, METRIC_1, PRE_TOPC, EUCLID,
CARD_1, XXREAL_0, SQUARE_1, ARYTM_3, RELAT_1, COMPLEX1, ARYTM_1, CARD_3,
FINSEQ_2, FINSEQ_1, NAT_1, FUNCT_1, NEWTON, RVSUM_1, TARSKI, XXREAL_1,
ORDINAL2, XXREAL_2, FINSET_1, RELAT_2, CONNSP_1, T_0TOPSP, TOPS_2,
SETFAM_1, RCOMP_1, ZFMISC_1, STRUCT_0, FUNCOP_1, SUPINF_2, MCART_1,
RLTOPSP1, PSCOMP_1, SPPOL_1, TOPREAL4, CONVEX1, TOPREAL1, TOPREAL2,
SPRECT_1, PCOMPS_1, SEQ_1, SEQ_2, TOPMETR, PARTFUN1, CONNSP_2, TOPS_1,
BORSUK_1, SEQ_4, FUNCT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
RELSET_1, PARTFUN1, FUNCT_2, FUNCT_3, BINOP_1, FINSET_1, ORDINAL1,
NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, SQUARE_1, NAT_1, NAT_D,
FUNCOP_1, FUNCT_4, SEQ_1, SEQ_2, SEQ_4, STRUCT_0, METRIC_1, TBSP_1,
FINSEQ_1, FINSEQ_2, RVSUM_1, NEWTON, XXREAL_0, XXREAL_2, CARD_3,
FINSEQ_4, RCOMP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1, CONNSP_2,
COMPTS_1, BORSUK_1, MEASURE6, PCOMPS_1, RLVECT_1, RLTOPSP1, EUCLID,
WEIERSTR, TOPMETR, TOPREAL1, TOPREAL2, T_0TOPSP, TOPREAL4, PSCOMP_1,
SPPOL_1, SPRECT_1;
constructors SETFAM_1, FUNCT_3, REAL_1, SQUARE_1, NAT_1, CARD_3, FINSEQOP,
RCOMP_1, FINSEQ_4, FINSOP_1, NEWTON, NAT_D, TOPS_1, CONNSP_1, TOPS_2,
COMPTS_1, TBSP_1, T_0TOPSP, MONOID_0, TOPREAL1, TOPREAL2, TOPREAL4,
SPPOL_1, JORDAN1, PSCOMP_1, WEIERSTR, SPRECT_1, JORDAN2C, XXREAL_2,
SEQ_4, FUNCSDOM, CONVEX1, BINOP_2, SEQ_2, MEASURE6, PCOMPS_1, COMSEQ_2;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FUNCT_4, FINSET_1,
NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED, FINSEQ_1, RCOMP_1,
STRUCT_0, PRE_TOPC, TOPS_1, COMPTS_1, METRIC_1, PCOMPS_1, BORSUK_1,
TEX_4, MONOID_0, EUCLID, TOPMETR, JORDAN1, PSCOMP_1, GOBOARD9, WAYBEL_2,
TOPGRP_1, JORDAN2C, VALUED_0, XXREAL_2, RLTOPSP1, TBSP_1, SPRECT_1,
FUNCT_2, JORDAN5A, NEWTON, RVSUM_1, NAT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin :: Real numbers
reserve a, b for Real,
r for Real,
rr 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;
::$CT
theorem :: TOPREAL6:2
0 <= a & a <= b implies |.a.| <= |.b.|;
theorem :: TOPREAL6:3
b <= a & a <= 0 implies |.a.| <= |.b.|;
theorem :: TOPREAL6:4
Product(0|->rr) = 1;
theorem :: TOPREAL6:5
Product(1|->rr) = rr;
theorem :: TOPREAL6:6
Product(2|->rr) = rr * rr;
theorem :: TOPREAL6:7
Product((n+1) |-> rr) = (Product(n|->rr))*rr;
theorem :: TOPREAL6:8
j <> 0 & rr = 0 iff Product(j|->rr) = 0;
theorem :: TOPREAL6:9
rr <> 0 & j <= i implies Product((i-'j) |-> rr) = Product(i|->rr) /
Product(j|->rr);
theorem :: TOPREAL6:10
r <> 0 & j <= i implies r|^(i-'j) = r|^i / r|^j;
reserve a, b for Real;
theorem :: TOPREAL6:11
for a,b being Real holds sqr <*a,b*> = <*a^2,b^2*>;
theorem :: TOPREAL6:12
for i be Nat for F being FinSequence of REAL st i in dom abs F &
a = F.i holds (abs F).i = |.a.|;
theorem :: TOPREAL6:13
for a,b being Real
holds abs <*a,b*> = <*|.a.|,|.b.|*>;
reserve a, b for Real;
theorem :: TOPREAL6:14
for a, b, c, d being Real st a <= b & c <= d holds |.b-a.| +
|.d-c.| = (b-a) + (d-c);
theorem :: TOPREAL6:15
for a, r being Real holds r > 0 implies a in ].a-r,a+r.[;
theorem :: TOPREAL6:16
for a, r being Real holds r >= 0 implies a in [.a-r,a+r.];
theorem :: TOPREAL6:17
for a, b being Real holds a < b implies lower_bound ].a,b.[ = a &
upper_bound ].a,b.[ = b;
begin :: Topological preliminaries
registration
let T be TopStruct, A be finite Subset of T;
cluster T|A -> finite;
end;
registration
let T be TopStruct;
cluster empty -> connected for Subset of T;
end;
::$CT
theorem :: TOPREAL6:19
for S, T being TopSpace st S, T are_homeomorphic & S is
connected holds T is connected;
theorem :: TOPREAL6:20
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
theorem :: TOPREAL6:21
for A, B, C, D being set, a, b being object st A c= B & C c= D
holds product (a,b) --> (A,C) c= product (a,b) --> (B,D);
theorem :: TOPREAL6:22
for A, B being Subset of REAL holds product ((1,2) --> (A,B)) is
Subset of TOP-REAL 2;
theorem :: TOPREAL6:23
|.|[0,a]|.| = |.a.| & |.|[a,0]|.| = |.a.|;
theorem :: TOPREAL6:24
for p being Point of Euclid 2, q being Point of TOP-REAL 2 st p
= 0.TOP-REAL 2 & p = q holds q = <* 0,0 *> & q`1 = 0 & q`2 = 0;
theorem :: TOPREAL6:25
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:26
r*p = |[r*p`1,r*p`2]|;
theorem :: TOPREAL6:27
s = (1-r)*p + r*q & s <> p & 0 <= r implies 0 < r;
theorem :: TOPREAL6:28
s = (1-r)*p + r*q & s <> q & r <= 1 implies r < 1;
theorem :: TOPREAL6:29
s in LSeg(p,q) & s <> p & s <> q & p`1 < q`1 implies p`1 < s`1 & s`1 < q`1;
theorem :: TOPREAL6:30
s in LSeg(p,q) & s <> p & s <> q & p`2 < q`2 implies p`2 < s`2 & s`2 < q`2;
theorem :: TOPREAL6:31
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:32
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:33
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:34
for p being Point of TOP-REAL 2 ex q being Point of TOP-REAL 2 st q`2
< S-bound D & p <> q;
registration
cluster non horizontal -> non empty for Subset of TOP-REAL 2;
cluster non vertical -> non empty for Subset of TOP-REAL 2;
cluster being_Region -> open connected for Subset of TOP-REAL 2;
cluster open connected -> being_Region for Subset of TOP-REAL 2;
end;
registration
cluster empty -> horizontal for Subset of TOP-REAL 2;
cluster empty -> vertical for Subset of TOP-REAL 2;
end;
registration
cluster non empty convex for Subset of TOP-REAL 2;
end;
registration
let a, b be Point of TOP-REAL 2;
cluster LSeg(a,b) -> connected;
end;
registration
cluster R^2-unit_square -> connected;
end;
registration
cluster being_simple_closed_curve -> connected for Subset of TOP-REAL 2;
end;
theorem :: TOPREAL6:35 :: SPRECT_3:26
LSeg(NE-corner P,SE-corner P) c= L~SpStSeq P;
theorem :: TOPREAL6:36
LSeg(SW-corner P,SE-corner P) c= L~SpStSeq P;
theorem :: TOPREAL6:37
LSeg(SW-corner P,NW-corner P) c= L~SpStSeq P;
theorem :: TOPREAL6:38
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
reserve r for Real;
theorem :: TOPREAL6:39
e = q & p in Ball(e,r) implies q`1-r < p`1 & p`1 < q`1+r;
theorem :: TOPREAL6:40
e = q & p in Ball(e,r) implies q`2-r < p`2 & p`2 < q`2+r;
theorem :: TOPREAL6:41
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:42
p = e implies Ball(e,r) c= product((1,2)-->(].p`1-r,p`1+r.[,].p
`2-r,p`2+r.[));
theorem :: TOPREAL6:43
P = Ball(e,r) & p = e implies proj1.:P = ].p`1-r,p`1+r.[;
theorem :: TOPREAL6:44
P = Ball(e,r) & p = e implies proj2.:P = ].p`2-r,p`2+r.[;
theorem :: TOPREAL6:45
D = Ball(e,r) & p = e implies W-bound D = p`1 - r;
theorem :: TOPREAL6:46
D = Ball(e,r) & p = e implies E-bound D = p`1 + r;
theorem :: TOPREAL6:47
D = Ball(e,r) & p = e implies S-bound D = p`2 - r;
theorem :: TOPREAL6:48
D = Ball(e,r) & p = e implies N-bound D = p`2 + r;
theorem :: TOPREAL6:49
D = Ball(e,r) implies D is non horizontal;
theorem :: TOPREAL6:50
D = Ball(e,r) implies D is non vertical;
theorem :: TOPREAL6:51
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:52
for X being non empty compact Subset of TOP-REAL 2, p being Point of
Euclid 2 st p = 0.TOP-REAL 2 & a > 0 holds X
c= Ball(p, |.E-bound X.|+|.N-bound X.|+|.W-bound X.|+|.S-bound X.|+a);
theorem :: TOPREAL6:53
for M being Reflexive symmetric triangle non empty MetrStruct,
z being Point of M holds r < 0 implies Sphere(z,r) = {};
theorem :: TOPREAL6:54
for M being Reflexive discerning non empty MetrStruct, z being Point
of M holds Sphere(z,0) = {z};
theorem :: TOPREAL6:55
for M being Reflexive symmetric triangle non empty MetrStruct, z
being Point of M holds r < 0 implies cl_Ball(z,r) = {};
theorem :: TOPREAL6:56
cl_Ball(z,0) = {z};
theorem :: TOPREAL6:57
for A being Subset of TopSpaceMetr M st A = cl_Ball(z,r) holds A is closed;
theorem :: TOPREAL6:58
A = cl_Ball(w,r) implies A is closed;
theorem :: TOPREAL6:59
for r being Real for M be Reflexive symmetric triangle
non empty MetrStruct for x be Element of M holds cl_Ball(x,r) is bounded;
theorem :: TOPREAL6:60
for A being Subset of TopSpaceMetr M st A = Sphere(z,r) holds A is closed;
theorem :: TOPREAL6:61
A = Sphere(w,r) implies A is closed;
theorem :: TOPREAL6:62
Sphere(z,r) is bounded;
theorem :: TOPREAL6:63
A is bounded implies Cl A is bounded;
theorem :: TOPREAL6:64
for M being non empty MetrStruct holds M is bounded iff for X being
Subset of M holds X is bounded;
theorem :: TOPREAL6:65
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:66
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;
theorem :: TOPREAL6:67
A is bounded & B is bounded implies A \/ B is bounded;
begin :: Topological properties of real numbers subsets
registration
let X be non empty Subset of REAL;
cluster Cl X -> non empty;
end;
registration
let D be bounded_below Subset of REAL;
cluster Cl D -> bounded_below;
end;
registration
let D be bounded_above Subset of REAL;
cluster Cl D -> bounded_above;
end;
theorem :: TOPREAL6:68
for D being non empty bounded_below Subset of REAL holds lower_bound D =
lower_bound Cl D;
theorem :: TOPREAL6:69
for D being non empty bounded_above Subset of REAL holds upper_bound D =
upper_bound Cl D;
registration
cluster R^1 -> T_2;
end;
::$CT 5
theorem :: TOPREAL6:75
for A, B being Subset of REAL, f being Function 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:76
for f being Function of [:R^1,R^1:], TOP-REAL 2 st for x, y
being Real holds f. [x,y] = <*x,y*> holds f is being_homeomorphism;
theorem :: TOPREAL6:77
[:R^1,R^1:], TOP-REAL 2 are_homeomorphic;
begin :: bounded subsets
theorem :: TOPREAL6:78
for A, B being compact Subset of REAL holds product ((1,2) --> (
A,B)) is compact Subset of TOP-REAL 2;
theorem :: TOPREAL6:79
P is bounded closed implies P is compact;
theorem :: TOPREAL6:80
P is bounded implies for g being continuous RealMap of TOP-REAL
2 holds Cl(g.:P) c= g.:Cl P;
theorem :: TOPREAL6:81
proj1.:Cl P c= Cl(proj1.:P);
theorem :: TOPREAL6:82
proj2.:Cl P c= Cl(proj2.:P);
theorem :: TOPREAL6:83
P is bounded implies Cl(proj1.:P) = proj1.:Cl P;
theorem :: TOPREAL6:84
P is bounded implies Cl(proj2.:P) = proj2.:Cl P;
theorem :: TOPREAL6:85
D is bounded implies W-bound D = W-bound Cl D;
theorem :: TOPREAL6:86
D is bounded implies E-bound D = E-bound Cl D;
theorem :: TOPREAL6:87
D is bounded implies N-bound D = N-bound Cl D;
theorem :: TOPREAL6:88
D is bounded implies S-bound D = S-bound Cl D;
:: Moved from JORDAN1I, AK, 23.02.2006
theorem :: TOPREAL6:89
for A,B being Subset of TOP-REAL n holds A is bounded or B is
bounded implies A /\ B is bounded;
theorem :: TOPREAL6:90
for A,B being Subset of TOP-REAL n holds A is not bounded & B is
bounded implies A \ B is not bounded;
begin :: Addenda
::form GOBRD14, 2006.03.26, A.T.
definition
let n be Nat, a, b be Point of TOP-REAL n;
func dist(a,b) -> Real means
:: TOPREAL6:def 1
ex p, q being Point of Euclid n st p = a & q = b & it = dist(p,q);
commutativity;
end;
reserve r1,r2,s1,s2 for Real;
theorem :: TOPREAL6:91
for u,v being Point of Euclid 2 st u = |[r1,s1]| & v = |[r2,s2
]| holds dist(u,v) =sqrt ((r1 - r2)^2 + (s1 - s2)^2);
theorem :: TOPREAL6:92
dist(p,q) = sqrt ((p`1-q`1)^2 + (p`2-q`2)^2);
theorem :: TOPREAL6:93
for p being Point of TOP-REAL n holds dist(p,p) = 0;
theorem :: TOPREAL6:94
for p, q, r being Point of TOP-REAL n holds dist(p,r) <= dist (p,q) +
dist(q,r);
theorem :: TOPREAL6:95
for x1, x2, y1, y2 being Real, a, b being Point of TOP-REAL 2
st x1 <= a`1 & a`1 <= x2 & y1 <= a`2 & a`2 <= y2 & x1 <= b`1 & b`1 <= x2 & y1
<= b`2 & b`2 <= y2 holds dist(a,b) <= (x2-x1) + (y2-y1);