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


Lm1: for n being Nat
for p, q being Point of (TOP-REAL n)
for r being Real holds (((1 - r) * p) + (r * q)) - p = r * (q - p)
proof end;

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

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

theorem Th2: :: BROUWER2:2
for n being Nat
for p, q, u, 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
proof end;

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 & p <> q & A /\ (halfline (p,q)) is bounded holds
ex w being Point of (Euclid n) st
( w in (Fr A) /\ (halfline (p,q)) & ( for u, P being Point of (Euclid n) st P = p & u in A /\ (halfline (p,q)) holds
dist (P,u) <= dist (P,w) ) & ( for r being Real st r > 0 holds
ex u being Point of (Euclid n) st
( u in A /\ (halfline (p,q)) & dist (w,u) < r ) ) )
proof end;

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 & p <> q & S /\ (halfline (p,q)) is bounded holds
ex w being Point of (TOP-REAL n) st
( w in (Fr S) /\ (halfline (p,q)) & ( for u being Point of (TOP-REAL n) st u in S /\ (halfline (p,q)) holds
|.(p - u).| <= |.(p - w).| ) & ( for r being Real st r > 0 holds
ex u being Point of (TOP-REAL n) st
( u in S /\ (halfline (p,q)) & |.(w - u).| < r ) ) )
proof end;

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 & p in Int A & p <> q & A /\ (halfline (p,q)) is bounded holds
ex u being Point of (TOP-REAL n) st (Fr A) /\ (halfline (p,q)) = {u}
proof end;

Lm4: for n being Element of NAT st n > 0 holds
for A being convex Subset of (TOP-REAL n) st A is compact & 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 & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
proof end;

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

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

theorem Th6: :: BROUWER2:6
for n being Element of NAT
for A being convex Subset of (TOP-REAL n) st A is compact & 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 & h .: (Fr A) = Sphere ((0. (TOP-REAL n)),1) )
proof end;

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

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

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

reconsider jj = 1 as Real ;

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)
proof end;

theorem :: BROUWER2:9
for n being Nat
for A being non empty convex Subset of (TOP-REAL n) st A is compact & 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
proof end;