:: BROUWER semantic presentation

set c1 = TOP-REAL 2;

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

definition
let c2, c3 be non empty TopSpace;
func DiffElems c1,c2 -> Subset of [:a1,a2:] equals :: BROUWER:def 1
{ [b1,b2] where B is Point of a1, B is Point of a2 : b1 <> b2 } ;
coherence
{ [b1,b2] where B is Point of c2, B is Point of c3 : b1 <> b2 } is Subset of [:c2,c3:]
proof end;
end;

:: deftheorem Def1 defines DiffElems BROUWER:def 1 :
for b1, b2 being non empty TopSpace holds DiffElems b1,b2 = { [b3,b4] where B is Point of b1, B is Point of b2 : b3 <> b4 } ;

theorem Th1: :: BROUWER:1
for b1, b2 being non empty TopSpace
for b3 being set holds
( b3 in DiffElems b1,b2 iff ex b4 being Point of b1ex b5 being Point of b2 st
( b3 = [b4,b5] & b4 <> b5 ) ) ;

registration
let c2 be non empty non trivial TopSpace;
let c3 be non empty TopSpace;
cluster DiffElems a1,a2 -> non empty ;
coherence
not DiffElems c2,c3 is empty
proof end;
end;

registration
let c2 be non empty TopSpace;
let c3 be non empty non trivial TopSpace;
cluster DiffElems a1,a2 -> non empty ;
coherence
not DiffElems c2,c3 is empty
proof end;
end;

theorem Th2: :: BROUWER:2
for b1 being Nat
for b2 being Point of (TOP-REAL b1) holds cl_Ball b2,0 = {b2}
proof end;

definition
let c2 be Nat;
let c3 be Point of (TOP-REAL c2);
let c4 be real number ;
func Tdisk c2,c3 -> SubSpace of TOP-REAL a1 equals :: BROUWER:def 2
(TOP-REAL a1) | (cl_Ball a2,a3);
coherence
(TOP-REAL c2) | (cl_Ball c3,c4) is SubSpace of TOP-REAL c2 ;
end;

:: deftheorem Def2 defines Tdisk BROUWER:def 2 :
for b1 being Nat
for b2 being Point of (TOP-REAL b1)
for b3 being real number holds Tdisk b2,b3 = (TOP-REAL b1) | (cl_Ball b2,b3);

registration
let c2 be Nat;
let c3 be Point of (TOP-REAL c2);
let c4 be real non negative number ;
cluster Tdisk a2,a3 -> non empty ;
coherence
not Tdisk c3,c4 is empty ;
end;

theorem Th3: :: BROUWER:3
for b1 being Nat
for b2 being real number
for b3 being Point of (TOP-REAL b1) holds the carrier of (Tdisk b3,b2) = cl_Ball b3,b2
proof end;

registration
let c2 be Nat;
let c3 be Point of (TOP-REAL c2);
let c4 be real number ;
cluster Tdisk a2,a3 -> convex ;
coherence
Tdisk c3,c4 is convex
proof end;
end;

theorem Th4: :: BROUWER:4
for b1 being Nat
for b2 being real non negative number
for b3, b4, b5 being Point of (TOP-REAL b1) st b3 <> b4 & b3 is Point of (Tdisk b5,b2) & b3 is not Point of (Tcircle b5,b2) holds
ex b6 being Point of (Tcircle b5,b2) st {b6} = (halfline b3,b4) /\ (Sphere b5,b2)
proof end;

theorem Th5: :: BROUWER:5
for b1 being Nat
for b2 being real non negative number
for b3, b4, b5 being Point of (TOP-REAL b1) st b3 <> b4 & b3 in the carrier of (Tcircle b5,b2) & b4 is Point of (Tdisk b5,b2) holds
ex b6 being Point of (Tcircle b5,b2) st
( b6 <> b3 & {b3,b6} = (halfline b3,b4) /\ (Sphere b5,b2) )
proof end;

definition
let c2 be non empty Nat;
let c3 be Point of (TOP-REAL c2);
let c4, c5 be Point of (TOP-REAL c2);
let c6 be real non negative number ;
assume that
E6: c4 is Point of (Tdisk c3,c6) and
E7: c5 is Point of (Tdisk c3,c6) and
E8: c4 <> c5 ;
func HC c3,c4,c2,c5 -> Point of (TOP-REAL a1) means :Def3: :: BROUWER:def 3
( a6 in (halfline a3,a4) /\ (Sphere a2,a5) & a6 <> a3 );
existence
ex b1 being Point of (TOP-REAL c2) st
( b1 in (halfline c4,c5) /\ (Sphere c3,c6) & b1 <> c4 )
proof end;
uniqueness
for b1, b2 being Point of (TOP-REAL c2) st b1 in (halfline c4,c5) /\ (Sphere c3,c6) & b1 <> c4 & b2 in (halfline c4,c5) /\ (Sphere c3,c6) & b2 <> c4 holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines HC BROUWER:def 3 :
for b1 being non empty Nat
for b2, b3, b4 being Point of (TOP-REAL b1)
for b5 being real non negative number st b3 is Point of (Tdisk b2,b5) & b4 is Point of (Tdisk b2,b5) & b3 <> b4 holds
for b6 being Point of (TOP-REAL b1) holds
( b6 = HC b3,b4,b2,b5 iff ( b6 in (halfline b3,b4) /\ (Sphere b2,b5) & b6 <> b3 ) );

