:: by Artur Korni{\l}owicz

::

:: Received February 19, 1999

:: Copyright (c) 1999 Association of Mizar Users

begin

theorem :: TOPREAL6:1

canceled;

theorem :: TOPREAL6:2

canceled;

theorem :: TOPREAL6:3

canceled;

theorem :: TOPREAL6:4

canceled;

theorem :: TOPREAL6:5

canceled;

theorem Th6: :: TOPREAL6:6

proof end;

theorem Th7: :: TOPREAL6:7

proof end;

theorem Th8: :: TOPREAL6:8

proof end;

theorem :: TOPREAL6:9

theorem Th10: :: TOPREAL6:10

proof end;

theorem :: TOPREAL6:11

proof end;

theorem Th12: :: TOPREAL6:12

proof end;

theorem Th13: :: TOPREAL6:13

proof end;

theorem Th14: :: TOPREAL6:14

for r being Real

for j, i being Element of NAT st r <> 0 & j <= i holds

Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r))

for j, i being Element of NAT st r <> 0 & j <= i holds

Product ((i -' j) |-> r) = (Product (i |-> r)) / (Product (j |-> r))

proof end;

theorem :: TOPREAL6:15

for r being Real

for j, i being Element of NAT st r <> 0 & j <= i holds

r |^ (i -' j) = (r |^ i) / (r |^ j)

for j, i being Element of NAT st r <> 0 & j <= i holds

r |^ (i -' j) = (r |^ i) / (r |^ j)

proof end;

theorem Th16: :: TOPREAL6:16

proof end;

theorem Th17: :: TOPREAL6:17

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 = abs a

for i being Nat

for F being FinSequence of REAL st i in dom (abs F) & a = F . i holds

(abs F) . i = abs a

proof end;

theorem :: TOPREAL6:18

proof end;

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)

(abs (b - a)) + (abs (d - c)) = (b - a) + (d - c)

proof end;

theorem Th20: :: TOPREAL6:20

proof end;

theorem :: TOPREAL6:21

proof end;

theorem Th22: :: TOPREAL6:22

proof end;

theorem :: TOPREAL6:23

canceled;

theorem Th24: :: TOPREAL6:24

proof end;

begin

registration

let T be TopStruct ;

let A be finite Subset of T;

cluster T | A -> finite ;

coherence

T | A is finite by PRE_TOPC:29;

end;
let A be finite Subset of T;

cluster T | A -> finite ;

coherence

T | A is finite by PRE_TOPC:29;

registration

let T be TopStruct ;

cluster empty -> connected Element of bool the carrier of T;

coherence

for b_{1} being Subset of T st b_{1} is empty holds

b_{1} is connected

end;
cluster empty -> connected Element of bool the carrier of T;

coherence

for b

b

proof end;

theorem Th25: :: TOPREAL6:25

proof end;

theorem :: TOPREAL6:26

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

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;

begin

theorem :: TOPREAL6:27

canceled;

theorem :: TOPREAL6:28

canceled;

theorem Th29: :: 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))

product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D))

proof end;

theorem Th30: :: TOPREAL6:30

proof end;

theorem :: TOPREAL6:31

proof end;

theorem Th32: :: TOPREAL6:32

for p being Point of (Euclid 2)

for 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 )

for 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 )

proof end;

theorem :: TOPREAL6:33

for p, q being Point of (Euclid 2)

for z being Point of (TOP-REAL 2) st p = 0.REAL 2 & q = z holds

dist (p,q) = |.z.|

for z being Point of (TOP-REAL 2) st p = 0.REAL 2 & q = z holds

dist (p,q) = |.z.|

proof end;

theorem Th34: :: TOPREAL6:34

proof end;

theorem Th35: :: TOPREAL6:35

for r being Real

for s, p, q being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> p & 0 <= r holds

0 < r

for s, p, q being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> p & 0 <= r holds

0 < r

proof end;

theorem Th36: :: TOPREAL6:36

