BROUWER2: Brouwer Fixed Point Theorem in the General Case

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

environ

vocabularies HIDDEN, ABIAN, ARYTM_1, ARYTM_3, BORSUK_1, BROUWER, CARD_1, COMPLEX1, CONNSP_2, CONVEX1, EUCLID, FUNCOP_1, FUNCT_1, FUNCT_3, FUNCT_4, JGRAPH_4, MEASURE5, MEMBERED, METRIC_1, NAT_1, NUMBERS, ORDINAL2, PCOMPS_1, PRE_TOPC, PROB_1, RCOMP_1, REAL_1, RELAT_1, RLAFFIN1, RLTOPSP1, RLVECT_1, RLVECT_5, RUSUB_4, RVSUM_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPMETR, TOPREALB, TOPS_1, TOPS_2, VALUED_1, VALUED_2, XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_2, FUNCT_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, NUMBERS, VALUED_1, CARD_1, XCMPLX_0, XREAL_0, XXREAL_0, MEMBERED, COMPLEX1, FUNCOP_1, FINSEQ_2, VALUED_2, STRUCT_0, PRE_TOPC, RLAFFIN2, TOPS_1, METRIC_1, PCOMPS_1, TOPMETR, BORSUK_1, RLVECT_1, RLTOPSP1, EUCLID, TOPREAL9, TOPREALB, DOMAIN_1, TOPS_2, COMPTS_1, TBSP_1, XXREAL_2, FUNCT_4, JGRAPH_4, TMAP_1, RUSUB_4, CONVEX1, REAL_1, CONNSP_2, BROUWER, ABIAN, RLVECT_5, RLAFFIN1;
definitions TARSKI, BORSUK_1;
theorems ABIAN, ABSVALUE, BOOLMARK, BORSUK_1, BROUWER, COMPLEX1, COMPTS_1, CONNSP_2, CONVEX1, EUCLID, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, GOBOARD6, HAUSDORF, JGRAPH_4, JORDAN24, JORDAN2C, MEMBERED, METRIC_1, NECKLACE, ORDINAL1, PRE_TOPC, RELAT_1, RLAFFIN1, RLAFFIN2, RLAFFIN3, RLTOPSP1, RLVECT_1, RUSUB_4, SIMPLEX2, SPPOL_1, SUBSET_1, TARSKI, TBSP_1, TMAP_1, TOPGEN_1, TOPMETR, TOPMETR2, TOPREAL9, TOPREALB, TOPREALC, TOPRNS_1, TOPS_1, TOPS_2, TOPS_4, VALUED_2, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_0, XREAL_1, XXREAL_0, XXREAL_2, ZFMISC_1, RLVECT_4;
schemes ;
registrations BORSUK_1, BORSUK_3, BROUWER, CARD_1, COMPTS_1, CONVEX1, EUCLID, FUNCOP_1, FUNCT_1, FUNCT_2, JGRAPH_4, JORDAN, JORDAN2C, MEMBERED, NAT_1, PCOMPS_1, PRE_TOPC, RELAT_1, REVROT_1, RLAFFIN1, RLAFFIN3, RLTOPSP1, RLVECT_1, SIMPLEX2, STRUCT_0, SUBSET_1, TMAP_1, TOPGRP_1, TOPMETR, TOPREAL1, TOPREAL9, TOPREALC, TOPS_1, VALUED_0, VALUED_2, WAYBEL_2, XBOOLE_0, XCMPLX_0, XREAL_0, XXREAL_0, RELSET_1, FINSET_1, ORDINAL1;
constructors HIDDEN, BINOP_2, COMPLEX1, TBSP_1, MONOID_0, CONVEX1, GRCAT_1, TOPREAL9, TOPS_1, COMPTS_1, PCOMPS_1, FUNCSDOM, JGRAPH_4, TMAP_1, TOPREALC, BROUWER, ABIAN, RUSUB_4, RLAFFIN1, RLAFFIN2, RLVECT_5, SEQ_4, FUNCT_4, REAL_1, XXREAL_3, SIMPLEX2, SIMPLEX1;
requirements HIDDEN, ARITHM, BOOLE, NUMERALS, SUBSET, REAL;
equalities XCMPLX_0, STRUCT_0, ALGSTR_0, TOPREAL9, BROUWER, ORDINAL1;
expansions TARSKI, BORSUK_1;

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

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;