:: Compactness of the Bounded Closed Subsets of TOP-REAL 2
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 1999-2021 Association of Mizar Users

theorem :: TOPREAL6:1
canceled;

::$CT theorem Th1: :: TOPREAL6:2 for a, b being Real st 0 <= a & a <= b holds |.a.| <= |.b.| proof end; theorem Th2: :: TOPREAL6:3 for a, b being Real st b <= a & a <= 0 holds |.a.| <= |.b.| proof end; theorem :: TOPREAL6:4 for rr being Real holds Product (0 |-> rr) = 1 by RVSUM_1:94; theorem Th4: :: TOPREAL6:5 for rr being Real holds Product (1 |-> rr) = rr proof end; theorem :: TOPREAL6:6 for rr being Real holds Product (2 |-> rr) = rr * rr proof end; theorem Th6: :: TOPREAL6:7 for rr being Real for n being Nat holds Product ((n + 1) |-> rr) = (Product (n |-> rr)) * rr proof end; theorem Th7: :: TOPREAL6:8 for rr being Real for j being Nat holds ( ( j <> 0 & rr = 0 ) iff Product (j |-> rr) = 0 ) proof end; theorem Th8: :: TOPREAL6:9 for rr being Real for i, j being Nat st rr <> 0 & j <= i holds Product ((i -' j) |-> rr) = (Product (i |-> rr)) / (Product (j |-> rr)) proof end; theorem :: TOPREAL6:10 for r being Real for i, j being Nat st r <> 0 & j <= i holds r |^ (i -' j) = (r |^ i) / (r |^ j) proof end; theorem Th10: :: TOPREAL6:11 for a, b being Real holds sqr <*a,b*> = <*(a ^2),(b ^2)*> proof end; theorem Th11: :: TOPREAL6:12 for a being Real for i being Nat for F being FinSequence of REAL st i in dom (abs F) & a = F . i holds (abs F) . i = |.a.| proof end; theorem :: TOPREAL6:13 for a, b being Real holds abs <*a,b*> = <*|.a.|,|.b.|*> proof end; theorem :: TOPREAL6:14 for a, b, c, d being Real st a <= b & c <= d holds |.(b - a).| + |.(d - c).| = (b - a) + (d - c) proof end; theorem Th14: :: TOPREAL6:15 for a, r being Real st r > 0 holds a in ].(a - r),(a + r).[ proof end; theorem :: TOPREAL6:16 for a, r being Real st r >= 0 holds a in [.(a - r),(a + r).] proof end; theorem Th16: :: TOPREAL6:17 for a, b being Real st a < b holds ( lower_bound ].a,b.[ = a & upper_bound ].a,b.[ = b ) proof end; registration let T be TopStruct ; let A be finite Subset of T; cluster T | A -> finite ; coherence T | A is finite by PRE_TOPC:8; end; registration let T be TopStruct ; cluster empty -> connected for Element of bool the carrier of T; coherence for b1 being Subset of T st b1 is empty holds b1 is connected proof end; end; theorem :: TOPREAL6:18 canceled; ::$CT
theorem Th17: :: TOPREAL6:19
for S, T being TopSpace st S,T are_homeomorphic & S is connected holds
T is connected
proof end;

theorem :: TOPREAL6:20
for T being TopSpace
for 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
proof end;

theorem Th19: :: TOPREAL6:21
for A, B, C, D being set
for a, b being object st A c= B & C c= D holds
product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D))
proof end;

theorem Th20: :: TOPREAL6:22
for A, B being Subset of REAL holds product ((1,2) --> (A,B)) is Subset of ()
proof end;

theorem :: TOPREAL6:23
for a being Real holds
( = |.a.| & = |.a.| )
proof end;

theorem Th22: :: TOPREAL6:24
for p being Point of ()
for q being Point of () st p = 0. () & p = q holds
( q = & q 1 = 0 & q 2 = 0 )
proof end;

theorem :: TOPREAL6:25
for p, q being Point of ()
for z being Point of () st p = 0.REAL 2 & q = z holds
dist (p,q) = |.z.|
proof end;

theorem Th24: :: TOPREAL6:26
for r being Real
for p being Point of () holds r * p = |[(r * (p 1)),(r * (p 2))]|
proof end;

theorem Th25: :: TOPREAL6:27
for r being Real
for p, q, s being Point of () st s = ((1 - r) * p) + (r * q) & s <> p & 0 <= r holds
0 < r
proof end;

theorem Th26: :: TOPREAL6:28
for r being Real
for p, q, s being Point of () st s = ((1 - r) * p) + (r * q) & s <> q & r <= 1 holds
r < 1
proof end;

theorem :: TOPREAL6:29
for p, q, s being Point of () st s in LSeg (p,q) & s <> p & s <> q & p 1 < q 1 holds
( p 1 < s 1 & s 1 < q 1 )
proof end;

