:: by Karol P\kak

::

:: Received December 21, 2010

:: Copyright (c) 2010-2016 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))

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

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 ) ) )

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}

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)

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

coherence

p + A is bounded

end;
let A be bounded Subset of (TOP-REAL n);

let p be Point of (TOP-REAL n);

coherence

p + A is bounded

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

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 )

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

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

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;