let V be RealLinearSpace; :: thesis: for Kv being non void SimplicialComplex of V st |.Kv.| c= [#] Kv & ( for n being Nat st n <= degree Kv holds
ex S being Simplex of Kv st
( card S = n + 1 & @ S is affinely-independent ) ) holds
degree Kv = degree (BCS Kv)
let Kv be non void SimplicialComplex of V; :: thesis: ( |.Kv.| c= [#] Kv & ( for n being Nat st n <= degree Kv holds
ex S being Simplex of Kv st
( card S = n + 1 & @ S is affinely-independent ) ) implies degree Kv = degree (BCS Kv) )
assume that
A1: |.Kv.| c= [#] Kv and
A2: for n being Nat st n <= degree Kv holds
ex S being Simplex of Kv st
( card S = n + 1 & @ S is affinely-independent ) ; :: thesis: degree Kv = degree (BCS Kv)
A3: dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;
A4: for n being Nat st n <= degree Kv holds
ex S being Subset of Kv st
( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )
proof
let n be Nat; :: thesis: ( n <= degree Kv implies ex S being Subset of Kv st
( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one ) )
assume n <= degree Kv ; :: thesis: ex S being Subset of Kv st
( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )
then consider S being Simplex of Kv such that
A5: card S = n + 1 and
A6: @ S is affinely-independent by A2;
take S ; :: thesis: ( S is simplex-like & card S = n + 1 & BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )
thus ( S is simplex-like & card S = n + 1 ) by A5; :: thesis: ( BOOL S c= dom (center_of_mass V) & (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )
A7: the topology of (Complex_of {(@ S)}) = bool S by SIMPLEX0:4;
reconsider SS = {(@ S)} as affinely-independent Subset-Family of V by A6;
A8: (center_of_mass V) .: (BOOL S) c= conv (@ S)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (center_of_mass V) .: (BOOL S) or y in conv (@ S) )
assume y in (center_of_mass V) .: (BOOL S) ; :: thesis: y in conv (@ S)
then consider x being object such that
A9: x in dom (center_of_mass V) and
A10: ( x in BOOL S & (center_of_mass V) . x = y ) by FUNCT_1:def 6;
reconsider x = x as non empty Subset of V by A9, ZFMISC_1:56;
( conv x c= conv (@ S) & y in conv x ) by A10, RLAFFIN2:16, RLTOPSP1:20;
hence y in conv (@ S) ; :: thesis: verum
end;
bool (@ S) c= bool the carrier of V by ZFMISC_1:67;
hence BOOL S c= dom (center_of_mass V) by A3, XBOOLE_1:33; :: thesis: ( (center_of_mass V) .: (BOOL S) is Subset of Kv & (center_of_mass V) | (BOOL S) is one-to-one )
conv (@ S) c= |.Kv.| by Th5;
then conv (@ S) c= [#] Kv by A1;
hence (center_of_mass V) .: (BOOL S) is Subset of Kv by A8, XBOOLE_1:1; :: thesis: (center_of_mass V) | (BOOL S) is one-to-one
( ((center_of_mass V) | (bool S)) | (BOOL S) = (center_of_mass V) | (BOOL S) & Complex_of SS is SimplicialComplex of V ) by RELAT_1:74;
hence (center_of_mass V) | (BOOL S) is one-to-one by A6, A7, FUNCT_1:52; :: thesis: verum
end;
not {} in dom (center_of_mass V) by ZFMISC_1:56;
then A11: dom (center_of_mass V) is with_non-empty_elements ;
BCS Kv = subdivision ((center_of_mass V),Kv) by A1, Def5;
hence degree Kv = degree (BCS Kv) by A4, A11, SIMPLEX0:53; :: thesis: verum