:: TOPREAL6 semantic presentation

Lm1: sqrt 2 > 0
by SQUARE_1:84;

theorem :: TOPREAL6:1

canceled;

theorem :: TOPREAL6:2

canceled;

theorem :: TOPREAL6:3

canceled;

theorem :: TOPREAL6:4

canceled;

theorem :: TOPREAL6:5

canceled;

theorem Th6: :: TOPREAL6:6

for a, b being real number st 0 <= a & 0 <= b holds
sqrt (a + b) <= (sqrt a) + (sqrt b)

proof end;

theorem Th7: :: TOPREAL6:7

for a, b being real number st 0 <= a & a <= b holds
abs a <= abs b

proof end;

theorem Th8: :: TOPREAL6:8

for b, a being real number st b <= a & a <= 0 holds
abs a <= abs b

proof end;

theorem :: TOPREAL6:9

for r being Real holds Product (0 |-> r) = 1 by FINSEQ_2:72, RVSUM_1:124;

theorem Th10: :: TOPREAL6:10

for r being Real holds Product (1 |-> r) = r

proof end;

theorem :: TOPREAL6:11

for r being Real holds Product (2 |-> r) = r * r

proof end;

theorem Th12: :: TOPREAL6:12

for r being Real
for n being Nat holds Product ((n + 1) |-> r) = (Product (n |-> r)) * r

proof end;

theorem Th13: :: TOPREAL6:13

for r being Real
for j being Nat holds
( ( j <> 0 & r = 0 ) iff Product (j |-> r) = 0 )

proof end;

theorem Th14: :: TOPREAL6:14

for r being Real
for j, i being 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 Nat st r <> 0 & j <= i holds
r |^ (i -' j) = (r |^ i) / (r |^ j)

proof end;

theorem Th16: :: TOPREAL6:16

for a, b being Real holds sqr <*a,b*> = <*(a ^2 ),(b ^2 )*>

proof end;

theorem Th17: :: TOPREAL6:17

for i being Nat
for a being Real
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

for a, b being Real holds abs <*a,b*> = <*(abs a),(abs b)*>

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)

proof end;

theorem Th20: :: TOPREAL6:20

for a, r being real number st r > 0 holds
a in ].(a - r),(a + r).[

proof end;

theorem :: TOPREAL6:21

for a, r being real number st r >= 0 holds
a in [.(a - r),(a + r).]

proof end;

theorem Th22: :: TOPREAL6:22

for a, b being real number st a < b holds
( inf ].a,b.[ = a & sup ].a,b.[ = b )

proof end;

theorem :: TOPREAL6:23

canceled;

theorem Th24: :: TOPREAL6:24

for A being bounded Subset of REAL holds A c= [.(inf A),(sup A).]

proof end;

registration

let T be TopStruct ;
let A be finite Subset of T;
cluster T | A -> finite ;
coherence

proof end;

end;

registration

cluster non empty strict finite TopStruct ;
existence

proof end;

end;

registration

let T be TopStruct ;
cluster empty -> connected Element of bool the carrier of T;
coherence

proof end;

end;

registration

let T be TopSpace;
cluster finite -> compact Element of bool the carrier of T;
coherence

proof end;

end;

theorem Th25: :: TOPREAL6:25

for S, T being TopSpace st S,T are_homeomorphic & S is connected holds
T is connected

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

proof end;

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)

proof end;

theorem Th30: :: TOPREAL6:30

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

proof end;

theorem :: TOPREAL6:31

for a being Real holds
( |.|[0,a]|.| = abs a & |.|[a,0]|.| = abs a )

proof end;

theorem Th32: :: TOPREAL6:32

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

proof end;

theorem Th34: :: TOPREAL6:34

for r being Real
for p being Point of (TOP-REAL 2) holds r * p = |[(r * (p `1 )),(r * (p `2 ))]|

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

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

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 )

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 )

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 )

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 )

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 )

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 )

proof end;

registration

cluster non empty convex -> connected Element of bool the carrier of (TOP-REAL 2);
coherence by JORDAN1:9;
cluster non horizontal -> non empty Element of bool the carrier of (TOP-REAL 2);
coherence

proof end;

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

proof end;

cluster being_Region -> open connected Element of bool the carrier of (TOP-REAL 2);
coherence by TOPREAL4:def 3;
cluster open connected -> being_Region Element of bool the carrier of (TOP-REAL 2);
coherence by TOPREAL4:def 3;

end;

registration

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

proof end;

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

proof end;

end;

registration

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

proof end;

end;

registration

let a, b be Point of (TOP-REAL 2);
cluster LSeg a,b -> connected convex ;
coherence by GOBOARD9:7, GOBOARD9:8;

end;

registration

cluster R^2-unit_square -> connected ;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem :: TOPREAL6:43

for P being Subset of (TOP-REAL 2) holds LSeg (NE-corner P),(SE-corner P) c= L~ (SpStSeq P)

