:: Brouwer Fixed Point Theorem for Simplexes :: by Karol P\kak :: :: Received December 21, 2010 :: Copyright (c) 2010-2012 Association of Mizar Users begin definition let M be non empty MetrSpace; assume B1: TopSpaceMetr M is compact ; let F be Subset-Family of (TopSpaceMetr M); assume that B2: F is open and B3: F is Cover of (TopSpaceMetr M) ; mode Lebesgue_number of F -> positive Real means :Def1: :: SIMPLEX2:def 1 for p being Point of M ex A being Subset of (TopSpaceMetr M) st ( A in F & Ball (p,it) c= A ); existence ex b1 being positive Real st for p being Point of M ex A being Subset of (TopSpaceMetr M) st ( A in F & Ball (p,b1) c= A ) proofend; end; :: deftheorem Def1 defines Lebesgue_number SIMPLEX2:def_1_:_ for M being non empty MetrSpace st TopSpaceMetr M is compact holds for F being Subset-Family of (TopSpaceMetr M) st F is open & F is Cover of (TopSpaceMetr M) holds for b3 being positive Real holds ( b3 is Lebesgue_number of F iff for p being Point of M ex A being Subset of (TopSpaceMetr M) st ( A in F & Ball (p,b3) c= A ) ); theorem :: SIMPLEX2:1 for M being non empty MetrSpace for F, G being open Subset-Family of (TopSpaceMetr M) for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F c= G holds L is Lebesgue_number of G proofend; theorem :: SIMPLEX2:2 for M being non empty MetrSpace for F, G being open Subset-Family of (TopSpaceMetr M) for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & F is_finer_than G holds L is Lebesgue_number of G proofend; theorem :: SIMPLEX2:3 for M being non empty MetrSpace for F being open Subset-Family of (TopSpaceMetr M) for L being Lebesgue_number of F for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of (TopSpaceMetr M) & L1 <= L holds L1 is Lebesgue_number of F proofend; begin registration let M be non empty Reflexive MetrStruct ; cluster finite -> bounded for Element of bool the carrier of M; coherence for b1 being Subset of M st b1 is finite holds b1 is bounded proofend; end; theorem :: SIMPLEX2:4 for M being non empty Reflexive MetrStruct for S being non empty finite Subset of M ex p, q being Point of M st ( p in S & q in S & dist (p,q) = diameter S ) proofend; definition let M be non empty Reflexive MetrStruct ; let K be SimplicialComplexStr; attrK is M bounded means :Def2: :: SIMPLEX2:def 2 ex r being real number st for A being Subset of M st A in the topology of K holds ( A is bounded & diameter A <= r ); end; :: deftheorem Def2 defines bounded SIMPLEX2:def_2_:_ for M being non empty Reflexive MetrStruct for K being SimplicialComplexStr holds ( K is M bounded iff ex r being real number st for A being Subset of M st A in the topology of K holds ( A is bounded & diameter A <= r ) ); theorem Th5: :: SIMPLEX2:5 for M being non empty Reflexive MetrStruct for A being Subset of M for K being non void SimplicialComplexStr st K is M bounded & A is Simplex of K holds A is bounded proofend; registration let M be non empty Reflexive MetrStruct ; let X be set ; cluster non void subset-closed finite-membered M bounded for SimplicialComplexStr of X; existence ex b1 being SimplicialComplex of X st ( b1 is M bounded & not b1 is void ) proofend; end; registration let M be non empty Reflexive MetrStruct ; cluster non void subset-closed finite-membered M bounded for TopStruct ; existence ex b1 being SimplicialComplexStr st ( b1 is M bounded & not b1 is void & b1 is subset-closed & b1 is finite-membered ) proofend; end; registration let M be non empty Reflexive MetrStruct ; let X be set ; let K be M bounded SimplicialComplexStr of X; cluster -> M bounded for SubSimplicialComplex of K; coherence for b1 being SubSimplicialComplex of K holds b1 is M bounded proofend; end; registration let M be non empty Reflexive MetrStruct ; let X be set ; let K be subset-closed M bounded SimplicialComplexStr of X; let i be Integer; cluster Skeleton_of (K,i) -> M bounded ; coherence Skeleton_of (K,i) is M bounded ; end; theorem Th6: :: SIMPLEX2:6 for M being non empty Reflexive MetrStruct for K being SimplicialComplexStr st K is finite-vertices holds K is M bounded proofend; begin Lm1: 0 in REAL by XREAL_0:def_1; definition let M be non empty Reflexive MetrStruct ; let K be SimplicialComplexStr; assume B1: K is M bounded ; func diameter (M,K) -> Real means :Def3: :: SIMPLEX2:def 3 ( ( for A being Subset of M st A in the topology of K holds diameter A <= it ) & ( for r being real number st ( for A being Subset of M 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 ; existence ( ( the topology of K meets bool ([#] M) implies ex b1 being Real st ( ( for A being Subset of M st A in the topology of K holds diameter A <= b1 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds diameter A <= r ) holds r >= b1 ) ) ) & ( not the topology of K meets bool ([#] M) implies ex b1 being Real st b1 = 0 ) ) proofend; uniqueness for b1, b2 being Real holds ( ( the topology of K meets bool ([#] M) & ( for A being Subset of M st A in the topology of K holds diameter A <= b1 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds diameter A <= r ) holds r >= b1 ) & ( for A being Subset of M st A in the topology of K holds diameter A <= b2 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds diameter A <= r ) holds r >= b2 ) implies b1 = b2 ) & ( not the topology of K meets bool ([#] M) & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proofend; consistency for b1 being Real holds verum ; end; :: deftheorem Def3 defines diameter SIMPLEX2:def_3_:_ for M being non empty Reflexive MetrStruct for K being SimplicialComplexStr st K is M bounded holds for b3 being Real holds ( ( the topology of K meets bool ([#] M) implies ( b3 = diameter (M,K) iff ( ( for A being Subset of M st A in the topology of K holds diameter A <= b3 ) & ( for r being real number st ( for A being Subset of M st A in the topology of K holds diameter A <= r ) holds r >= b3 ) ) ) ) & ( not the topology of K meets bool ([#] M) implies ( b3 = diameter (M,K) iff b3 = 0 ) ) ); theorem Th7: :: SIMPLEX2:7 for M being non empty Reflexive MetrStruct for K being SimplicialComplexStr st K is M bounded holds 0 <= diameter (M,K) proofend; theorem :: SIMPLEX2:8 for X being set for M being non empty Reflexive MetrStruct for K being b2 bounded SimplicialComplexStr of X for KX being SubSimplicialComplex of K holds diameter (M,KX) <= diameter (M,K) proofend; theorem :: SIMPLEX2:9 for X being set for M being non empty Reflexive MetrStruct for K being subset-closed b2 bounded SimplicialComplexStr of X for i being Integer holds diameter (M,(Skeleton_of (K,i))) <= diameter (M,K) proofend; definition let M be non empty Reflexive MetrStruct ; let K be non void subset-closed M bounded SimplicialComplexStr; :: original:diameter redefine func diameter (M,K) -> Real means :Def4: :: SIMPLEX2:def 4 ( ( for A being Subset of M st A is Simplex of K holds diameter A <= it ) & ( for r being real number st ( for A being Subset of M st A is Simplex of K holds diameter A <= r ) holds r >= it ) ); coherence diameter (M,K) is Real ; compatibility for b1 being Real holds ( b1 = diameter (M,K) iff ( ( for A being Subset of M st A is Simplex of K holds diameter A <= b1 ) & ( for r being real number st ( for A being Subset of M st A is Simplex of K holds diameter A <= r ) holds r >= b1 ) ) ) proofend; end; :: deftheorem Def4 defines diameter SIMPLEX2:def_4_:_ for M being non empty Reflexive MetrStruct for K being non void subset-closed b1 bounded SimplicialComplexStr for b3 being Real holds ( b3 = diameter (M,K) iff ( ( for A being Subset of M st A is Simplex of K holds diameter A <= b3 ) & ( for r being real number st ( for A being Subset of M st A is Simplex of K holds diameter A <= r ) holds r >= b3 ) ) ); theorem :: SIMPLEX2:10 for M being non empty Reflexive MetrStruct for S being finite Subset of M holds diameter (M,(Complex_of {S})) = diameter S proofend; definition let n be Nat; let K be SimplicialComplexStr of (TOP-REAL n); attrK is bounded means :Def5: :: SIMPLEX2:def 5 K is Euclid n bounded ; func diameter K -> Real equals :: SIMPLEX2:def 6 diameter ((Euclid n),K); coherence diameter ((Euclid n),K) is Real ; end; :: deftheorem Def5 defines bounded SIMPLEX2:def_5_:_ for n being Nat for K being SimplicialComplexStr of (TOP-REAL n) holds ( K is bounded iff K is Euclid n bounded ); :: deftheorem defines diameter SIMPLEX2:def_6_:_ for n being Nat for K being SimplicialComplexStr of (TOP-REAL n) holds diameter K = diameter ((Euclid n),K); registration let n be Nat; cluster bounded -> Euclid n bounded for SimplicialComplexStr of the carrier of (TOP-REAL n); coherence for b1 being SimplicialComplexStr of (TOP-REAL n) st b1 is bounded holds b1 is Euclid n bounded by Def5; cluster non void subset-closed finite-membered finite-degree total affinely-independent simplex-join-closed bounded for SimplicialComplexStr of the carrier of (TOP-REAL n); existence ex b1 being SimplicialComplex of (TOP-REAL n) st ( b1 is bounded & b1 is affinely-independent & b1 is simplex-join-closed & not b1 is void & b1 is finite-degree & b1 is total ) proofend; cluster finite-vertices -> bounded for SimplicialComplexStr of the carrier of (TOP-REAL n); coherence for b1 being SimplicialComplexStr of (TOP-REAL n) st b1 is finite-vertices holds b1 is bounded proofend; end; Lm2: for n being Nat holds [#] (TOP-REAL n) = [#] (Euclid n) proofend; begin Lm3: for x being set holds {x} is c=-linear proofend; theorem Th11: :: SIMPLEX2:11 for V being RealLinearSpace for Kv being non void SimplicialComplex of V for S being Simplex of (BCS Kv) for F being c=-linear finite finite-membered Subset-Family of V st S = (center_of_mass V) .: F holds for a1, a2 being VECTOR of V st a1 in S & a2 in S holds ex b1, b2 being VECTOR of V ex r being 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)) ) proofend; theorem Th12: :: SIMPLEX2:12 for n being Nat for X being set for A being affinely-independent Subset of (TOP-REAL n) for E being Enumeration of A st not (dom E) \ X is empty holds conv (E .: X) = meet { (conv (A \ {(E . k)})) where k is Element of NAT : k in (dom E) \ X } proofend; theorem Th13: :: SIMPLEX2:13 for n being Nat for A being Subset of (TOP-REAL n) for a being bounded Subset of (Euclid n) st a = A holds for p being Point of (Euclid n) st p in conv A holds conv A c= cl_Ball (p,(diameter a)) proofend; theorem Th14: :: SIMPLEX2:14 for n being Nat for A being Subset of (TOP-REAL n) holds ( A is bounded iff conv A is bounded ) proofend; theorem Th15: :: SIMPLEX2:15 for n being Nat for A being Subset of (TOP-REAL n) for a, ca being bounded Subset of (Euclid n) st ca = conv A & a = A holds diameter a = diameter ca proofend; registration let n be Nat; let K be bounded SimplicialComplexStr of (TOP-REAL n); cluster -> bounded for SubdivisionStr of K; coherence for b1 being SubdivisionStr of K holds b1 is bounded proofend; end; theorem Th16: :: SIMPLEX2:16 for n being Nat for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds diameter (BCS K) <= ((degree K) / ((degree K) + 1)) * (diameter K) proofend; theorem Th17: :: SIMPLEX2:17 for n, k being Nat for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds diameter (BCS (k,K)) <= (((degree K) / ((degree K) + 1)) |^ k) * (diameter K) proofend; theorem Th18: :: SIMPLEX2:18 for n being Nat for K being non void finite-degree bounded SimplicialComplex of (TOP-REAL n) st |.K.| c= [#] K holds for r being real number st r > 0 holds ex k being Nat st diameter (BCS (k,K)) < r proofend; theorem Th19: :: SIMPLEX2:19 for i, j being Element of NAT ex f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st ( f is being_homeomorphism & ( for fi being Element of (TOP-REAL i) for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) ) proofend; Lm4: for n being Nat holds [#] (TOP-REAL n) = [#] (TopSpaceMetr (Euclid n)) proofend; theorem Th20: :: SIMPLEX2:20 for i, j being Element of NAT for f being Function of [:(TOP-REAL i),(TOP-REAL j):],(TOP-REAL (i + j)) st ( for fi being Element of (TOP-REAL i) for fj being Element of (TOP-REAL j) holds f . (fi,fj) = fi ^ fj ) holds for r being real number for fi being Point of (Euclid i) for fj being Point of (Euclid j) for fij being Point of (Euclid (i + j)) st fij = fi ^ fj holds f .: [:(OpenHypercube (fi,r)),(OpenHypercube (fj,r)):] = OpenHypercube (fij,r) proofend; theorem Th21: :: SIMPLEX2:21 for n being Nat for A being Subset of (TOP-REAL n) holds ( A is bounded iff ex p being Point of (Euclid n) ex r being real number st A c= OpenHypercube (p,r) ) proofend; Lm5: for A being Subset of (TOP-REAL 1) st A is closed & A is bounded holds A is compact proofend; Lm6: for n being Nat for A being Subset of (TOP-REAL n) st A is closed & A is bounded holds A is compact proofend; registration let n be Nat; cluster closed bounded -> compact for Element of bool the carrier of (TOP-REAL n); coherence for b1 being Subset of (TOP-REAL n) st b1 is closed & b1 is bounded holds b1 is compact by Lm6; end; registration let n be Nat; let A be affinely-independent Subset of (TOP-REAL n); cluster conv A -> compact ; coherence conv A is compact proofend; end; begin theorem Th22: :: SIMPLEX2:22 for n being Nat for A being non empty affinely-independent Subset of (TOP-REAL n) for E being Enumeration of A for F being FinSequence of bool the carrier of ((TOP-REAL n) | (conv A)) st len F = card A & rng F is closed & ( for S being Subset of (dom F) holds conv (E .: S) c= union (F .: S) ) holds not meet (rng F) is empty proofend; theorem Th23: :: SIMPLEX2:23 for n being Nat for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) ex p being Point of (TOP-REAL n) st ( p in dom f & f . p = p ) proofend; theorem :: SIMPLEX2:24 for n being Nat for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds for f being continuous Function of ((TOP-REAL n) | (conv A)),((TOP-REAL n) | (conv A)) holds f is with_fixpoint proofend; theorem Th25: :: SIMPLEX2:25 for n being Nat for A being affinely-independent Subset of (TOP-REAL n) st card A = n + 1 holds ind (conv A) = n proofend; theorem :: SIMPLEX2:26 for n being Nat holds ind (TOP-REAL n) = n proofend;