theorem :: TOPREAL6:30
for p, q, s being Point of () st s in LSeg (p,q) & s <> p & s <> q & p 2 < q 2 holds
( p 2 < s 2 & s 2 < q 2 )
proof end;

theorem :: TOPREAL6:31
for D being non empty Subset of ()
for p being Point of () ex q being Point of () st
( q 1 < W-bound D & p <> q )
proof end;

theorem :: TOPREAL6:32
for D being non empty Subset of ()
for p being Point of () ex q being Point of () st
( q 1 > E-bound D & p <> q )
proof end;

theorem :: TOPREAL6:33
for D being non empty Subset of ()
for p being Point of () ex q being Point of () st
( q 2 > N-bound D & p <> q )
proof end;

theorem :: TOPREAL6:34
for D being non empty Subset of ()
for p being Point of () ex q being Point of () st
( q 2 < S-bound D & p <> q )
proof end;

registration
cluster non horizontal -> non empty for Element of bool the carrier of ();
coherence
for b1 being Subset of () st not b1 is horizontal holds
not b1 is empty
;
cluster non vertical -> non empty for Element of bool the carrier of ();
coherence
for b1 being Subset of () st not b1 is vertical holds
not b1 is empty
;
cluster being_Region -> open connected for Element of bool the carrier of ();
coherence
for b1 being Subset of () st b1 is being_Region holds
( b1 is open & b1 is connected )
by TOPREAL4:def 3;
cluster open connected -> being_Region for Element of bool the carrier of ();
coherence
for b1 being Subset of () st b1 is open & b1 is connected holds
b1 is being_Region
by TOPREAL4:def 3;
end;

registration
cluster empty -> horizontal for Element of bool the carrier of ();
coherence
for b1 being Subset of () st b1 is empty holds
b1 is horizontal
;
cluster empty -> vertical for Element of bool the carrier of ();
coherence
for b1 being Subset of () st b1 is empty holds
b1 is vertical
;
end;

registration
cluster non empty convex for Element of bool the carrier of ();
existence
ex b1 being Subset of () st
( not b1 is empty & b1 is convex )
proof end;
end;

registration
let a, b be Point of ();
cluster LSeg (a,b) -> connected ;
coherence
LSeg (a,b) is connected
;
end;

registration
coherence
proof end;
end;

registration
cluster being_simple_closed_curve -> connected for Element of bool the carrier of ();
coherence
for b1 being Subset of () st b1 is being_simple_closed_curve holds
b1 is connected
proof end;
end;

theorem :: TOPREAL6:35
for P being Subset of () holds LSeg ((),()) c= L~ ()
proof end;

theorem :: TOPREAL6:36
for P being Subset of () holds LSeg ((),()) c= L~ ()
proof end;

theorem :: TOPREAL6:37
for P being Subset of () holds LSeg ((),()) c= L~ ()
proof end;

theorem :: TOPREAL6:38
for C being Subset of () holds { p where p is Point of () : p 1 < W-bound C } is non empty connected convex Subset of ()
proof end;

theorem Th37: :: TOPREAL6:39
for p, q being Point of ()
for e being Point of ()
for r being Real st e = q & p in Ball (e,r) holds
( (q 1) - r < p 1 & p 1 < (q 1) + r )
proof end;

theorem Th38: :: TOPREAL6:40
for p, q being Point of ()
for e being Point of ()
for r being Real st e = q & p in Ball (e,r) holds
( (q 2) - r < p 2 & p 2 < (q 2) + r )
proof end;

theorem Th39: :: TOPREAL6:41
for p being Point of ()
for e being Point of ()
for r being Real st p = e holds
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)
proof end;

theorem Th40: :: TOPREAL6:42
for p being Point of ()
for e being Point of ()
for r being Real st p = e holds
Ball (e,r) c= product ((1,2) --> (].((p 1) - r),((p 1) + r).[,].((p 2) - r),((p 2) + r).[))
proof end;