for r being Real

for s, p, q being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> q & r <= 1 holds

r < 1

for s, p, q being Point of (TOP-REAL 2) st s = ((1 - r) * p) + (r * q) & s <> q & r <= 1 holds

r < 1

proof end;

theorem :: TOPREAL6:37

for s, p, q being Point of (TOP-REAL 2) st s in LSeg (p,q) & s <> p & s <> q & p `1 < q `1 holds

( p `1 < s `1 & s `1 < q `1 )

( p `1 < s `1 & s `1 < q `1 )

proof end;

theorem :: TOPREAL6:38

for s, p, q being Point of (TOP-REAL 2) st s in LSeg (p,q) & s <> p & s <> q & p `2 < q `2 holds

( p `2 < s `2 & s `2 < q `2 )

( p `2 < s `2 & s `2 < q `2 )

proof end;

theorem :: TOPREAL6:39

for D being non empty Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st

( q `1 < W-bound D & p <> q )

for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st

( q `1 < W-bound D & p <> q )

proof end;

theorem :: TOPREAL6:40

for D being non empty Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st

( q `1 > E-bound D & p <> q )

for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st

( q `1 > E-bound D & p <> q )

proof end;

theorem :: TOPREAL6:41

for D being non empty Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st

( q `2 > N-bound D & p <> q )

for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st

( q `2 > N-bound D & p <> q )

proof end;

theorem :: TOPREAL6:42

for D being non empty Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st

( q `2 < S-bound D & p <> q )

for p being Point of (TOP-REAL 2) ex q being Point of (TOP-REAL 2) st

( q `2 < S-bound D & p <> q )

proof end;

registration

cluster non horizontal -> non empty Element of bool the carrier of (TOP-REAL 2);

coherence

for b_{1} being Subset of (TOP-REAL 2) st not b_{1} is horizontal holds

not b_{1} is empty

coherence

for b_{1} being Subset of (TOP-REAL 2) st not b_{1} is vertical holds

not b_{1} is empty

coherence

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is being_Region holds

( b_{1} is open & b_{1} is connected )
by TOPREAL4:def 3;

cluster open connected -> being_Region Element of bool the carrier of (TOP-REAL 2);

coherence

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is open & b_{1} is connected holds

b_{1} is being_Region
by TOPREAL4:def 3;

end;
coherence

for b

not b

proof end;

cluster non vertical -> non empty Element of bool the carrier of (TOP-REAL 2);coherence

for b

not b

proof end;

cluster being_Region -> open connected Element of bool the carrier of (TOP-REAL 2);coherence

for b

