begin
theorem Th1:
theorem Th2:
:: deftheorem defines @ SIMPLEX1:def 1 :
:: deftheorem defines @ SIMPLEX1:def 2 :
theorem Th3:
begin
:: deftheorem Def3 defines |. SIMPLEX1:def 3 :
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem
begin
:: deftheorem Def4 defines SubdivisionStr SIMPLEX1:def 4 :
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
begin
:: deftheorem Def5 defines BCS SIMPLEX1:def 5 :
:: deftheorem Def6 defines BCS SIMPLEX1:def 6 :
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
Lm1:
for n being Nat holds card n = n
theorem Th24:
begin
:: deftheorem Def7 defines affinely-independent SIMPLEX1:def 7 :
:: deftheorem Def8 defines simplex-join-closed SIMPLEX1:def 8 :
theorem Th25:
theorem Th26:
theorem
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
Lm2:
for V being RealLinearSpace
for S being finite finite-membered Subset-Family of V st S is c=-linear & S is with_non-empty_elements & card S = card (union S) holds
for A being non empty finite Subset of V st A misses union S & (union S) \/ A is affinely-independent holds
((center_of_mass V) .: S) \/ ((center_of_mass V) .: {((union S) \/ A)}) is Simplex of card S, BCS (Complex_of {((union S) \/ A)})
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
begin
theorem Th46:
theorem