theorem Th41: :: TOPREAL6:43
for p being Point of ()
for e being Point of ()
for P being Subset of ()
for r being Real st P = Ball (e,r) & p = e holds
proj1 .: P = ].((p 1) - r),((p 1) + r).[
proof end;

theorem Th42: :: TOPREAL6:44
for p being Point of ()
for e being Point of ()
for P being Subset of ()
for r being Real st P = Ball (e,r) & p = e holds
proj2 .: P = ].((p 2) - r),((p 2) + r).[
proof end;

theorem :: TOPREAL6:45
for p being Point of ()
for e being Point of ()
for D being non empty Subset of ()
for r being Real st D = Ball (e,r) & p = e holds
W-bound D = (p 1) - r
proof end;

theorem :: TOPREAL6:46
for p being Point of ()
for e being Point of ()
for D being non empty Subset of ()
for r being Real st D = Ball (e,r) & p = e holds
E-bound D = (p 1) + r
proof end;

theorem :: TOPREAL6:47
for p being Point of ()
for e being Point of ()
for D being non empty Subset of ()
for r being Real st D = Ball (e,r) & p = e holds
S-bound D = (p 2) - r
proof end;

theorem :: TOPREAL6:48
for p being Point of ()
for e being Point of ()
for D being non empty Subset of ()
for r being Real st D = Ball (e,r) & p = e holds
N-bound D = (p 2) + r
proof end;

theorem :: TOPREAL6:49
for e being Point of ()
for D being non empty Subset of ()
for r being Real st D = Ball (e,r) holds
not D is horizontal
proof end;

theorem :: TOPREAL6:50
for e being Point of ()
for D being non empty Subset of ()
for r being Real st D = Ball (e,r) holds
not D is vertical
proof end;

theorem :: TOPREAL6:51
for a being Real
for f being Point of ()
for x being Point of () st x in Ball (f,a) holds
not |[((x 1) - (2 * a)),(x 2)]| in Ball (f,a)
proof end;

theorem :: TOPREAL6:52
for a being Real
for X being non empty compact Subset of ()
for p being Point of () st p = 0. () & a > 0 holds
X c= Ball (p,((((|.().| + |.().|) + |.().|) + |.().|) + a))
proof end;

theorem Th51: :: TOPREAL6:53
for r being Real
for M being non empty Reflexive symmetric triangle MetrStruct
for z being Point of M st r < 0 holds
Sphere (z,r) = {}
proof end;

theorem :: TOPREAL6:54
for M being non empty Reflexive discerning MetrStruct
for z being Point of M holds Sphere (z,0) = {z}
proof end;

theorem :: TOPREAL6:55
for r being Real
for M being non empty Reflexive symmetric triangle MetrStruct
for z being Point of M st r < 0 holds
cl_Ball (z,r) = {}
proof end;

theorem :: TOPREAL6:56
for M being non empty MetrSpace
for z being Point of M holds cl_Ball (z,0) = {z}
proof end;

Lm1: for M being non empty MetrSpace
for z being Point of M
for r being Real
for A being Subset of () st A = cl_Ball (z,r) holds
A  is open

proof end;

theorem Th55: :: TOPREAL6:57
for M being non empty MetrSpace
for z being Point of M
for r being Real
for A being Subset of () st A = cl_Ball (z,r) holds
A is closed
proof end;

theorem :: TOPREAL6:58
for n being Nat
for w being Point of ()
for A being Subset of ()
for r being Real st A = cl_Ball (w,r) holds
A is closed
proof end;

theorem Th57: :: TOPREAL6:59
for r being Real
for M being non empty Reflexive symmetric triangle MetrStruct
for x being Element of M holds cl_Ball (x,r) is bounded
proof end;

theorem Th58: :: TOPREAL6:60
for M being non empty MetrSpace
for z being Point of M
for r being Real
for A being Subset of () st A = Sphere (z,r) holds
A is closed
proof end;

theorem :: TOPREAL6:61
for n being Nat
for w being Point of ()
for A being Subset of ()
for r being Real st A = Sphere (w,r) holds
A is closed
proof end;

theorem :: TOPREAL6:62
for M being non empty MetrSpace
for z being Point of M
for r being Real holds Sphere (z,r) is bounded
proof end;

theorem :: TOPREAL6:63
for n being Nat
for A being Subset of () st A is bounded holds
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 )
proof end;

theorem Th63: :: TOPREAL6:65
for M being non empty Reflexive symmetric triangle MetrStruct
for X, Y being Subset of M st the carrier of M = X \/ Y & not M is bounded & X is bounded holds
not Y is bounded
proof end;

theorem :: TOPREAL6:66
for n being Nat
for X, Y being Subset of () st n >= 1 & the carrier of () = X \/ Y & X is bounded holds
not Y is bounded
proof end;

theorem Th65: :: TOPREAL6:67
for n being Nat
for A, B being Subset of () st A is bounded & B is bounded holds
A \/ B is bounded
proof end;

registration
let X be non empty Subset of REAL;
cluster Cl X -> non empty ;
coherence
not Cl X is empty
by ;
end;

registration
let D be bounded_below Subset of REAL;
coherence
proof end;
end;

registration
let D be bounded_above Subset of REAL;
coherence
proof end;
end;

theorem Th66: :: TOPREAL6:68
for D being non empty bounded_below Subset of REAL holds lower_bound D = lower_bound (Cl D)
proof end;

theorem Th67: :: TOPREAL6:69
for D being non empty bounded_above Subset of REAL holds upper_bound D = upper_bound (Cl D)
proof end;

registration
coherence
R^1 is T_2
by ;
end;

theorem :: TOPREAL6:70
canceled;

