:: Brouwer Fixed Point Theorem for Simplexes
:: by Karol P\kak
::
:: Received December 21, 2010
:: 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 (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 b₁ being positive Real st
for p being Point of M ex A being Subset of (TopSpaceMetr M) st
( A in F & Ball (p,b₁) 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 b₃ being positive Real holds
( b₃ 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,b₃) 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;

registration

let M be non empty Reflexive MetrStruct ;

cluster finite -> bounded for Element of bool the carrier of M;

coherence
for b₁ being Subset of M st b₁ is finite holds
b₁ 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 ;

cluster non void subset-closed finite-membered M bounded for SimplicialComplexStr of X;

existence
ex b₁ being SimplicialComplex of X st
( b₁ is M bounded & not b₁ is void )

proof end;

end;

registration

let M be non empty Reflexive MetrStruct ;

cluster non void subset-closed finite-membered M bounded for TopStruct ;

existence
ex b₁ being SimplicialComplexStr st
( b₁ is M bounded & not b₁ is void & b₁ is subset-closed & b₁ 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 b₁ being SubSimplicialComplex of K holds b₁ 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 b₁ being Real st
( ( for A being Subset of M st A in the topology of K holds
diameter A <= b₁ ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b₁ ) ) ) & ( not the topology of K meets bool ([#] M) implies ex b₁ being Real st b₁ = 0 ) )

proof end;

uniqueness
for b₁, b₂ 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 <= b₁ ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b₁ ) & ( for A being Subset of M st A in the topology of K holds
diameter A <= b₂ ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b₂ ) implies b₁ = b₂ ) & ( not the topology of K meets bool ([#] M) & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) )

proof end;

consistency
for b₁ 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 b₃ being Real holds
( ( the topology of K meets bool ([#] M) implies ( b₃ = diameter (M,K) iff ( ( for A being Subset of M st A in the topology of K holds
diameter A <= b₃ ) & ( for r being Real st ( for A being Subset of M st A in the topology of K holds
diameter A <= r ) holds
r >= b₃ ) ) ) ) & ( not the topology of K meets bool ([#] M) implies ( b₃ = diameter (M,K) iff b₃ = 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 b₂ 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 b₂ 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 b₁ being Real holds
( b₁ = diameter (M,K) iff ( ( for A being Subset of M st A is Simplex of K holds
diameter A <= b₁ ) & ( for r being Real st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= b₁ ) ) )

proof end;

end;

:: deftheorem Def4 defines diameter SIMPLEX2:def 4 :
for M being non empty Reflexive MetrStruct
for K being non void subset-closed b₁ bounded SimplicialComplexStr
for b₃ being Real holds
( b₃ = diameter (M,K) iff ( ( for A being Subset of M st A is Simplex of K holds
diameter A <= b₃ ) & ( for r being Real st ( for A being Subset of M st A is Simplex of K holds
diameter A <= r ) holds
r >= b₃ ) ) );

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 :: 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 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 b₁ being SimplicialComplexStr of (TOP-REAL n) st b₁ is bounded holds
b₁ is Euclid n bounded ;

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 b₁ being SimplicialComplex of (TOP-REAL n) st
( b₁ is bounded & b₁ is affinely-independent & b₁ is simplex-join-closed & not b₁ is void & b₁ is finite-degree & b₁ is total )

proof end;

cluster finite-vertices -> bounded for SimplicialComplexStr of the carrier of (TOP-REAL n);

coherence
for b₁ being SimplicialComplexStr of (TOP-REAL n) st b₁ is finite-vertices holds
b₁ is bounded by Th6;

end;

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

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 = (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)) )

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 for SubdivisionStr of K;

coherence
for b₁ being SubdivisionStr of K holds b₁ 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 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
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 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 for Element of bool the carrier of (TOP-REAL n);

coherence
for b₁ being Subset of (TOP-REAL n) st b₁ is closed & b₁ is bounded holds
b₁ 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;

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 is with_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;