:: Brouwer Fixed Point Theorem for Simplexes
:: by Karol P\kak
::
:: Copyright (c) 2010-2021 Association of Mizar Users

reconsider jj = 1 as positive Real ;

definition
let M be non empty MetrSpace;
assume A1: TopSpaceMetr M is compact ;
let F be Subset-Family of ();
assume that
A2: F is open and
A3: F is Cover of () ;
mode Lebesgue_number of F -> positive Real means :Def1: :: SIMPLEX2:def 1
for p being Point of M ex A being Subset of () 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 () 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 () st F is open & F is Cover of () 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 () 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 ()
for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of () & 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 ()
for L being Lebesgue_number of F st TopSpaceMetr M is compact & F is Cover of () & 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 ()
for L being Lebesgue_number of F
for L1 being positive Real st TopSpaceMetr M is compact & F is Cover of () & L1 <= L holds
L1 is Lebesgue_number of F
proof end;

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
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 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 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 ;
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 ;
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 for 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 dim-like number ;
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;

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 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 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 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 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 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 dim-like number 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;
redefine func diameter (M,K) 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 st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= it ) );
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 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 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,()) = diameter S
proof end;

definition
let n be Nat;
let K be SimplicialComplexStr of ();
attr K is bounded means :: SIMPLEX2:def 5
K is Euclid n bounded ;
func diameter K -> Real equals :: SIMPLEX2:def 6
diameter ((),K);
coherence
diameter ((),K) is Real
;
end;

:: deftheorem defines bounded SIMPLEX2:def 5 :
for n being Nat
for K being SimplicialComplexStr of () 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 () holds diameter K = diameter ((),K);

registration
let n be Nat;
cluster bounded -> Euclid n bounded for SimplicialComplexStr of the carrier of ();
coherence
for b1 being SimplicialComplexStr of () st b1 is bounded holds
b1 is Euclid n bounded
;
existence
ex b1 being SimplicialComplex of () 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 for SimplicialComplexStr of the carrier of ();
coherence
for b1 being SimplicialComplexStr of () st b1 is finite-vertices holds
b1 is bounded
by Th6;
end;

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

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 = () .: 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 ()) & b2 in Vertices (BCS ()) & a1 - a2 = r * (b1 - b2) & 0 <= r & r <= ((card ()) - 1) / (card ()) )
proof end;

theorem Th12: :: SIMPLEX2:12
for n being Nat
for X being set
for A being affinely-independent Subset of ()
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 ()
for a being bounded Subset of () st a = A holds
for p being Point of () st p in conv A holds
conv A c= cl_Ball (p,())
proof end;

theorem Th14: :: SIMPLEX2:14
for n being Nat
for A being Subset of () holds
( A is bounded iff conv A is bounded )
proof end;

theorem Th15: :: SIMPLEX2:15
for n being Nat
for A being Subset of ()
for a, ca being bounded Subset of () st ca = conv A & a = A holds
diameter a = diameter ca
proof end;

registration
let n be Nat;
let K be bounded SimplicialComplexStr of ();
cluster -> bounded for 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 () st |.K.| c= [#] K holds
diameter (BCS K) <= (() / (() + 1)) * ()
proof end;

theorem Th17: :: SIMPLEX2:17
for n, k being Nat
for K being non void finite-degree bounded SimplicialComplex of () st |.K.| c= [#] K holds
diameter (BCS (k,K)) <= ((() / (() + 1)) |^ k) * ()
proof end;

theorem Th18: :: SIMPLEX2:18
for n being Nat
for K being non void finite-degree bounded SimplicialComplex of () st |.K.| c= [#] K holds
for r being Real 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 + j)) st
( f is being_homeomorphism & ( for fi being Element of ()
for fj being Element of () holds f . (fi,fj) = fi ^ fj ) )
proof end;

Lm3: for n being Nat holds [#] () = [#] ()
proof end;

theorem Th20: :: SIMPLEX2:20
for i, j being Element of NAT
for f being Function of [:(),():],(TOP-REAL (i + j)) st ( for fi being Element of ()
for fj being Element of () holds f . (fi,fj) = fi ^ fj ) holds
for r being Real
for fi being Point of ()
for fj being Point of ()
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 () holds
( A is bounded iff ex p being Point of () ex r being Real st A c= OpenHypercube (p,r) )
proof end;

Lm4: for A being Subset of () st A is closed & A is bounded holds
A is compact

proof end;

Lm5: for n being Nat
for A being Subset of () st A is closed & A is bounded holds
A is compact

proof end;

registration
let n be Nat;
cluster closed bounded -> compact for Element of bool the carrier of ();
coherence
for b1 being Subset of () 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 ();
coherence
conv A is compact
proof end;
end;

theorem Th22: :: SIMPLEX2:22
for n being Nat
for A being non empty affinely-independent Subset of ()
for E being Enumeration of A
for F being FinSequence of bool the carrier of (() | (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 () st card A = n + 1 holds
for f being continuous Function of (() | (conv A)),(() | (conv A)) ex p being Point of () st
( p in dom f & f . p = p )
proof end;

theorem :: SIMPLEX2:24
for n being Nat
for A being affinely-independent Subset of () st card A = n + 1 holds
for f being continuous Function of (() | (conv A)),(() | (conv A)) holds f is with_fixpoint
proof end;

theorem Th25: :: SIMPLEX2:25
for n being Nat
for A being affinely-independent Subset of () st card A = n + 1 holds
ind (conv A) = n
proof end;

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