begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
canceled;
theorem
canceled;
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
definition
func Out_In_Sq -> Function of
NonZero (TOP-REAL 2),
NonZero (TOP-REAL 2) means :
Def1:
for
p being
Point of st
p <> 0. (TOP-REAL 2) holds
( ( ( (
p `2 <= p `1 &
- (p `1 ) <= p `2 ) or (
p `2 >= p `1 &
p `2 <= - (p `1 ) ) ) implies
it . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( (
p `2 <= p `1 &
- (p `1 ) <= p `2 ) or (
p `2 >= p `1 &
p `2 <= - (p `1 ) ) or
it . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) );
existence
ex b1 being Function of NonZero (TOP-REAL 2), NonZero (TOP-REAL 2) st
for p being Point of st p <> 0. (TOP-REAL 2) holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies b1 . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or b1 . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) )
uniqueness
for b1, b2 being Function of NonZero (TOP-REAL 2), NonZero (TOP-REAL 2) st ( for p being Point of st p <> 0. (TOP-REAL 2) holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies b1 . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or b1 . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) ) & ( for p being Point of st p <> 0. (TOP-REAL 2) holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies b2 . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or b2 . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Out_In_Sq JGRAPH_2:def 1 :
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
Lm1:
0. (TOP-REAL 2) = 0.REAL 2
by EUCLID:70;
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
for
K0,
B0 being
Subset of
for
f being
Function of
((TOP-REAL 2) | K0),
((TOP-REAL 2) | B0) for
f1,
f2 being
Function of
((TOP-REAL 2) | K0),
R^1 st
f1 is
continuous &
f2 is
continuous &
K0 <> {} &
B0 <> {} & ( for
x,
y,
r,
s being
real number st
|[x,y]| in K0 &
r = f1 . |[x,y]| &
s = f2 . |[x,y]| holds
f . |[x,y]| = |[r,s]| ) holds
f is
continuous
theorem Th46:
theorem Th47:
scheme
TopCompl{
P1[
set ],
F1()
-> Subset of } :
F1()
` = { p where p is Point of : P1[p] }
provided
A1:
F1()
= { p where p is Point of : P1[p] }
Lm2:
now
let p01,
p02,
px1,
px2 be
real number ;
( (p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4)) implies (p01 - p02) / 2 <= px1 - px2 )set r0 =
(p01 - p02) / 4;
assume
(p01 - px1) - (p02 - px2) <= ((p01 - p02) / 4) - (- ((p01 - p02) / 4))
;
(p01 - p02) / 2 <= px1 - px2then
(p01 - p02) - (px1 - px2) <= ((p01 - p02) / 4) + ((p01 - p02) / 4)
;
then
p01 - p02 <= (px1 - px2) + (((p01 - p02) / 4) + ((p01 - p02) / 4))
by XREAL_1:22;
then
(p01 - p02) - ((p01 - p02) / 2) <= px1 - px2
by XREAL_1:22;
hence
(p01 - p02) / 2
<= px1 - px2
;
verum
end;
deffunc H1( Point of ) -> Element of REAL = $1 `1 ;
deffunc H2( Point of ) -> Element of REAL = $1 `2 ;
Lm3:
for p, q being Point of holds
( H1(p - q) = H1(p) - H1(q) & H2(p - q) = H2(p) - H2(q) )
by TOPREAL3:8;
Lm4:
for p, q being Point of holds |.(p - q).| ^2 = (H1(p - q) ^2 ) + (H2(p - q) ^2 )
by JGRAPH_1:46;
Lm5:
{ p7 where p7 is Point of : H1(p7) <= H2(p7) } is closed Subset of
from JGRAPH_2:sch 3(Lm3, Lm4);
Lm6:
for p, q being Point of holds
( H2(p - q) = H2(p) - H2(q) & H1(p - q) = H1(p) - H1(q) )
by TOPREAL3:8;
Lm7:
for p, q being Point of holds |.(p - q).| ^2 = (H2(p - q) ^2 ) + (H1(p - q) ^2 )
by JGRAPH_1:46;
Lm8:
{ p7 where p7 is Point of : H2(p7) <= H1(p7) } is closed Subset of
from JGRAPH_2:sch 3(Lm6, Lm7);
deffunc H3( Point of ) -> Element of REAL = - ($1 `1 );
deffunc H4( Point of ) -> Element of REAL = - ($1 `2 );
Lm9:
now
let p,
q be
Point of ;
( H3(p - q) = H3(p) - H3(q) & H2(p - q) = H2(p) - H2(q) )thus H3(
p - q) =
- ((p `1 ) - (q `1 ))
by TOPREAL3:8
.=
H3(
p)
- H3(
q)
;
H2(p - q) = H2(p) - H2(q)thus
H2(
p - q)
= H2(
p)
- H2(
q)
by TOPREAL3:8;
verum
end;
Lm11:
{ p7 where p7 is Point of : H3(p7) <= H2(p7) } is closed Subset of
from JGRAPH_2:sch 3(Lm9, Lm10);
Lm12:
now
let p,
q be
Point of ;
( H2(p - q) = H2(p) - H2(q) & H3(p - q) = H3(p) - H3(q) )thus
H2(
p - q)
= H2(
p)
- H2(
q)
by TOPREAL3:8;
H3(p - q) = H3(p) - H3(q)thus H3(
p - q) =
- ((p `1 ) - (q `1 ))
by TOPREAL3:8
.=
H3(
p)
- H3(
q)
;
verum
end;
Lm14:
{ p7 where p7 is Point of : H2(p7) <= H3(p7) } is closed Subset of
from JGRAPH_2:sch 3(Lm12, Lm13);
Lm15:
now
let p,
q be
Point of ;
( H4(p - q) = H4(p) - H4(q) & H1(p - q) = H1(p) - H1(q) )thus H4(
p - q) =
- ((p `2 ) - (q `2 ))
by TOPREAL3:8
.=
H4(
p)
- H4(
q)
;
H1(p - q) = H1(p) - H1(q)thus
H1(
p - q)
= H1(
p)
- H1(
q)
by TOPREAL3:8;
verum
end;
Lm17:
{ p7 where p7 is Point of : H4(p7) <= H1(p7) } is closed Subset of
from JGRAPH_2:sch 3(Lm15, Lm16);
Lm18:
now
let p,
q be
Point of ;
( H1(p - q) = H1(p) - H1(q) & H4(p - q) = H4(p) - H4(q) )thus
H1(
p - q)
= H1(
p)
- H1(
q)
by TOPREAL3:8;
H4(p - q) = H4(p) - H4(q)thus H4(
p - q) =
- ((p `2 ) - (q `2 ))
by TOPREAL3:8
.=
H4(
p)
- H4(
q)
;
verum
end;
Lm20:
{ p7 where p7 is Point of : H1(p7) <= H4(p7) } is closed Subset of
from JGRAPH_2:sch 3(Lm18, Lm19);
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
definition
let A,
B,
C,
D be
real number ;
func AffineMap A,
B,
C,
D -> Function of
(TOP-REAL 2),
(TOP-REAL 2) means :
Def2:
for
t being
Point of holds
it . t = |[((A * (t `1 )) + B),((C * (t `2 )) + D)]|;
existence
ex b1 being Function of (TOP-REAL 2),(TOP-REAL 2) st
for t being Point of holds b1 . t = |[((A * (t `1 )) + B),((C * (t `2 )) + D)]|
uniqueness
for b1, b2 being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for t being Point of holds b1 . t = |[((A * (t `1 )) + B),((C * (t `2 )) + D)]| ) & ( for t being Point of holds b2 . t = |[((A * (t `1 )) + B),((C * (t `2 )) + D)]| ) holds
b1 = b2
end;
:: deftheorem Def2 defines AffineMap JGRAPH_2:def 2 :
theorem Th54:
theorem
theorem
theorem
theorem