theorem Th6: :: BROUWER:6
for b1 being real non negative number
for b2 being non empty Nat
for b3, b4, b5 being Point of (TOP-REAL b2) st b3 is Point of (Tdisk b4,b1) & b5 is Point of (Tdisk b4,b1) & b3 <> b5 holds
HC b3,b5,b4,b1 is Point of (Tcircle b4,b1)
proof end;

theorem Th7: :: BROUWER:7
for b1 being real number
for b2 being real non negative number
for b3 being non empty Nat
for b4, b5, b6 being Point of (TOP-REAL b3)
for b7, b8, b9 being Element of REAL b3 st b7 = b4 & b8 = b5 & b9 = b6 & b4 is Point of (Tdisk b6,b2) & b5 is Point of (Tdisk b6,b2) & b4 <> b5 & b1 = ((- |((b5 - b4),(b4 - b6))|) + (sqrt ((|((b5 - b4),(b4 - b6))| ^2 ) - ((Sum (sqr (b8 - b7))) * ((Sum (sqr (b7 - b9))) - (b2 ^2 )))))) / (Sum (sqr (b8 - b7))) holds
HC b4,b5,b6,b2 = ((1 - b1) * b4) + (b1 * b5)
proof end;

theorem Th8: :: BROUWER:8
for b1 being real number
for b2 being real non negative number
for b3, b4, b5, b6 being real number
for b7, b8, b9 being Point of (TOP-REAL 2) st b7 is Point of (Tdisk b9,b2) & b8 is Point of (Tdisk b9,b2) & b7 <> b8 & b3 = (b8 `1 ) - (b7 `1 ) & b4 = (b8 `2 ) - (b7 `2 ) & b5 = (b7 `1 ) - (b9 `1 ) & b6 = (b7 `2 ) - (b9 `2 ) & b1 = ((- ((b5 * b3) + (b6 * b4))) + (sqrt ((((b5 * b3) + (b6 * b4)) ^2 ) - (((b3 ^2 ) + (b4 ^2 )) * (((b5 ^2 ) + (b6 ^2 )) - (b2 ^2 )))))) / ((b3 ^2 ) + (b4 ^2 )) holds
HC b7,b8,b9,b2 = |[((b7 `1 ) + (b1 * b3)),((b7 `2 ) + (b1 * b4))]|
proof end;

definition
let c2 be non empty Nat;
let c3 be Point of (TOP-REAL c2);
let c4 be real non negative number ;
let c5 be Point of (Tdisk c3,c4);
let c6 be Function of (Tdisk c3,c4),(Tdisk c3,c4);
assume E9: not c5 is_a_fixpoint_of c6 ;
func HC c4,c5 -> Point of (Tcircle a2,a3) means :Def4: :: BROUWER:def 4
ex b1, b2 being Point of (TOP-REAL a1) st
( b1 = a4 & b2 = a5 . a4 & a6 = HC b2,b1,a2,a3 );
existence
ex b1 being Point of (Tcircle c3,c4)ex b2, b3 being Point of (TOP-REAL c2) st
( b2 = c5 & b3 = c6 . c5 & b1 = HC b3,b2,c3,c4 )
proof end;
uniqueness
for b1, b2 being Point of (Tcircle c3,c4) st ex b3, b4 being Point of (TOP-REAL c2) st
( b3 = c5 & b4 = c6 . c5 & b1 = HC b4,b3,c3,c4 ) & ex b3, b4 being Point of (TOP-REAL c2) st
( b3 = c5 & b4 = c6 . c5 & b2 = HC b4,b3,c3,c4 ) holds
b1 = b2 ;
end;

:: deftheorem Def4 defines HC BROUWER:def 4 :
for b1 being non empty Nat
for b2 being Point of (TOP-REAL b1)
for b3 being real non negative number
for b4 being Point of (Tdisk b2,b3)
for b5 being Function of (Tdisk b2,b3),(Tdisk b2,b3) st not b4 is_a_fixpoint_of b5 holds
for b6 being Point of (Tcircle b2,b3) holds
( b6 = HC b4,b5 iff ex b7, b8 being Point of (TOP-REAL b1) st
( b7 = b4 & b8 = b5 . b4 & b6 = HC b8,b7,b2,b3 ) );

theorem Th9: :: BROUWER:9
for b1 being real non negative number
for b2 being non empty Nat
for b3 being Point of (TOP-REAL b2)
for b4 being Point of (Tdisk b3,b1)
for b5 being Function of (Tdisk b3,b1),(Tdisk b3,b1) st not b4 is_a_fixpoint_of b5 & b4 is Point of (Tcircle b3,b1) holds
HC b4,b5 = b4
proof end;

