:: Brouwer Fixed Point Theorem for Simplexes :: by Karol P\kak :: :: Received December 21, 2010 :: Copyright (c) 2010-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ABIAN, AOFA_I00, ARYTM_1, ARYTM_3, CARD_1, CARD_3, CLASSES1, COMPLEX1, CONVEX1, EUCLID, EUCLID_9, FINSEQ_1, FINSEQ_2, FINSEQ_4, FINSET_1, FUNCOP_1, FUNCT_1, FUNCT_2, FUNCT_4, GLIB_000, INT_1, MATROID0, MEASURE5, MEMBERED, METRIC_1, NAT_1, NEWTON, NUMBERS, ORDERS_1, ORDINAL1, ORDINAL2, ORDINAL4, PARTFUN1, PCOMPS_1, PEPIN, POWER, PRE_TOPC, QC_LANG1, RCOMP_1, REAL_1, RELAT_1, RLAFFIN1, RLAFFIN2, RLVECT_1, RLVECT_2, RLVECT_5, RUSUB_4, SEMI_AF1, SEQ_4, SETFAM_1, SGRAPH1, SIMPLEX0, SIMPLEX1, SQUARE_1, STRUCT_0, SUBSET_1, SUPINF_2, TARSKI, TOPDIM_1, TOPMETR, TOPS_1, TOPS_2, VALUED_1, WEIERSTR, XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_1, XXREAL_2, ZFMISC_1, SIMPLEX2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, ZFMISC_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, PARTFUN1, FUNCOP_1, FUNCT_4, XXREAL_3, VALUED_1, PRE_TOPC, NUMBERS, XCMPLX_0, XREAL_0, FINSEQ_1, BINOP_1, FINSEQ_2, TOPMETR, METRIC_1, EUCLID, FINSET_1, XXREAL_0, REAL_1, SETFAM_1, TOPS_2, INT_1, STRUCT_0, COMPTS_1, PCOMPS_1, RCOMP_1, WEIERSTR, SEQ_4, XXREAL_2, RVSUM_1, RLVECT_1, RUSUB_4, RLVECT_5, SIMPLEX0, RLAFFIN1, RLAFFIN2, SIMPLEX1, ORDERS_1, CARD_1, DOMAIN_1, PENCIL_1, CLASSES1, RLTOPSP1, MATROID0, TBSP_1, MEMBERED, RLVECT_2, CONVEX1, TOPREAL9, COMPLEX1, NEWTON, POWER, SQUARE_1, BORSUK_1, CARD_3, EUCLID_9, TMAP_1, FINSEQOP, ABIAN, TOPDIM_1, TOPDIM_2, RLAFFIN3; constructors ABIAN, BINOP_2, COMPTS_1, CONVEX1, EUCLID_9, FINSEQOP, FUNCSDOM, MONOID_0, NEWTON, POWER, REAL_1, RFINSEQ2, RLAFFIN1, RLAFFIN2, RLAFFIN3, RLVECT_5, RUSUB_5, SEQ_4, SIMPLEX1, SQUARE_1, TBSP_1, TMAP_1, TOPDIM_1, TOPDIM_2, TOPREAL9, TOPS_2, WAYBEL23, WEIERSTR, RCOMP_1; registrations BORSUK_1, BORSUK_2, CARD_1, COMPTS_1, EUCLID, EUCLID_9, FINSEQ_1, FINSET_1, FUNCT_2, INT_1, JORDAN2B, JORDAN2C, MEMBERED, METRIZTS, MONOID_0, NAT_1, NEWTON, NUMBERS, PCOMPS_1, PRE_TOPC, RELAT_1, RELSET_1, RLAFFIN1, RLAFFIN3, SEQ_4, SIMPLEX0, SIMPLEX1, STRUCT_0, SUBSET_1, TBSP_1, TMAP_1, TOPDIM_1, TOPDIM_2, TOPMETR, TOPREAL9, TOPREALC, TOPS_1, VALUED_0, VALUED_1, XBOOLE_0, XREAL_0, XXREAL_0, XXREAL_2, XXREAL_3, YELLOW13, JORDAN, ORDINAL1, FINSEQ_2; requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE; begin :: The Lebesgue Number reserve M for non empty MetrSpace, F,G for open Subset-Family of TopSpaceMetr M; definition let M such that TopSpaceMetr M is compact; let F be Subset-Family of TopSpaceMetr M such that F is open and F is Cover of TopSpaceMetr M; mode Lebesgue_number of F -> positive Real means :: SIMPLEX2:def 1 for p be Point of M ex A be Subset of TopSpaceMetr M st A in F & Ball(p,it) c= A; end; reserve L for Lebesgue_number of F; theorem :: SIMPLEX2:1 TopSpaceMetr M is compact & F is Cover of TopSpaceMetr M & F c= G implies L is Lebesgue_number of G; theorem :: SIMPLEX2:2 TopSpaceMetr M is compact & F is Cover of TopSpaceMetr M & F is_finer_than G implies L is Lebesgue_number of G; theorem :: SIMPLEX2:3 for L1 be positive Real st TopSpaceMetr M is compact & F is Cover of TopSpaceMetr M & L1 <= L holds L1 is Lebesgue_number of F; begin :: Bounded Simplicial Complexes reserve n,k for Nat, r for Real, X for set, M for Reflexive non empty MetrStruct, A for Subset of M, K for SimplicialComplexStr; registration let M; cluster finite -> bounded for Subset of M; end; theorem :: SIMPLEX2:4 for S be finite non empty Subset of M ex p,q be Point of M st p in S & q in S & dist(p,q) = diameter S; definition let M,K; attr K is M bounded means :: SIMPLEX2:def 2 ex r st for A st A in the topology of K holds A is bounded & diameter A <= r; end; theorem :: SIMPLEX2:5 for K be non void SimplicialComplexStr st K is M bounded & A is Simplex of K holds A is bounded; registration let M,X; cluster M bounded non void for SimplicialComplex of X; end; registration let M; cluster M bounded non void subset-closed finite-membered for SimplicialComplexStr; end; registration let M,X; let K be M bounded SimplicialComplexStr of X; cluster -> M bounded for (SubSimplicialComplex of K); end; registration let M,X; let K be M bounded subset-closed SimplicialComplexStr of X; let i be dim-like number; cluster Skeleton_of(K,i) -> M bounded; end; theorem :: SIMPLEX2:6 K is finite-vertices implies K is M bounded; begin definition let M; let K be SimplicialComplexStr such that K is M bounded; func diameter(M,K) -> Real means :: SIMPLEX2:def 3 (for A st A in the topology of K holds diameter A <= it) & for r st (for A st A in the topology of K holds diameter A <= r) holds r >= it if the topology of K meets bool [#]M otherwise it = 0; end; theorem :: SIMPLEX2:7 K is M bounded implies 0 <= diameter(M,K); theorem :: SIMPLEX2:8 for K be M bounded SimplicialComplexStr of X, KX be SubSimplicialComplex of K holds diameter(M,KX) <= diameter(M,K); theorem :: SIMPLEX2:9 for K be M bounded subset-closed SimplicialComplexStr of X, i be dim-like number holds diameter(M,Skeleton_of(K,i)) <= diameter(M,K); definition let M; let K be M bounded non void subset-closed SimplicialComplexStr; redefine func diameter(M,K) means :: SIMPLEX2:def 4 (for A st A is Simplex of K holds diameter A <= it) & for r st (for A st A is Simplex of K holds diameter A <= r) holds r >= it; end; theorem :: SIMPLEX2:10 for S be finite Subset of M holds diameter(M,Complex_of{S}) = diameter S; definition let n; let K be SimplicialComplexStr of TOP-REAL n; attr K is bounded means :: SIMPLEX2:def 5 K is (Euclid n) bounded; func diameter K -> Real equals :: SIMPLEX2:def 6 diameter(Euclid n,K); end; registration let n; cluster bounded -> Euclid n bounded for (SimplicialComplexStr of TOP-REAL n); cluster bounded affinely-independent simplex-join-closed non void finite-degree total for SimplicialComplex of TOP-REAL n; cluster finite-vertices -> bounded for SimplicialComplexStr of TOP-REAL n; end; begin :: The Estimation of Diameter of the Barycentric Subdivision reserve V for RealLinearSpace, Kv for non void SimplicialComplex of V; theorem :: SIMPLEX2:11 for S be Simplex of BCS Kv for F be c=-linear finite finite-membered Subset-Family of V st S = (center_of_mass V).:F for a1,a2 be VECTOR of V st a1 in S & a2 in S ex b1,b2 be VECTOR of V,r be Real st b1 in Vertices BCS Complex_of{union F} & b2 in Vertices BCS Complex_of{union F} & a1-a2 = r*(b1-b2) & 0 <= r & r <= (card union F-1)/card union F; theorem :: SIMPLEX2:12 for A be affinely-independent Subset of TOP-REAL n for E be Enumeration of A st dom E\X is non empty holds conv(E.:X) = meet{conv(A\{E.k}) where k is Element of NAT: k in dom E\X}; reserve A for Subset of TOP-REAL n; theorem :: SIMPLEX2:13 for a be bounded Subset of Euclid n st a=A for p be Point of Euclid n st p in conv A holds conv A c= cl_Ball(p,diameter a); theorem :: SIMPLEX2:14 A is bounded iff conv A is bounded; theorem :: SIMPLEX2:15 for a,ca be bounded Subset of Euclid n st ca = conv A & a = A holds diameter a = diameter ca; registration let n; let K be bounded SimplicialComplexStr of TOP-REAL n; cluster -> bounded for SubdivisionStr of K; end; theorem :: SIMPLEX2:16 for K be bounded finite-degree non void SimplicialComplex of TOP-REAL n st |.K.| c= [#]K holds diameter BCS K <= degree K/(degree K+1) * diameter K; theorem :: SIMPLEX2:17 for K be bounded finite-degree non void SimplicialComplex of TOP-REAL n st |.K.| c= [#]K holds diameter BCS(k,K) <= (degree K/(degree K+1))|^k * diameter K; theorem :: SIMPLEX2:18 for K be bounded finite-degree non void SimplicialComplex of TOP-REAL n st |.K.| c= [#]K for r st r>0 ex k st diameter BCS(k,K) < r; theorem :: SIMPLEX2:19 for i,j be Element of NAT ex f be Function of[:TOP-REAL i,TOP-REAL j:],TOP-REAL(i+j) st f is being_homeomorphism & for fi be Element of TOP-REAL i,fj be Element of TOP-REAL j holds f.(fi,fj) = fi^fj; theorem :: SIMPLEX2:20 for i,j be Element of NAT for f be Function of [:TOP-REAL i,TOP-REAL j:],TOP-REAL(i+j) st for fi be Element of TOP-REAL i,fj be Element of TOP-REAL j holds f.(fi,fj) = fi^fj for r for fi be Point of Euclid i,fj be Point of Euclid j, fij be Point of Euclid(i+j) st fij = fi^fj holds f.:[:OpenHypercube(fi,r),OpenHypercube(fj,r):] = OpenHypercube(fij,r) ; theorem :: SIMPLEX2:21 A is bounded iff ex p be Point of Euclid n,r st A c= OpenHypercube(p,r); registration let n; cluster closed bounded -> compact for Subset of TOP-REAL n; end; registration let n; let A be affinely-independent Subset of TOP-REAL n; cluster conv A -> compact; end; begin :: Main Theorems theorem :: SIMPLEX2:22 for A be non empty affinely-independent Subset of TOP-REAL n for E be Enumeration of A for F be FinSequence of bool the carrier of ((TOP-REAL n)|(conv A)) st len F = card A & rng F is closed & for S be Subset of dom F holds conv(E.:S) c= union(F.:S) holds meet rng F is non empty; reserve A for affinely-independent Subset of TOP-REAL n; theorem :: SIMPLEX2:23 for A st card A = n+1 for f be continuous Function of(TOP-REAL n)|conv A,(TOP-REAL n)|conv A ex p be Point of TOP-REAL n st p in dom f & f.p=p; theorem :: SIMPLEX2:24 for A st card A = n+1 for f be continuous Function of (TOP-REAL n)|conv A,(TOP-REAL n)|conv A holds f is with_fixpoint; theorem :: SIMPLEX2:25 card A = n+1 implies ind conv A = n; theorem :: SIMPLEX2:26 ind TOP-REAL n = n;