( b

cluster open connected -> being_Region Element of bool the carrier of (TOP-REAL 2);

coherence

for b

b

registration

cluster empty -> horizontal Element of bool the carrier of (TOP-REAL 2);

coherence

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is empty holds

b_{1} is horizontal
;

cluster empty -> vertical Element of bool the carrier of (TOP-REAL 2);

coherence

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is empty holds

b_{1} is vertical
;

end;
coherence

for b

b

cluster empty -> vertical Element of bool the carrier of (TOP-REAL 2);

coherence

for b

b

registration

cluster non empty convex Element of bool the carrier of (TOP-REAL 2);

existence

ex b_{1} being Subset of (TOP-REAL 2) st

( not b_{1} is empty & b_{1} is convex )

end;
existence

ex b

( not b

proof end;

registration

let a, b be Point of (TOP-REAL 2);

cluster LSeg (a,b) -> connected ;

coherence

LSeg (a,b) is connected ;

end;
cluster LSeg (a,b) -> connected ;

coherence

LSeg (a,b) is connected ;

registration
end;

registration

cluster being_simple_closed_curve -> connected Element of bool the carrier of (TOP-REAL 2);

coherence

for b_{1} being Subset of (TOP-REAL 2) st b_{1} is being_simple_closed_curve holds

b_{1} is connected

end;
coherence

for b

b

proof end;

theorem :: TOPREAL6:43

proof end;

theorem :: TOPREAL6:44

proof end;

theorem :: TOPREAL6:45

proof end;

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 connected convex Subset of (TOP-REAL 2)

proof end;

begin

theorem Th47: :: TOPREAL6:47

for q, p being Point of (TOP-REAL 2)

for e being Point of (Euclid 2)

for r being real number st e = q & p in Ball (e,r) holds

( (q `1) - r < p `1 & p `1 < (q `1) + r )

for e being Point of (Euclid 2)

for r being real number st e = q & p in Ball (e,r) holds

( (q `1) - r < p `1 & p `1 < (q `1) + r )

proof end;

theorem Th48: :: TOPREAL6:48

for q, p being Point of (TOP-REAL 2)

for e being Point of (Euclid 2)

for r being real number st e = q & p in Ball (e,r) holds

( (q `2) - r < p `2 & p `2 < (q `2) + r )

for e being Point of (Euclid 2)

for r being real number st e = q & p in Ball (e,r) holds

( (q `2) - r < p `2 & p `2 < (q `2) + r )

proof end;

theorem Th49: :: TOPREAL6:49

for p being Point of (TOP-REAL 2)

for e being Point of (Euclid 2)

for r being real number 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)

for e being Point of (Euclid 2)

for r being real number 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 Th50: :: TOPREAL6:50

for p being Point of (TOP-REAL 2)

for e being Point of (Euclid 2)

for r being real number st p = e holds

Ball (e,r) c= product ((1,2) --> (].((p `1) - r),((p `1) + r).[,].((p `2) - r),((p `2) + r).[))

for e being Point of (Euclid 2)

for r being real number 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 Th51: :: TOPREAL6:51

for p being Point of (TOP-REAL 2)

for e being Point of (Euclid 2)

for P being Subset of (TOP-REAL 2)

for r being real number st P = Ball (e,r) & p = e holds

proj1 .: P = ].((p `1) - r),((p `1) + r).[

for e being Point of (Euclid 2)

for P being Subset of (TOP-REAL 2)

for r being real number st P = Ball (e,r) & p = e holds

proj1 .: P = ].((p `1) - r),((p `1) + r).[

proof end;

theorem Th52: :: TOPREAL6:52

for p being Point of (TOP-REAL 2)

for e being Point of (Euclid 2)

for P being Subset of (TOP-REAL 2)

for r being real number st P = Ball (e,r) & p = e holds

proj2 .: P = ].((p `2) - r),((p `2) + r).[

for e being Point of (Euclid 2)

for P being Subset of (TOP-REAL 2)

for r being real number st P = Ball (e,r) & p = e holds

proj2 .: P = ].((p `2) - r),((p `2) + r).[

proof end;

theorem :: TOPREAL6:53

for p being Point of (TOP-REAL 2)

for e being Point of (Euclid 2)

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) & p = e holds

W-bound D = (p `1) - r

for e being Point of (Euclid 2)

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) & p = e holds

W-bound D = (p `1) - r

proof end;

theorem :: TOPREAL6:54

for p being Point of (TOP-REAL 2)

for e being Point of (Euclid 2)

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) & p = e holds

E-bound D = (p `1) + r

for e being Point of (Euclid 2)

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) & p = e holds

E-bound D = (p `1) + r

proof end;

theorem :: TOPREAL6:55

for p being Point of (TOP-REAL 2)

for e being Point of (Euclid 2)

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) & p = e holds

S-bound D = (p `2) - r

for e being Point of (Euclid 2)

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) & p = e holds

S-bound D = (p `2) - r

proof end;

theorem :: TOPREAL6:56

for p being Point of (TOP-REAL 2)

for e being Point of (Euclid 2)

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) & p = e holds

N-bound D = (p `2) + r

for e being Point of (Euclid 2)

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) & p = e holds

N-bound D = (p `2) + r

proof end;

theorem :: TOPREAL6:57

