let V be RealLinearSpace; :: thesis: for S being finite Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds
for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf})
let S be finite Subset-Family of V; :: thesis: ( S is c=-linear & S is with_non-empty_elements & card S = card (union S) implies for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf}) )
assume that
A1: ( S is c=-linear & S is with_non-empty_elements ) and
A2: card S = card (union S) ; :: thesis: for Af, Bf being finite Subset of V st not Af is empty & Af misses union S & (union S) \/ Af is affinely-independent & (union S) \/ Af c= Bf holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ Af)}) is Simplex of card S, BCS (Complex_of {Bf})
set U = union S;
set b = center_of_mass V;
let A, B be finite Subset of V; :: thesis: ( not A is empty & A misses union S & (union S) \/ A is affinely-independent & (union S) \/ A c= B implies ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {B}) )
assume that
A3: not A is empty and
A4: ( A misses union S & (union S) \/ A is affinely-independent ) and
A5: (union S) \/ A c= B ; :: thesis: ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {B})
reconsider UA = (union S) \/ A as finite Subset of V by A5;
dom (center_of_mass V) = (bool the carrier of V) \ {{}} by FUNCT_2:def 1;
then UA in dom (center_of_mass V) by A3, ZFMISC_1:56;
then A6: {((center_of_mass V) . UA)} = Im ((center_of_mass V),UA) by FUNCT_1:59
.= (center_of_mass V) .: {UA} by RELAT_1:def 16 ;
set CA = Complex_of {UA};
set CB = Complex_of {B};
{UA} is_finer_than {B}
proof
let x be set ; :: according to SETFAM_1:def 2 :: thesis: ( not x in {UA} or ex b1 being set st
( b1 in {B} & x c= b1 ) )
assume x in {UA} ; :: thesis: ex b1 being set st
( b1 in {B} & x c= b1 )
then A7: x = UA by TARSKI:def 1;
B in {B} by TARSKI:def 1;
hence ex b1 being set st
( b1 in {B} & x c= b1 ) by A5, A7; :: thesis: verum
end;
then Complex_of {UA} is SubSimplicialComplex of Complex_of {B} by SIMPLEX0:30;
then A8: subdivision ((center_of_mass V),(Complex_of {UA})) is SubSimplicialComplex of subdivision ((center_of_mass V),(Complex_of {B})) by SIMPLEX0:58;
|.(Complex_of {UA}).| c= [#] (Complex_of {UA}) ;
then A9: subdivision ((center_of_mass V),(Complex_of {UA})) = BCS (Complex_of {UA}) by Def5;
|.(Complex_of {B}).| c= [#] (Complex_of {B}) ;
then A10: BCS (Complex_of {UA}) is SubSimplicialComplex of BCS (Complex_of {B}) by A8, A9, Def5;
S is finite-membered
proof
let x be set ; :: according to FINSET_1:def 6 :: thesis: ( not x in S or x is finite )
assume x in S ; :: thesis: x is finite
then A11: x c= union S by ZFMISC_1:74;
union S is finite by A2;
hence x is finite by A11; :: thesis: verum
end;
then ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {UA}) is Simplex of card S, BCS (Complex_of {UA}) by A1, A2, A3, A4, Lm1;
hence ((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {B}) by A6, A10, SIMPLEX0:49; :: thesis: verum