:: Brouwer Fixed Point Theorem for Disks on the Plane
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received February 22, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

set T2 = TOP-REAL 2;

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:]
proofend;
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
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] &amp; s <> t ) ) ;

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

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

theorem Th2: :: BROUWER:2
for n being Element of NAT
for x being Point of (TOP-REAL n) holds cl_Ball (x,0) = {x}
proofend;

definition
let n be Element of 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 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));

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

theorem Th3: :: BROUWER:3
for n being Element of 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)
proofend;

registration
let n be Element of 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
proofend;
end;

theorem Th4: :: BROUWER:4
for n being Element of NAT
for r being non negative real number
for s, t, x being Point of (TOP-REAL n) st s <> t &amp; s is Point of (Tdisk (x,r)) &amp; 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))
proofend;

theorem Th5: :: BROUWER:5
for n being Element of NAT
for r being non negative real number
for s, t, x being Point of (TOP-REAL n) st s <> t &amp; s in the carrier of (Tcircle (x,r)) &amp; t is Point of (Tdisk (x,r)) holds
ex e being Point of (Tcircle (x,r)) st
( e <> s &amp; {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) )
proofend;

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: :: BROUWER:def 3
( it in (halfline (s,t)) /\ (Sphere (o,r)) &amp; it <> s );
existence
 ex b1 being Point of (TOP-REAL n) st
( b1 in (halfline (s,t)) /\ (Sphere (o,r)) &amp; b1 <> s )
proofend;
uniqueness
 for b1, b2 being Point of (TOP-REAL n) st b1 in (halfline (s,t)) /\ (Sphere (o,r)) &amp; b1 <> s &amp; b2 in (halfline (s,t)) /\ (Sphere (o,r)) &amp; b2 <> s holds
b1 = b2
proofend;
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)) &amp; t is Point of (Tdisk (o,r)) &amp; 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)) &amp; b6 <> s ) );

theorem Th6: :: BROUWER:6
for r being non negative real number
for n being non empty Element of NAT
for s, o, t being Point of (TOP-REAL n) st s is Point of (Tdisk (o,r)) &amp; t is Point of (Tdisk (o,r)) &amp; s <> t holds
HC (s,t,o,r) is Point of (Tcircle (o,r))
proofend;

theorem :: BROUWER:7
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 &amp; T = t &amp; O = o &amp; s is Point of (Tdisk (o,r)) &amp; t is Point of (Tdisk (o,r)) &amp; s <> t &amp; 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)
proofend;

theorem Th8: :: BROUWER:8
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)) &amp; t is Point of (Tdisk (o,r)) &amp; s <> t &amp; r1 = (t `1) - (s `1) &amp; r2 = (t `2) - (s `2) &amp; s1 = (s `1) - (o `1) &amp; s2 = (s `2) - (o `2) &amp; 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))]|
proofend;

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: :: BROUWER:def 4
 ex y, z being Point of (TOP-REAL n) st
( y = x &amp; z = f . x &amp; 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 &amp; z = f . x &amp; b1 = HC (z,y,o,r) )
proofend;
uniqueness
 for b1, b2 being Point of (Tcircle (o,r)) st ex y, z being Point of (TOP-REAL n) st
( y = x &amp; z = f . x &amp; b1 = HC (z,y,o,r) ) &amp; ex y, z being Point of (TOP-REAL n) st
( y = x &amp; z = f . x &amp; 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 &amp; z = f . x &amp; b6 = HC (z,y,o,r) ) );

theorem Th9: :: BROUWER:9
for r being non negative real number
for n being non empty Element of 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 &amp; x is Point of (Tcircle (o,r)) holds
HC (x,f) = x
proofend;

theorem Th10: :: BROUWER:10
for r being positive real 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)
proofend;

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: :: 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)
proofend;
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) ) &amp; ( for x being Point of (Tdisk (o,r)) holds b2 . x = HC (x,f) ) holds
b1 = b2
proofend;
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: :: BROUWER:11
for r being non negative real number
for n being non empty Element of 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 &amp; x is Point of (Tcircle (o,r)) holds
(BR-map f) . x = x
proofend;

theorem :: BROUWER:12
for r being non negative real number
for n being non empty Element of NAT
for o being Point of (TOP-REAL n)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
proofend;

Lm1: now__::_thesis:_for_T_being_non_empty_TopSpace
for_a_being_Real_holds_the_carrier_of_T_-->_a_is_continuous
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
let Y be Subset of REAL; :: according toPSCOMP_1:def_3 ::_thesis: ( not Y is closed or ( the carrier of T --> a) " Y is closed )
A1: dom ( the carrier of T --> a) = the carrier of T by FUNCT_2:def_1;
assume  Y is closed ; ::_thesis: ( the carrier of T --> a) " Y is closed
A2: rng ( the carrier of T --> a) = {a} by FUNCOP_1:8;
percases ( 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:31;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " (rng ( the carrier of T --> a)) by A3, XBOOLE_1:28
.= [#] T by A1, RELAT_1:134 ;
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:50;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " {} by A4, XBOOLE_0:def_7
.= {} T ;
hence  ( the carrier of T --> a) " Y is closed ; ::_thesis: verum
end;
end;
end;
end;

theorem Th13: :: BROUWER:13
for r being positive real number
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
BR-map f is continuous
proofend;

:: [WP: ] Brouwer_Fixed_Point_Theorem
theorem Th14: :: BROUWER:14
for r being non negative real number
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f is with_fixpoint
proofend;

:: [WP: ] Brouwer_Fixed_Point_Theorem_for_Disks_on_the_Plane
theorem :: BROUWER:15
for r being non negative real 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
proofend;