let V be RealLinearSpace; :: thesis: for Kas being non void affinely-independent simplex-join-closed SimplicialComplex of V
for S being simplex-like Subset-Family of Kas st S is with_non-empty_elements holds
card S = card ((center_of_mass V) .: S)
let Kas be non void affinely-independent simplex-join-closed SimplicialComplex of V; :: thesis: for S being simplex-like Subset-Family of Kas st S is with_non-empty_elements holds
card S = card ((center_of_mass V) .: S)
set B = center_of_mass V;
set T = the topology of Kas;
let S be simplex-like Subset-Family of Kas; :: thesis: ( S is with_non-empty_elements implies card S = card ((center_of_mass V) .: S) )
assume A1: S is with_non-empty_elements ; :: thesis: card S = card ((center_of_mass V) .: S)
A2: not {} in S by A1;
[#] Kas c= the carrier of V by SIMPLEX0:def 9;
then bool the carrier of Kas c= bool the carrier of V by ZFMISC_1:67;
then ( dom (center_of_mass V) = (bool the carrier of V) \ {{}} & S c= bool the carrier of V ) by FUNCT_2:def 1;
then A3: dom ((center_of_mass V) | S) = S by A2, RELAT_1:62, ZFMISC_1:34;
S c= the topology of Kas
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in the topology of Kas )
assume x in S ; :: thesis: x in the topology of Kas
then x is Simplex of Kas by TOPS_2:def 1;
hence x in the topology of Kas by PRE_TOPC:def 2; :: thesis: verum
end;
then ((center_of_mass V) | the topology of Kas) | S = (center_of_mass V) | S by RELAT_1:74;
then A4: (center_of_mass V) | S is one-to-one by FUNCT_1:52;
(center_of_mass V) .: S = rng ((center_of_mass V) | S) by RELAT_1:115;
then S,(center_of_mass V) .: S are_equipotent by A3, A4, WELLORD2:def 4;
hence card S = card ((center_of_mass V) .: S) by CARD_1:5; :: thesis: verum