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 ;
let s,
t be
Point of ;
let r be non
negative real number ;
assume that A1:
s is
Point of
and A2:
t is
Point of
and A3:
s <> t
;
func HC s,
t,
o,
r -> Point of
means :
Def3:
(
it in (halfline s,t) /\ (Sphere o,r) &
it <> s );
existence
ex b1 being Point of st
( b1 in (halfline s,t) /\ (Sphere o,r) & b1 <> s )
uniqueness
for b1, b2 being Point of 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
theorem Th8:
definition
let n be non
empty Element of
NAT ;
let o be
Point of ;
let r be non
negative real number ;
let x be
Point of ;
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
means :
Def4:
ex
y,
z being
Point of st
(
y = x &
z = f . x &
it = HC z,
y,
o,
r );
existence
ex b1 being Point of ex y, z being Point of st
( y = x & z = f . x & b1 = HC z,y,o,r )
uniqueness
for b1, b2 being Point of st ex y, z being Point of st
( y = x & z = f . x & b1 = HC z,y,o,r ) & ex y, z being Point of st
( y = x & z = f . x & b2 = HC z,y,o,r ) holds
b1 = b2
;
end;
:: deftheorem Def4 defines HC BROUWER:def 4 :
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 ;
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 holds
it . x = HC x,
f;
existence
ex b1 being Function of (Tdisk o,r),(Tcircle o,r) st
for x being Point of 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 holds b1 . x = HC x,f ) & ( for x being Point of 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