:: Brouwer Fixed Point Theorem in the General Case
:: by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

Lm1:  for n being Nat
for p, q being Point of (TOP-REAL n)
for r being real number holds (((1 - r) * p) + (r * q)) - p = r * (q - p)
proofend;

Lm2:  for n being Nat
for p being Point of (TOP-REAL n)
for r being real number st r >= 0 holds
r * p in halfline ((0. (TOP-REAL n)),p)
proofend;

theorem Th1: :: BROUWER2:1
for n being Nat
for p, q being Point of (TOP-REAL n)
for r being real number holds ((1 - r) * p) + (r * q) = p + (r * (q - p))
proofend;

theorem Th2: :: BROUWER2:2
for n being Nat
for u, p, q, w being Point of (TOP-REAL n) st u in halfline (p,q) & w in halfline (p,q) & |.(u - p).| = |.(w - p).| holds
u = w
proofend;

Lm3:  for n being Nat
for p, q being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n) st p in A &amp; p <> q &amp; A /\ (halfline (p,q)) is bounded holds
ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) &amp; ( for u, P being Point of (Euclid n) st P = p &amp; u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) &amp; ( for r being real number st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) &amp; dist (w,u) < r ) ) )
proofend;

theorem :: BROUWER2:3
for n being Nat
for p, q being Point of (TOP-REAL n)
for S being Subset of (TOP-REAL n) st p in S &amp; p <> q &amp; S /\ (halfline (p,q)) is bounded holds
ex w being Point of (TOP-REAL n) st
( w in (Fr S) /\ (halfline (p,q)) &amp; ( for u being Point of (TOP-REAL n) st u in S /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) &amp; ( for r being real number st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in S /\ (halfline (p,q)) &amp; |.(w - u).| < r ) ) )
proofend;

theorem Th4: :: BROUWER2:4
for n being Nat
for p, q being Point of (TOP-REAL n)
for A being convex Subset of (TOP-REAL n) st A is closed &amp; p in Int A &amp; p <> q &amp; A /\ (halfline (p,q)) is bounded holds
ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
proofend;

Lm4:  for n being Element of NAT st n > 0 holds
for A being convex Subset of (TOP-REAL n) st A is compact &amp; 0* n in Int A holds
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism &amp; h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
proofend;

theorem Th5: :: BROUWER2:5
for n being Nat
for p being Point of (TOP-REAL n)
for r being real number st r > 0 holds
Fr (cl_Ball (p,r)) = Sphere (p,r)
proofend;

registration
let n be Element of NAT ;
let A be bounded Subset of (TOP-REAL n);
let p be Point of (TOP-REAL n);
clusterp + A ->  bounded ;
coherence
 p + A is bounded
proofend;
end;

begin

theorem Th6: :: BROUWER2:6
for n being Element of NAT
for A being convex Subset of (TOP-REAL n) st A is compact &amp; not A is boundary holds
ex h being Function of ((TOP-REAL n) | A),(Tdisk ((0. (TOP-REAL n)),1)) st
( h is being_homeomorphism &amp; h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
proofend;

theorem Th7: :: BROUWER2:7
for n being Nat
for A, B being convex Subset of (TOP-REAL n) st A is compact &amp; not A is boundary &amp; B is compact &amp; not B is boundary holds
ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | B) st
( h is being_homeomorphism &amp; h .: (Fr A) = Fr B )
proofend;

theorem Th8: :: BROUWER2:8
for n being Nat
for A being convex Subset of (TOP-REAL n) st A is compact &amp; not A is boundary holds
for h being continuous Function of ((TOP-REAL n) | A),((TOP-REAL n) | A) holds h is with_fixpoint
proofend;

Lm5:  for n being Nat holds not cl_Ball ((0. (TOP-REAL n)),1) is boundary
proofend;

Lm6:  for n being Element of NAT
for X being non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1) st X = Tcircle ((0. (TOP-REAL n)),1) holds
not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1)
proofend;

theorem :: BROUWER2:9
for n being Nat
for A being non empty convex Subset of (TOP-REAL n) st A is compact &amp; not A is boundary holds
for FR being non empty SubSpace of (TOP-REAL n) | A st [#] FR = Fr A holds
not FR is_a_retract_of (TOP-REAL n) | A
proofend;