for e being Point of (Euclid 2)

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) holds

not D is horizontal

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) holds

not D is horizontal

proof end;

theorem :: TOPREAL6:58

for e being Point of (Euclid 2)

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) holds

not D is vertical

for D being non empty Subset of (TOP-REAL 2)

for r being real number st D = Ball (e,r) holds

not D is vertical

proof end;

theorem :: TOPREAL6:59

for a being Real

for f being Point of (Euclid 2)

for 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)

for f being Point of (Euclid 2)

for 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)

proof end;

theorem :: TOPREAL6:60

for a being Real

for X being non empty compact Subset of (TOP-REAL 2)

for p being Point of (Euclid 2) st p = 0. (TOP-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))

for X being non empty compact Subset of (TOP-REAL 2)

for p being Point of (Euclid 2) st p = 0. (TOP-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))

proof end;

theorem Th61: :: TOPREAL6:61

for r being real number

for M being non empty Reflexive symmetric triangle MetrStruct

for z being Point of M st r < 0 holds

Sphere (z,r) = {}

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:62

for M being non empty Reflexive discerning MetrStruct

for z being Point of M holds Sphere (z,0) = {z}

for z being Point of M holds Sphere (z,0) = {z}

proof end;

theorem :: TOPREAL6:63

for r being real number

for M being non empty Reflexive symmetric triangle MetrStruct

for z being Point of M st r < 0 holds

cl_Ball (z,r) = {}

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:64

proof end;

Lm1: for M being non empty MetrSpace

for z being Point of M

for r being real number

for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds

