:: Brouwer Fixed Point Theorem for Simplexes
:: by Karol P\kak
::
:: Received December 21, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users


begin

definition
let M be non empty MetrSpace;
assume A1: TopSpaceMetr M is compact ;
let F be Subset-Family of (TopSpaceMetr M);
assume that
A2: F is open and
A3: 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 )
proof end;
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
proof end;

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

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

begin

registration
let M be non empty Reflexive MetrStruct ;
cluster finite -> bounded Element of bool the carrier of M;
coherence
for b1 being Subset of M st b1 is finite holds
b1 is bounded
proof end;
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 )
proof end;

definition
let M be non empty Reflexive MetrStruct ;
let K be SimplicialComplexStr;
attr K 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
proof end;

registration
let M be non empty Reflexive MetrStruct ;
let X be set ;
cluster non void subset-closed finite-membered M bounded SimplicialComplexStr of X;
existence
ex b1 being SimplicialComplex of X st
( b1 is M bounded & not b1 is void )
proof end;
end;

registration
let M be non empty Reflexive MetrStruct ;
cluster non void subset-closed finite-membered M bounded TopStruct ;
existence
ex b1 being SimplicialComplexStr st
( b1 is M bounded & not b1 is void & b1 is subset-closed & b1 is finite-membered )
proof end;
end;

registration
let M be non empty Reflexive MetrStruct ;
let X be set ;
let K be M bounded SimplicialComplexStr of X;
cluster -> M bounded SubSimplicialComplex of K;
coherence
for b1 being SubSimplicialComplex of K holds b1 is M bounded
proof end;
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
proof end;

begin

X: 0 in REAL
by XREAL_0:def 1;

definition
let M be non empty Reflexive MetrStruct ;
let K be SimplicialComplexStr;
assume A1: 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 ) )
proof end;
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 ) )
proof end;
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)
proof end;

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

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

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

definition
let n be Nat;
let K be SimplicialComplexStr of (TOP-REAL n);
attr K 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 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 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 )
proof end;
cluster finite-vertices -> bounded 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
proof end;
end;

Lm1: for n being Nat holds [#] (TOP-REAL n) = [#] (Euclid n)
proof end;

begin

Lm2: for x being set holds {x} is c=-linear
proof end;

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 & union F is Simplex of Kv 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)) )
proof end;

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

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

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

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

registration
let n be Nat;
let K be bounded SimplicialComplexStr of (TOP-REAL n);
cluster -> bounded SubdivisionStr of K;
coherence
for b1 being SubdivisionStr of K holds b1 is bounded
proof end;
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)
proof end;

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

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

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

Lm3: for n being Nat holds [#] (TOP-REAL n) = [#] (TopSpaceMetr (Euclid n))
proof end;

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

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

Lm4: for A being Subset of (TOP-REAL 1) st A is closed & A is Bounded holds
A is compact
proof end;

Lm5: for n being Nat
for A being Subset of (TOP-REAL n) st A is closed & A is Bounded holds
A is compact
proof end;

registration
let n be Nat;
cluster closed Bounded -> compact 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 Lm5;
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
proof end;
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
proof end;

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

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

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

theorem :: SIMPLEX2:26
for n being Nat holds ind (TOP-REAL n) = n
proof end;