environ
vocabularies HIDDEN, NUMBERS, TARSKI, FUNCT_1, CARD_1, RELAT_1, NAT_1, INT_1, XXREAL_0, SUBSET_1, ABIAN, ARYTM_3, ARYTM_1, NEWTON, POWER, FINSEQ_1, ORDINAL4, CARD_3, XBOOLE_0, BSPACE, FUNCT_2, ZFMISC_1, SUPINF_2, MESFUNC1, FUNCOP_1, PRE_POLY, RLVECT_5, FINSET_1, VECTSP_1, QC_LANG1, RLVECT_3, STRUCT_0, FINSEQ_2, RANKNULL, RLSUB_1, VECTSP10, ORDINAL2, POLYFORM, MSSUBFAM, UNIALG_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, BINOP_1, CARD_1, ORDINAL1, NUMBERS, FUNCOP_1, FINSET_1, XCMPLX_0, XXREAL_0, INT_1, CARD_2, FINSEQ_1, FINSEQ_2, POWER, RVSUM_1, NEWTON, ABIAN, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_7, FVSUM_1, MATRLIN, VECTSP_9, RANKNULL, BSPACE, PRE_POLY, MOD_2;
definitions XBOOLE_0, TARSKI;
theorems XBOOLE_0, FUNCT_1, RELAT_1, TARSKI, ZFMISC_1, FUNCT_2, GROUP_1, RLVECT_1, VECTSP_1, FVSUM_1, FINSEQ_2, CARD_1, FINSEQ_1, NAT_1, FINSOP_1, VECTSP_4, BSPACE, RANKNULL, VECTSP_9, ORDINAL1, NEWTON, RVSUM_1, GR_CY_1, FUNCOP_1, XREAL_1, XXREAL_0, INT_1, POWER, FIB_NUM2, CARD_2, FINSEQ_3, SUBSET_1, MOD_2, MATRIX_3, CALCUL_1, RELSET_1;
schemes FUNCT_2, FINSEQ_1, FINSEQ_2;
registrations FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1, SUBSET_1, NAT_1, INT_1, VECTSP_1, STRUCT_0, FINSEQ_1, FINSEQ_2, CARD_1, MATRLIN, BSPACE, ORDINAL1, NEWTON, FUNCOP_1, ABIAN, XREAL_0, NUMBERS, JORDAN23, PRE_POLY, XCMPLX_0, XXREAL_0, VALUED_0, PARTFUN1, RELSET_1, WSIERP_1;
constructors HIDDEN, VECTSP_9, REALSET1, FINSOP_1, FVSUM_1, BSPACE, REAL_1, BINOP_2, RANKNULL, VECTSP_7, VECTSP_5, NEWTON, GR_CY_1, ABIAN, POWER, CARD_2, RELSET_1, BINOP_1;
requirements HIDDEN, NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
equalities BINOP_1, STRUCT_0, FVSUM_1, FINSEQ_1, BSPACE, RANKNULL, ALGSTR_0;
expansions XBOOLE_0, BINOP_1, TARSKI, FINSEQ_1;
Lm1:
for x being Element of NAT st 0 < x holds
0 + 1 <= x
by NAT_1:13;
theorem Th10:
for
n being
Nat holds 1
< n + 2
definition
let p be
polyhedron;
let k be
Integer;
let x be
Element of
(k - 1) -polytopes p;
let v be
Element of
(k -chain-space p);
existence
ex b1 being FinSequence of Z_2 st
( ( (k - 1) -polytopes p is empty implies b1 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b1 = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b1 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )
uniqueness
for b1, b2 being FinSequence of Z_2 st ( (k - 1) -polytopes p is empty implies b1 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b1 = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b1 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) & ( (k - 1) -polytopes p is empty implies b2 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b2 = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b2 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) holds
b1 = b2
end;