theorem Th10: :: BROUWER:10
for b1 being real positive number
for b2 being Point of (TOP-REAL 2)
for b3 being non empty SubSpace of Tdisk b2,b1 st b3 = Tcircle b2,b1 holds
not b3 is_a_retract_of Tdisk b2,b1
proof end;

definition
let c2 be non empty Nat;
let c3 be real non negative number ;
let c4 be Point of (TOP-REAL c2);
let c5 be Function of (Tdisk c4,c3),(Tdisk c4,c3);
func BR-map c4 -> Function of (Tdisk a3,a2),(Tcircle a3,a2) means :Def5: :: BROUWER:def 5
for b1 being Point of (Tdisk a3,a2) holds a5 . b1 = HC b1,a4;
existence
ex b1 being Function of (Tdisk c4,c3),(Tcircle c4,c3) st
for b2 being Point of (Tdisk c4,c3) holds b1 . b2 = HC b2,c5
proof end;
uniqueness
for b1, b2 being Function of (Tdisk c4,c3),(Tcircle c4,c3) st ( for b3 being Point of (Tdisk c4,c3) holds b1 . b3 = HC b3,c5 ) & ( for b3 being Point of (Tdisk c4,c3) holds b2 . b3 = HC b3,c5 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines BR-map BROUWER:def 5 :
for b1 being non empty Nat
for b2 being real non negative number
for b3 being Point of (TOP-REAL b1)
for b4 being Function of (Tdisk b3,b2),(Tdisk b3,b2)
for b5 being Function of (Tdisk b3,b2),(Tcircle b3,b2) holds
( b5 = BR-map b4 iff for b6 being Point of (Tdisk b3,b2) holds b5 . b6 = HC b6,b4 );

theorem Th11: :: BROUWER:11
for b1 being real non negative number
for b2 being non empty Nat
for b3 being Point of (TOP-REAL b2)
for b4 being Point of (Tdisk b3,b1)
for b5 being Function of (Tdisk b3,b1),(Tdisk b3,b1) st not b4 is_a_fixpoint_of b5 & b4 is Point of (Tcircle b3,b1) holds
(BR-map b5) . b4 = b4
proof end;

theorem Th12: :: BROUWER:12
for b1 being real non negative number
for b2 being non empty Nat
for b3 being Point of (TOP-REAL b2)
for b4 being continuous Function of (Tdisk b3,b1),(Tdisk b3,b1) st b4 has_no_fixpoint holds
(BR-map b4) | (Sphere b3,b1) = id (Tcircle b3,b1)
proof end;

E14: now
let c2 be non empty TopSpace;
let c3 be Real;
set c4 = the carrier of c2;
set c5 = the carrier of c2 --> c3;
thus the carrier of c2 --> c3 is continuous
proof
E15: dom (the carrier of c2 --> c3) = the carrier of c2 by FUNCT_2:def 1;
E16: rng (the carrier of c2 --> c3) = {c3} by FUNCOP_1:14;
let c6 be Subset of REAL ; :: according to PSCOMP_1:def 25
assume c6 is closed ;
per cases ( c3 in c6 or not c3 in c6 ) ;
suppose c3 in c6 ;
then E17: rng (the carrier of c2 --> c3) c= c6 by E16, ZFMISC_1:37;
(the carrier of c2 --> c3) " c6 = (the carrier of c2 --> c3) " ((rng (the carrier of c2 --> c3)) /\ c6) by RELAT_1:168
.= (the carrier of c2 --> c3) " (rng (the carrier of c2 --> c3)) by E17, XBOOLE_1:28
.= the carrier of c2 by E15, RELAT_1:169
.= [#] c2 by PRE_TOPC:12 ;
hence (the carrier of c2 --> c3) " c6 is closed ;
end;
suppose not c3 in c6 ;
then E17: rng (the carrier of c2 --> c3) misses c6 by E16, ZFMISC_1:56;
(the carrier of c2 --> c3) " c6 = (the carrier of c2 --> c3) " ((rng (the carrier of c2 --> c3)) /\ c6) by RELAT_1:168
.= (the carrier of c2 --> c3) " {} by E17, XBOOLE_0:def 7
.= {} c2 by RELAT_1:171 ;
hence (the carrier of c2 --> c3) " c6 is closed ;
end;
end;
end;
end;

theorem Th13: :: BROUWER:13
for b1 being real positive number
for b2 being Point of (TOP-REAL 2)
for b3 being continuous Function of (Tdisk b2,b1),(Tdisk b2,b1) st b3 has_no_fixpoint holds
BR-map b3 is continuous
proof end;

theorem Th14: :: BROUWER:14
for b1 being real non negative number
for b2 being Point of (TOP-REAL 2)
for b3 being continuous Function of (Tdisk b2,b1),(Tdisk b2,b1) holds b3 has_a_fixpoint
proof end;

theorem Th15: :: BROUWER:15
for b1 being real non negative number
for b2 being Point of (TOP-REAL 2)
for b3 being continuous Function of (Tdisk b2,b1),(Tdisk b2,b1) ex b4 being Point of (Tdisk b2,b1) st b3 . b4 = b4
proof end;