proof end;

theorem :: TOPREAL6:44

for P being Subset of (TOP-REAL 2) holds LSeg (SW-corner P),(SE-corner P) c= L~ (SpStSeq P)

proof end;

theorem :: TOPREAL6:45

for P being Subset of (TOP-REAL 2) holds LSeg (SW-corner P),(NW-corner P) c= L~ (SpStSeq P)

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;

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 )

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 )

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

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

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

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

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

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

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

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

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

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

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

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.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 = {}

proof end;

theorem :: TOPREAL6:62

for M being non empty Reflexive discerning MetrStruct
for z being Point of M holds Sphere z,0 = {z}

proof end;

theorem Th63: :: 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 = {}

proof end;

theorem Th64: :: TOPREAL6:64

for M being non empty MetrSpace
for z being Point of M holds cl_Ball z,0 = {z}

proof end;

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

proof end;

theorem Th66: :: TOPREAL6:66

for n being 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 by Th65;

theorem Th67: :: TOPREAL6:67

for M being non empty MetrSpace
for z being Point of M
for r being real number holds cl_Ball z,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

proof end;

theorem :: TOPREAL6:69

for n being 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 by Th68;

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

proof end;

theorem Th71: :: TOPREAL6:71

for n being Nat
for A being Subset of (TOP-REAL n) st A is Bounded holds
Cl A is Bounded

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 )

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

proof end;

theorem :: TOPREAL6:74

for n being 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

proof end;

theorem :: TOPREAL6:75

canceled;

theorem :: TOPREAL6:76

for n being Nat
for A, B being Subset of (TOP-REAL n) 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

proof end;

end;

registration

let D be bounded_below Subset of REAL ;
cluster Cl D -> bounded_below ;
coherence

proof end;

end;

registration

let D be bounded_above Subset of REAL ;
cluster Cl D -> bounded_above ;
coherence

proof end;

end;

theorem Th77: :: TOPREAL6:77

for D being non empty bounded_below Subset of REAL holds inf D = inf (Cl D)

proof end;

theorem Th78: :: TOPREAL6:78

for D being non empty bounded_above Subset of REAL holds sup D = sup (Cl D)

proof end;

registration

cluster R^1 -> being_T2 ;
coherence by PCOMPS_1:38, TOPMETR:def 7;

end;

Lm3: R^1 = TopStruct(# the carrier of RealSpace ,(Family_open_set RealSpace ) #)
by PCOMPS_1:def 6, TOPMETR:def 7;

theorem Th79: :: TOPREAL6:79

for A being Subset of REAL
for B being Subset of R^1 st A = B holds
( A is closed iff B is closed )

proof end;

theorem :: TOPREAL6:80

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

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 )

proof end;

registration

cluster finite -> compact Element of bool REAL ;
coherence

proof end;

end;

registration

let a, b be real number ;
cluster [.a,b.] -> compact ;
coherence by RCOMP_1:24;

end;

theorem :: TOPREAL6:82

for a, b being real number holds
( a <> b iff Cl ].a,b.[ = [.a,b.] )

proof end;

registration

cluster non empty finite bounded compact Element of bool REAL ;
existence

proof end;

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 )

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)

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_homeomorphism

proof end;

theorem :: TOPREAL6:86

[:R^1 ,R^1 :], TOP-REAL 2 are_homeomorphic

proof end;

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

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

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)

proof end;

theorem Th90: :: TOPREAL6:90

for P being Subset of (TOP-REAL 2) holds proj1 .: (Cl P) c= Cl (proj1 .: P)

proof end;

theorem Th91: :: TOPREAL6:91

for P being Subset of (TOP-REAL 2) holds proj2 .: (Cl P) c= Cl (proj2 .: P)

proof end;

theorem Th92: :: TOPREAL6:92

for P being Subset of (TOP-REAL 2) st P is Bounded holds
Cl (proj1 .: P) = proj1 .: (Cl P)

proof end;

theorem Th93: :: TOPREAL6:93

for P being Subset of (TOP-REAL 2) st P is Bounded holds
Cl (proj2 .: P) = proj2 .: (Cl P)

proof end;

theorem :: TOPREAL6:94

for D being non empty Subset of (TOP-REAL 2) st D is Bounded holds
W-bound D = W-bound (Cl D)

proof end;

theorem :: TOPREAL6:95

for D being non empty Subset of (TOP-REAL 2) st D is Bounded holds
E-bound D = E-bound (Cl D)

proof end;

theorem :: TOPREAL6:96

for D being non empty Subset of (TOP-REAL 2) st D is Bounded holds
N-bound D = N-bound (Cl D)

proof end;

theorem :: TOPREAL6:97

for D being non empty Subset of (TOP-REAL 2) st D is Bounded holds
S-bound D = S-bound (Cl D)

proof end;