A ` is open

proof end;

theorem Th65: :: TOPREAL6:65

for M being non empty MetrSpace

for z being Point of M

for r being real number

for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds

A is closed

for z being Point of M

for r being real number

for A being Subset of (TopSpaceMetr M) st A = cl_Ball (z,r) holds

A is closed

proof end;

theorem :: TOPREAL6:66

for n being Element of NAT

for w being Point of (Euclid n)

for A being Subset of (TOP-REAL n)

for r being real number st A = cl_Ball (w,r) holds

A is closed

for w being Point of (Euclid n)

for A being Subset of (TOP-REAL n)

for r being real number st A = cl_Ball (w,r) holds

A is closed

proof end;

theorem Th67: :: TOPREAL6:67

for r being real number

for M being non empty Reflexive symmetric triangle MetrStruct

for x being Element of M holds cl_Ball (x,r) is bounded

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 Th68: :: TOPREAL6:68

for M being non empty MetrSpace

for z being Point of M

for r being real number

for A being Subset of (TopSpaceMetr M) st A = Sphere (z,r) holds

A is closed

for z being Point of M

for r being real number

for A being Subset of (TopSpaceMetr M) st A = Sphere (z,r) holds

A is closed

proof end;

theorem :: TOPREAL6:69

for n being Element of NAT

for w being Point of (Euclid n)

for A being Subset of (TOP-REAL n)

for r being real number st A = Sphere (w,r) holds

A is closed

for w being Point of (Euclid n)

for A being Subset of (TOP-REAL n)

for r being real number st A = Sphere (w,r) holds

A is closed

proof end;

theorem :: TOPREAL6:70

for M being non empty MetrSpace

for z being Point of M

for r being real number holds Sphere (z,r) is bounded

for z being Point of M

for r being real number holds Sphere (z,r) is bounded

proof end;

theorem Th71: :: TOPREAL6:71

proof end;

theorem :: TOPREAL6:72

for M being non empty MetrStruct holds

( M is bounded iff for X being Subset of M holds X is bounded )

( M is bounded iff for X being Subset of M holds X is bounded )

proof end;

theorem Th73: :: TOPREAL6:73

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

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:74

for n being Element of NAT

for X, Y being Subset of (TOP-REAL n) st n >= 1 & the carrier of (TOP-REAL n) = X \/ Y & X is Bounded holds

not Y is Bounded

for X, Y being Subset of (TOP-REAL n) st n >= 1 & the carrier of (TOP-REAL n) = X \/ Y & X is Bounded holds

not Y is Bounded

proof end;

theorem :: TOPREAL6:75

canceled;

theorem Th76: :: TOPREAL6:76

for n being Element of NAT

for A, B being Subset of (TOP-REAL n) st A is Bounded & B is Bounded holds

A \/ B is Bounded

for A, B being Subset of (TOP-REAL n) st A is Bounded & B is Bounded holds

A \/ B is Bounded

proof end;

begin

registration

let X be non empty Subset of REAL;

cluster Cl X -> non empty ;

coherence

not Cl X is empty by MEASURE6:94, XBOOLE_1:3;

end;
cluster Cl X -> non empty ;

coherence

not Cl X is empty by MEASURE6:94, XBOOLE_1:3;

registration

let D be bounded_below Subset of REAL;

cluster Cl D -> bounded_below ;

coherence

Cl D is bounded_below

end;
cluster Cl D -> bounded_below ;

coherence

Cl D is bounded_below

proof end;

registration

let D be bounded_above Subset of REAL;

cluster Cl D -> bounded_above ;

coherence

Cl D is bounded_above

end;
cluster Cl D -> bounded_above ;

coherence

Cl D is bounded_above

proof end;

theorem Th77: :: TOPREAL6:77

proof end;

theorem Th78: :: TOPREAL6:78

proof end;

Lm2: R^1 = TopStruct(# the carrier of RealSpace,(Family_open_set RealSpace) #)

by PCOMPS_1:def 6, TOPMETR:def 7;

theorem Th79: :: TOPREAL6:79

proof end;

theorem :: TOPREAL6:80

proof end;

theorem Th81: :: TOPREAL6:81

for A being Subset of REAL

for B being Subset of R^1 st A = B holds

( A is compact iff B is compact )

for B being Subset of R^1 st A = B holds

( A is compact iff B is compact )

proof end;

registration

cluster finite -> compact Element of bool REAL;

coherence

for b_{1} being Subset of REAL st b_{1} is finite holds

b_{1} is compact
by Th81, TOPMETR:24;

end;
coherence

for b

b

registration

let a, b be real number ;

cluster K217(a,b) -> compact Subset of REAL;

coherence

for b_{1} being Subset of REAL st b_{1} = [.a,b.] holds

b_{1} is compact
by RCOMP_1:24;

end;
cluster K217(a,b) -> compact Subset of REAL;

coherence

for b

b

theorem :: TOPREAL6:82

proof end;

registration

cluster non empty finite V195() V196() V197() bounded Element of bool REAL;

existence

ex b_{1} being Subset of REAL st

( not b_{1} is empty & b_{1} is finite & b_{1} is bounded )

end;
existence

ex b

( not b

proof end;

theorem Th83: :: TOPREAL6:83

for T being TopStruct

for f being RealMap of T

for g being Function of T,R^1 st f = g holds

( f is continuous iff g is continuous )

for f being RealMap of T

for g being Function of T,R^1 st f = g holds

( f is continuous iff g is continuous )

proof end;

theorem Th84: :: TOPREAL6:84

for A, B being Subset of REAL

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 .: [:A,B:] = product ((1,2) --> (A,B))

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 .: [:A,B:] = product ((1,2) --> (A,B))

proof end;

theorem Th85: :: TOPREAL6:85

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

f is being_homeomorphism

proof end;

theorem :: TOPREAL6:86

proof end;

begin

theorem Th87: :: TOPREAL6:87

for A, B being compact Subset of REAL holds product ((1,2) --> (A,B)) is compact Subset of (TOP-REAL 2)

proof end;

theorem Th88: :: TOPREAL6:88

proof end;

theorem Th89: :: TOPREAL6:89

for P being Subset of (TOP-REAL 2) st P is Bounded holds

for g being continuous RealMap of (TOP-REAL 2) holds Cl (g .: P) c= g .: (Cl P)

for g being continuous RealMap of (TOP-REAL 2) holds Cl (g .: P) c= g .: (Cl P)

proof end;

theorem Th90: :: TOPREAL6:90

proof end;

theorem Th91: :: TOPREAL6:91

proof end;

theorem Th92: :: TOPREAL6:92

proof end;

theorem Th93: :: TOPREAL6:93

proof end;

theorem :: TOPREAL6:94

proof end;

theorem :: TOPREAL6:95

proof end;

theorem :: TOPREAL6:96

proof end;

theorem :: TOPREAL6:97

proof end;

theorem Th98: :: TOPREAL6:98

for n being Element of NAT

for A, B being Subset of (TOP-REAL n) st ( A is Bounded or B is Bounded ) holds

A /\ B is Bounded

for A, B being Subset of (TOP-REAL n) st ( A is Bounded or B is Bounded ) holds

A /\ B is Bounded

proof end;

theorem :: TOPREAL6:99

for n being Element of NAT

for A, B being Subset of (TOP-REAL n) st not A is Bounded & B is Bounded holds

not A \ B is Bounded

for A, B being Subset of (TOP-REAL n) st not A is Bounded & B is Bounded holds

not A \ B is Bounded

proof end;

begin

definition

let n be Element of NAT ;

let a, b be Point of (TOP-REAL n);

func dist (a,b) -> Real means :Def1: :: TOPREAL6:def 1

ex p, q being Point of (Euclid n) st

( p = a & q = b & it = dist (p,q) );

existence

ex b_{1} being Real ex p, q being Point of (Euclid n) st

( p = a & q = b & b_{1} = dist (p,q) )

for b_{1}, b_{2} being Real st ex p, q being Point of (Euclid n) st

( p = a & q = b & b_{1} = dist (p,q) ) & ex p, q being Point of (Euclid n) st

( p = a & q = b & b_{2} = dist (p,q) ) holds

b_{1} = b_{2}
;

commutativity

for b_{1} being Real

for a, b being Point of (TOP-REAL n) st ex p, q being Point of (Euclid n) st

( p = a & q = b & b_{1} = dist (p,q) ) holds

ex p, q being Point of (Euclid n) st

( p = b & q = a & b_{1} = dist (p,q) )
;

end;
let a, b be Point of (TOP-REAL n);

func dist (a,b) -> Real means :Def1: :: TOPREAL6:def 1

ex p, q being Point of (Euclid n) st

( p = a & q = b & it = dist (p,q) );

existence

ex b

( p = a & q = b & b

proof end;

uniqueness for b

( p = a & q = b & b

( p = a & q = b & b

b

commutativity

for b

for a, b being Point of (TOP-REAL n) st ex p, q being Point of (Euclid n) st

( p = a & q = b & b

ex p, q being Point of (Euclid n) st

( p = b & q = a & b

:: deftheorem Def1 defines dist TOPREAL6:def 1 :

for n being Element of NAT

for a, b being Point of (TOP-REAL n)

for b

( b

( p = a & q = b & b

theorem Th100: :: TOPREAL6:100

for r1, s1, r2, s2 being real number

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))

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))

proof end;

theorem Th101: :: TOPREAL6:101

for p, q being Point of (TOP-REAL 2) holds dist (p,q) = sqrt ((((p `1) - (q `1)) ^2) + (((p `2) - (q `2)) ^2))

proof end;

theorem :: TOPREAL6:102

proof end;

theorem :: TOPREAL6:103

for n being Element of NAT

for p, q, r being Point of (TOP-REAL n) holds dist (p,r) <= (dist (p,q)) + (dist (q,r))

for p, q, r being Point of (TOP-REAL n) holds dist (p,r) <= (dist (p,q)) + (dist (q,r))

proof end;

theorem :: TOPREAL6:104

for x1, x2, y1, y2 being real number

for 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)

for 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)

proof end;