theorem :: TOPREAL6:71
canceled;

theorem :: TOPREAL6:72
canceled;

theorem :: TOPREAL6:73
canceled;

theorem :: TOPREAL6:74
canceled;

::\$CT 5
theorem Th68: :: TOPREAL6:75
for A, B being Subset of REAL
for f being Function of ,() st ( for x, y being Real holds f . [x,y] = <*x,y*> ) holds
f .: [:A,B:] = product ((1,2) --> (A,B))
proof end;

theorem Th69: :: TOPREAL6:76
for f being Function of ,() st ( for x, y being Real holds f . [x,y] = <*x,y*> ) holds
f is being_homeomorphism
proof end;

theorem :: TOPREAL6:77
proof end;

theorem Th71: :: TOPREAL6:78
for A, B being compact Subset of REAL holds product ((1,2) --> (A,B)) is compact Subset of ()
proof end;

theorem Th72: :: TOPREAL6:79
for P being Subset of () st P is bounded & P is closed holds
P is compact
proof end;

theorem Th73: :: TOPREAL6:80
for P being Subset of () st P is bounded holds
for g being continuous RealMap of () holds Cl (g .: P) c= g .: (Cl P)
proof end;

theorem Th74: :: TOPREAL6:81
for P being Subset of () holds proj1 .: (Cl P) c= Cl ()
proof end;

theorem Th75: :: TOPREAL6:82
for P being Subset of () holds proj2 .: (Cl P) c= Cl ()
proof end;

theorem Th76: :: TOPREAL6:83
for P being Subset of () st P is bounded holds
Cl () = proj1 .: (Cl P) by ;

theorem Th77: :: TOPREAL6:84
for P being Subset of () st P is bounded holds
Cl () = proj2 .: (Cl P) by ;

theorem :: TOPREAL6:85
for D being non empty Subset of () st D is bounded holds
W-bound D = W-bound (Cl D)
proof end;

theorem :: TOPREAL6:86
for D being non empty Subset of () st D is bounded holds
E-bound D = E-bound (Cl D)
proof end;

theorem :: TOPREAL6:87
for D being non empty Subset of () st D is bounded holds
N-bound D = N-bound (Cl D)
proof end;

theorem :: TOPREAL6:88
for D being non empty Subset of () st D is bounded holds
S-bound D = S-bound (Cl D)
proof end;

:: Moved from JORDAN1I, AK, 23.02.2006
theorem Th82: :: TOPREAL6:89
for n being Nat
for A, B being Subset of () st ( A is bounded or B is bounded ) holds
A /\ B is bounded
proof end;

theorem :: TOPREAL6:90
for n being Nat
for A, B being Subset of () st not A is bounded & B is bounded holds
not A \ B is bounded
proof end;

::form GOBRD14, 2006.03.26, A.T.
definition
let n be Nat;
let a, b be Point of ();
func dist (a,b) -> Real means :Def1: :: TOPREAL6:def 1
ex p, q being Point of () st
( p = a & q = b & it = dist (p,q) );
existence
ex b1 being Real ex p, q being Point of () st
( p = a & q = b & b1 = dist (p,q) )
proof end;
uniqueness
for b1, b2 being Real st ex p, q being Point of () st
( p = a & q = b & b1 = dist (p,q) ) & ex p, q being Point of () st
( p = a & q = b & b2 = dist (p,q) ) holds
b1 = b2
;
commutativity
for b1 being Real
for a, b being Point of () st ex p, q being Point of () st
( p = a & q = b & b1 = dist (p,q) ) holds
ex p, q being Point of () st
( p = b & q = a & b1 = dist (p,q) )
;
end;

:: deftheorem Def1 defines dist TOPREAL6:def 1 :
for n being Nat
for a, b being Point of ()
for b4 being Real holds
( b4 = dist (a,b) iff ex p, q being Point of () st
( p = a & q = b & b4 = dist (p,q) ) );

theorem Th84: :: TOPREAL6:91
for r1, r2, s1, s2 being Real
for u, v being Point of () st u = |[r1,s1]| & v = |[r2,s2]| holds
dist (u,v) = sqrt (((r1 - r2) ^2) + ((s1 - s2) ^2))
proof end;

theorem Th85: :: TOPREAL6:92
for p, q being Point of () holds dist (p,q) = sqrt ((((p 1) - (q 1)) ^2) + (((p 2) - (q 2)) ^2))
proof end;

theorem :: TOPREAL6:93
for n being Nat
for p being Point of () holds dist (p,p) = 0
proof end;

theorem :: TOPREAL6:94
for n being Nat
for p, q, r being Point of () holds dist (p,r) <= (dist (p,q)) + (dist (q,r))
proof end;

theorem :: TOPREAL6:95
for x1, x2, y1, y2 being Real
for a, b being Point of () 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)
proof end;