begin
set T2 = TOP-REAL 2;
:: deftheorem defines DiffElems BROUWER:def 1 :
theorem
theorem Th2:
:: deftheorem defines Tdisk BROUWER:def 2 :
theorem Th3:
theorem Th4:
theorem Th5:
definition
let n be non
empty Element of
NAT ;
let o be
Point of
(TOP-REAL n);
let s,
t be
Point of
(TOP-REAL n);
let r be non
negative real number ;
assume that A1:
s is
Point of
(Tdisk o,r)
and A2:
t is
Point of
(Tdisk o,r)
and A3:
s <> t
;
func HC s,
t,
o,
r -> Point of
(TOP-REAL n) means :
Def3:
(
it in (halfline s,t) /\ (Sphere o,r) &
it <> s );
existence
ex b1 being Point of (TOP-REAL n) st
( b1 in (halfline s,t) /\ (Sphere o,r) & b1 <> s )
uniqueness
for b1, b2 being Point of (TOP-REAL n) st b1 in (halfline s,t) /\ (Sphere o,r) & b1 <> s & b2 in (halfline s,t) /\ (Sphere o,r) & b2 <> s holds
b1 = b2
end;
:: deftheorem Def3 defines HC BROUWER:def 3 :
theorem Th6:
theorem
for
a being
real number for
r being non
negative real number for
n being non
empty Element of
NAT for
s,
t,
o being
Point of
(TOP-REAL n) for
S,
T,
O being
Element of
REAL n st
S = s &
T = t &
O = o &
s is
Point of
(Tdisk o,r) &
t is
Point of
(Tdisk o,r) &
s <> t &
a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2 ) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2 )))))) / (Sum (sqr (T - S))) holds
HC s,
t,
o,
r = ((1 - a) * s) + (a * t)
theorem Th8:
for
a being
real number for
r being non
negative real number for
r1,
r2,
s1,
s2 being
real number for
s,
t,
o being
Point of
(TOP-REAL 2) st
s is
Point of
(Tdisk o,r) &
t is
Point of
(Tdisk o,r) &
s <> t &
r1 = (t `1 ) - (s `1 ) &
r2 = (t `2 ) - (s `2 ) &
s1 = (s `1 ) - (o `1 ) &
s2 = (s `2 ) - (o `2 ) &
a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2 ) - (((r1 ^2 ) + (r2 ^2 )) * (((s1 ^2 ) + (s2 ^2 )) - (r ^2 )))))) / ((r1 ^2 ) + (r2 ^2 )) holds
HC s,
t,
o,
r = |[((s `1 ) + (a * r1)),((s `2 ) + (a * r2))]|
definition
let n be non
empty Element of
NAT ;
let o be
Point of
(TOP-REAL n);
let r be non
negative real number ;
let x be
Point of
(Tdisk o,r);
let f be
Function of
(Tdisk o,r),
(Tdisk o,r);
assume A1:
not
x is_a_fixpoint_of f
;
func HC x,
f -> Point of
(Tcircle o,r) means :
Def4:
ex
y,
z being
Point of
(TOP-REAL n) st
(
y = x &
z = f . x &
it = HC z,
y,
o,
r );
existence
ex b1 being Point of (Tcircle o,r) ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & b1 = HC z,y,o,r )
uniqueness
for b1, b2 being Point of (Tcircle o,r) st ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & b1 = HC z,y,o,r ) & ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & b2 = HC z,y,o,r ) holds
b1 = b2
;
end;
:: deftheorem Def4 defines HC BROUWER:def 4 :
for
n being non
empty Element of
NAT for
o being
Point of
(TOP-REAL n) for
r being non
negative real number for
x being
Point of
(Tdisk o,r) for
f being
Function of
(Tdisk o,r),
(Tdisk o,r) st not
x is_a_fixpoint_of f holds
for
b6 being
Point of
(Tcircle o,r) holds
(
b6 = HC x,
f iff ex
y,
z being
Point of
(TOP-REAL n) st
(
y = x &
z = f . x &
b6 = HC z,
y,
o,
r ) );
theorem Th9:
theorem Th10:
definition
let n be non
empty Element of
NAT ;
let r be non
negative real number ;
let o be
Point of
(TOP-REAL n);
let f be
Function of
(Tdisk o,r),
(Tdisk o,r);
func BR-map f -> Function of
(Tdisk o,r),
(Tcircle o,r) means :
Def5:
for
x being
Point of
(Tdisk o,r) holds
it . x = HC x,
f;
existence
ex b1 being Function of (Tdisk o,r),(Tcircle o,r) st
for x being Point of (Tdisk o,r) holds b1 . x = HC x,f
uniqueness
for b1, b2 being Function of (Tdisk o,r),(Tcircle o,r) st ( for x being Point of (Tdisk o,r) holds b1 . x = HC x,f ) & ( for x being Point of (Tdisk o,r) holds b2 . x = HC x,f ) holds
b1 = b2
end;
:: deftheorem Def5 defines BR-map BROUWER:def 5 :
theorem Th11:
theorem
theorem Th13:
theorem Th14:
theorem