:: BROUWER semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

set T2 = TOP-REAL 2;

Lm1: [#] (TOP-REAL 2) = the carrier of (TOP-REAL 2)
by PRE_TOPC:12;

definition
let S, T be non empty TopSpace;
func DiffElems S,T -> Subset of [:S,T:] equals :: BROUWER:def 1
{ [s,t] where s is Point of S, t is Point of T : s <> t } ;
coherence
{ [s,t] where s is Point of S, t is Point of T : s <> t } is Subset of [:S,T:]
proof end;
end;

:: 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 :: BROUWER:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S, T being non empty TopSpace
for x being set holds
( x in DiffElems S,T iff ex s being Point of S ex t being Point of T st
( x = [s,t] & s <> t ) ) ;

registration
let S be non empty non trivial TopSpace;
let T be non empty TopSpace;
cluster DiffElems S,T -> non empty ;
coherence
not DiffElems S,T is empty
proof end;
end;

registration
let S be non empty TopSpace;
let T be non empty non trivial TopSpace;
cluster DiffElems S,T -> non empty ;
coherence
not DiffElems S,T is empty
proof end;
end;

theorem Th2: :: BROUWER:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for x being Point of (TOP-REAL n) holds cl_Ball x,0 = {x}
proof end;

definition
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real number ;
func Tdisk x,r -> SubSpace of TOP-REAL n equals :: BROUWER:def 2
(TOP-REAL n) | (cl_Ball x,r);
coherence
(TOP-REAL n) | (cl_Ball x,r) is SubSpace of TOP-REAL n
;
end;

:: deftheorem defines Tdisk BROUWER:def 2 :
for n being 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);

registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real non negative number ;
cluster Tdisk x,r -> non empty ;
coherence
not Tdisk x,r is empty
;
end;

theorem Th3: :: BROUWER:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real number
for x being Point of (TOP-REAL n) holds the carrier of (Tdisk x,r) = cl_Ball x,r
proof end;

registration
let n be Nat;
let x be Point of (TOP-REAL n);
let r be real number ;
cluster Tdisk x,r -> convex ;
coherence
Tdisk x,r is convex
proof end;
end;

theorem Th4: :: BROUWER:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real non negative number
for s, t, x being Point of (TOP-REAL n) st s <> t & s is Point of (Tdisk x,r) & s is not Point of (Tcircle x,r) holds
ex e being Point of (Tcircle x,r) st {e} = (halfline s,t) /\ (Sphere x,r)
proof end;

theorem Th5: :: BROUWER:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being real non negative number
for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle x,r) & t is Point of (Tdisk x,r) holds
ex e being Point of (Tcircle x,r) st
( e <> s & {s,e} = (halfline s,t) /\ (Sphere x,r) )
proof end;

definition
let n be non empty Nat;
let o be Point of (TOP-REAL n);
let s, t be Point of (TOP-REAL n);
let r be real non negative 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: :: BROUWER:def 3
( 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 )
proof end;
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
proof end;
end;

:: deftheorem Def3 defines HC BROUWER:def 3 :
for n being non empty Nat
for o, s, t being Point of (TOP-REAL n)
for r being real non negative 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: :: BROUWER:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real non negative number
for n being non empty Nat
for s, o, t being Point of (TOP-REAL n) st s is Point of (Tdisk o,r) & t is Point of (Tdisk o,r) & s <> t holds
HC s,t,o,r is Point of (Tcircle o,r)
proof end;

theorem :: BROUWER:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for r being real non negative number
for n being non empty 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)
proof end;

theorem Th8: :: BROUWER:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a being real number
for r being real non negative 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))]|
proof end;

definition
let n be non empty Nat;
let o be Point of (TOP-REAL n);
let r be real non negative 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: :: BROUWER:def 4
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 )
proof end;
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 Nat
for o being Point of (TOP-REAL n)
for r being real non negative 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: :: BROUWER:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real non negative number
for n being non empty Nat
for o being Point of (TOP-REAL n)
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 & x is Point of (Tcircle o,r) holds
HC x,f = x
proof end;

theorem Th10: :: BROUWER:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real positive number
for o being Point of (TOP-REAL 2)
for Y being non empty SubSpace of Tdisk o,r st Y = Tcircle o,r holds
not Y is_a_retract_of Tdisk o,r
proof end;

definition
let n be non empty Nat;
let r be real non negative 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: :: BROUWER:def 5
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
proof end;
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
proof end;
end;

:: deftheorem Def5 defines BR-map BROUWER:def 5 :
for n being non empty Nat
for r being real non negative 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: :: BROUWER:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real non negative number
for n being non empty Nat
for o being Point of (TOP-REAL n)
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 & x is Point of (Tcircle o,r) holds
(BR-map f) . x = x
proof end;

theorem :: BROUWER:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real non negative number
for n being non empty Nat
for o being Point of (TOP-REAL n)
for f being continuous Function of (Tdisk o,r),(Tdisk o,r) st f has_no_fixpoint holds
(BR-map f) | (Sphere o,r) = id (Tcircle o,r)
proof end;

Lm2: now
let T be non empty TopSpace; :: thesis: for a being Real holds the carrier of T --> a is continuous
let a be Real; :: thesis: the carrier of T --> a is continuous
set c = the carrier of T;
set f = the carrier of T --> a;
thus the carrier of T --> a is continuous :: thesis: verum
proof
A1: dom (the carrier of T --> a) = the carrier of T by FUNCT_2:def 1;
A2: rng (the carrier of T --> a) = {a} by FUNCOP_1:14;
let Y be Subset of REAL ; :: according to PSCOMP_1:def 25 :: thesis: ( not Y is closed or (the carrier of T --> a) " Y is closed )
assume Y is closed ; :: thesis: (the carrier of T --> a) " Y is closed
per cases ( a in Y or not a in Y ) ;
suppose a in Y ; :: thesis: (the carrier of T --> a) " Y is closed
then A3: rng (the carrier of T --> a) c= Y by A2, ZFMISC_1:37;
(the carrier of T --> a) " Y = (the carrier of T --> a) " ((rng (the carrier of T --> a)) /\ Y) by RELAT_1:168
.= (the carrier of T --> a) " (rng (the carrier of T --> a)) by A3, XBOOLE_1:28
.= the carrier of T by A1, RELAT_1:169
.= [#] T by PRE_TOPC:12 ;
hence (the carrier of T --> a) " Y is closed ; :: thesis: verum
end;
suppose not a in Y ; :: thesis: (the carrier of T --> a) " Y is closed
then A4: rng (the carrier of T --> a) misses Y by A2, ZFMISC_1:56;
(the carrier of T --> a) " Y = (the carrier of T --> a) " ((rng (the carrier of T --> a)) /\ Y) by RELAT_1:168
.= (the carrier of T --> a) " {} by A4, XBOOLE_0:def 7
.= {} T by RELAT_1:171 ;
hence (the carrier of T --> a) " Y is closed ; :: thesis: verum
end;
end;
end;
end;

theorem Th13: :: BROUWER:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real positive number
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk o,r),(Tdisk o,r) st f has_no_fixpoint holds
BR-map f is continuous
proof end;

theorem Th14: :: BROUWER:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real non negative number
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk o,r),(Tdisk o,r) holds f has_a_fixpoint
proof end;

theorem :: BROUWER:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r being real non negative number
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk o,r),(Tdisk o,r) ex x being Point of (Tdisk o,r) st f . x = x
proof end;