begin
set T2 = TOP-REAL 2;
:: deftheorem defines DiffElems BROUWER:def 1 :
for S, T being non empty TopSpace holds DiffElems (S,T) = { [s,t] where s is Point of S, t is Point of T : s <> t } ;
theorem
theorem Th2:
:: deftheorem defines Tdisk BROUWER:def 2 :
for n being Element of NAT
for x being Point of (TOP-REAL n)
for r being real number holds Tdisk (x,r) = (TOP-REAL n) | (cl_Ball (x,r));
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 :
for n being non empty Element of NAT
for o, s, t being Point of (TOP-REAL n)
for r being non negative real number st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds
for b6 being Point of (TOP-REAL n) holds
( b6 = HC (s,t,o,r) iff ( b6 in (halfline (s,t)) /\ (Sphere (o,r)) & b6 <> s ) );
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 :
for n being non empty Element of NAT
for r being non negative real number
for o being Point of (TOP-REAL n)
for f being Function of (Tdisk (o,r)),(Tdisk (o,r))
for b5 being Function of (Tdisk (o,r)),(Tcircle (o,r)) holds
( b5 = BR-map f iff for x being Point of (Tdisk (o,r)) holds b5 . x = HC (x,f) );
theorem Th11:
theorem
theorem Th13:
theorem Th14:
theorem