:: Euler's Polyhedron Formula
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
environ
vocabularies FINSET_1, FUNCT_1, FUNCT_2, CARD_1, SUBSET_1, TARSKI, BOOLE,
RELAT_1, ORDINAL2, VECTSP_1, VECTSP_9, INT_1, RLVECT_1, GROUP_1, ARYTM_1,
FINSEQ_1, FINSEQ_2, QC_LANG1, RLSUB_1, BSPACE, RANKNULL, RLVECT_3,
MATRLIN, FINSEQ_4, POLYFORM, VECTSP10, SEQ_1, PRALG_1, MATRIX_2, POWER,
FUNCOP_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, WELLORD2, MCART_1, FUNCT_2, FUNCT_3,
BINOP_1, NUMBERS, ORDINAL1, ORDINAL2, ARYTM_3, FUNCOP_1, FINSET_1,
SETWISEO, XCMPLX_0, COMPLEX1, XXREAL_0, REAL_1, NAT_1, INT_1, CARD_1,
CARD_2, FINSEQ_1, SEQ_1, FINSEQ_2, MCART_2, FINSEQ_4, POWER, FINSOP_1,
RVSUM_1, NEWTON, WSIERP_1, REALSET1, ABIAN, STRUCT_0, LATTICES, RLVECT_1,
GROUP_1, ALGSTR_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7,
MOD_2, FVSUM_1, GR_CY_1, MATRLIN, VECTSP_9, RANKNULL, BSPACE;
constructors FINSET_1, XBOOLE_0, NAT_1, FUNCT_1, FUNCT_2, CARD_1, ZFMISC_1,
SUBSET_1, TARSKI, MCART_1, RELAT_1, NUMBERS, ORDINAL1, ORDINAL2,
RLVECT_1, LATTICES, GROUP_1, VECTSP_1, VECTSP_9, INT_1, STRUCT_0,
BINOP_1, MCART_2, FRAENKEL, ENUMSET1, RELSET_1, PARTFUN1, REALSET1,
FINSEQ_1, FINSOP_1, XXREAL_0, FINSEQ_2, FVSUM_1, SETWOP_2, WELLORD2,
SETWISEO, ALGSTR_1, VECTSP_4, BSPACE, SETFAM_1, RELAT_2, PBOOLE, REAL_1,
COMPLEX1, INT_2, BINOP_2, FINSEQOP, NAT_D, GROUP_2, GROUP_3, GROUP_4,
MATRIX_2, WELLORD1, FUNCT_3, RANKNULL, MOD_2, VECTSP_6, VECTSP_7,
MATRLIN, FINSEQ_4, RFINSEQ, VECTSP_5, NEWTON, WSIERP_1, RVSUM_1, GR_CY_1,
FUNCOP_1, ABIAN, ARYTM_3, POWER, XREAL_0, SEQ_1, CARD_2, INT_3, XCMPLX_0;
registrations FRAENKEL, FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1,
SUBSET_1, NAT_1, INT_1, VECTSP_1, STRUCT_0, RLVECT_1, RELSET_1, FVSUM_1,
FINSEQ_1, REALSET1, FINSEQ_2, SETWISEO, VECTSP_4, ZFMISC_1, RANKNULL,
MOD_2, VECTSP_7, CARD_1, MATRLIN, BSPACE, VECTSP_9, FINSEQ_4, RFINSEQ,
ORDINAL1, ORDINAL2, VECTSP_5, NEWTON, RVSUM_1, GR_CY_1, FUNCOP_1,
FUNCT_7, POLYNOM1, ABIAN, ARYTM_3, XREAL_0, SEQ_1, NUMBERS, JORDAN23,
INT_3, INT_2, ARMSTRNG, GOBRD13, XCMPLX_0, PARTFUN1, XXREAL_0, GROUP_1,
FINSUB_1, ALGSTR_1;
requirements NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
definitions XBOOLE_0, RELAT_1, FUNCT_1, SUBSET_1, FUNCT_2, MCART_2, ENUMSET1,
RLVECT_1, BINOP_1, STRUCT_0, GROUP_1, VECTSP_1, TARSKI, REALSET1,
FVSUM_1, FINSEQ_1, ZFMISC_1, FINSEQ_2, VECTSP_4, BSPACE, RANKNULL, MOD_2,
VECTSP_6, VECTSP_7, CARD_1, MATRLIN, VECTSP_9, FUNCT_3, FINSEQ_4,
RFINSEQ, ORDINAL1, ORDINAL2, VECTSP_5, NEWTON, WSIERP_1, RVSUM_1,
GR_CY_1, FUNCOP_1, ABIAN, ARYTM_3, INT_1, POWER, XREAL_0, SEQ_1, CARD_2,
INT_3, INT_2;
theorems XBOOLE_0, FUNCT_1, RELAT_1, XBOOLE_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, JORDAN16, POWER,
FIB_NUM2, SEQ_1, NUMBERS, CARD_2, PRE_CIRC, FINSEQ_3, SUBSET_1, MOD_2,
MATRIX_3, CALCUL_1, PARTFUN1;
schemes FUNCT_2, FINSEQ_1, FINSEQ_2;
begin
theorem Th1:
for X,c,d being set
st (ex a,b being set st a <> b & X = {a,b}) &
c in X &
d in X &
c <> d
holds X = {c,d}
proof
let X,c,d be set such that
A1: ex a,b being set st a <> b & X = {a,b} and
A2: c in X and
A3: d in X and
A4: c <> d;
consider a,b being set such that
a <> b and
A5: X = {a,b} by A1;
A6: {c,d} c= X by A2,A3,ZFMISC_1:38;
X c= {c,d}
proof
A7: c = a or c = b by A2,A5,TARSKI:def 2;
A8: d = a or d = b by A3,A5,TARSKI:def 2;
let x be set such that
A9: x in X;
per cases by A5,A9,TARSKI:def 2;
suppose x = a;
hence thesis by A4,A7,A8,TARSKI:def 2;
end;
suppose x = b;
hence thesis by A4,A7,A8,TARSKI:def 2;
end;
end;
hence thesis by A6,XBOOLE_0:def 10;
end;
theorem Th2:
for f being Function st f is one-to-one
holds Card (dom f) = Card (rng f)
proof
let f be Function such that
A1: f is one-to-one;
A2: dom f, f .: (dom f) are_equipotent by A1,CARD_1:60;
f .: (dom f) = rng f by RELAT_1:146;
hence thesis by A2,CARD_1:21;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Arithmetical Preliminaries
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
reserve n for Nat,
k for Integer;
theorem Th3:
1 <= k implies k is Nat
proof
assume A1: 1 <= k;
reconsider k as Element of NAT by A1,INT_1:16;
k is Nat;
hence thesis;
end;
definition
let a be Integer,
b be Nat;
redefine func
a*b -> Element of INT;
coherence by INT_1:def 2;
end;
theorem Th4:
1 is odd
proof
1 = 2*0 + 1;
hence thesis;
end;
theorem Th5:
2 is even
proof
2 = 2*1;
hence thesis;
end;
theorem Th6:
3 is odd
proof
3 = 2*1 + 1;
hence thesis;
end;
theorem Th7:
4 is even
proof
4 = 2*2;
hence thesis;
end;
theorem Th8:
n is even implies (-1)|^n = 1
proof
assume A1: n is even;
reconsider n as Element of NAT by ORDINAL1:def 13;
(-1)|^n = (-1) to_power n by POWER:48;
hence thesis by A1,FIB_NUM2:5;
end;
theorem Th9:
n is odd implies (-1)|^n = -1
proof
assume A1: n is odd;
reconsider n as Element of NAT by ORDINAL1:def 13;
(-1)|^n = (-1) to_power n by POWER:46;
hence thesis by A1,FIB_NUM2:3;
end;
theorem Th10:
(-1) |^ n is Integer
proof
per cases;
suppose n is even;
hence thesis by Th8;
end;
suppose n is odd;
hence thesis by Th9;
end;
end;
definition
let a be Integer,
n be Nat;
redefine func
a |^ n -> Element of INT;
coherence
proof
consider b being Element of NAT such that
A1: a = b or a = -b by INT_1:8;
per cases by A1;
suppose A2: a = b;
reconsider a as Element of NAT by A2;
reconsider s = a |^ n as Element of NAT by ORDINAL1:def 13;
s in NAT;
hence thesis by NUMBERS:17;
end;
suppose A3: a = -b;
A4: -b = (-1)*b;
reconsider bn = b |^ n as Element of NAT by ORDINAL1:def 13;
A5: (-1) |^n is Integer by Th10;
reconsider l = (-1) |^ n as Element of INT by A5,INT_1:def 2;
a |^ n = l*bn by A3,A4,NEWTON:12;
hence thesis;
end;
end;
end;
Lm1: for x being Element of NAT st 0 < x holds 0+1 <= x by NAT_1:13;
theorem Th11:
for p,q,r being FinSequence holds
len (p ^ q) <= len (p ^ (q ^ r))
proof
let p,q,r be FinSequence;
len ((p ^ q) ^ r) = len (p ^ (q ^ r)) by FINSEQ_1:45;
hence thesis by CALCUL_1:6;
end;
theorem Th12:
1 < n + 2
proof
0 < n + 1 implies 1 < n + 2
proof
assume 0 < n + 1;
0 + 1 = 1;
hence thesis by XREAL_1:10;
end;
hence thesis;
end;
theorem Th13:
(-1)|^2 = 1
proof
(-1)|^2 = (-1)|^(1+1)
.= ((-1)|^1)*((-1)|^1) by NEWTON:13
.= ((-1)|^1)*(-1) by NEWTON:10
.= (-1)*(-1) by NEWTON:10;
hence thesis;
end;
theorem Th14:
for n being Nat
holds (-1)|^n = (-1)|^(n+2)
proof
let n be Nat;
(-1)|^(n+2) = ((-1)|^n)*((-1)|^2) by NEWTON:13
.= (-1)|^n by Th13;
hence thesis;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Preliminaries on Finite Sequences
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
registration
let f be FinSequence of INT,
k be Nat;
cluster f.k -> integer;
coherence
proof
per cases;
suppose k in dom f;
then f.k = f/.k by PARTFUN1:def 8;
hence thesis;
end;
suppose not k in dom f;
hence thesis by FUNCT_1:def 4;
end;
end;
end;
:: A theorem on telescoping sequences of integers.
theorem Th15:
for a,b,s being FinSequence of INT
st len s > 0 &
len a = len s &
len b = len s &
(for n being Nat
st 1 <= n & n <= len s
holds s.n = a.n + b.n) &
(for k being Nat
st 1 <= k & k < len s
holds b.k = -(a.(k+1)))
holds Sum s = (a.1) + (b.(len s))
proof
let a,b,s be FinSequence of INT such that
A1: len s > 0 and
A2: len a = len s and
A3: len b = len s and
A4: for n being Nat
st 1 <= n & n <= len s
holds s.n = a.n + b.n and
A5: for k being Nat
st 1 <= k & k < len s
holds b.k = -(a.(k+1));
defpred P[FinSequence of INT] means
len $1 > 0 implies
for a,b being FinSequence of INT
st len a = len $1 &
len b = len $1 &
(for n being Nat
st 1 <= n & n <= len $1
holds $1.n = a.n + b.n) &
(for k being Nat
st 1 <= k & k < len $1
holds b.k = -(a.(k+1)))
holds Sum $1 = a.1 + b.(len $1);
A6: P[<*>INT] by FINSEQ_1:32;
A7: for p being FinSequence of INT,
x being Element of INT
st P[p]
holds P[p^<*x*>]
proof
let p be FinSequence of INT,
x be Element of INT such that
A8: P[p];
set t = p ^ <*x*>;
assume len t > 0; :: this is outright provable, of course
let a,b be FinSequence of INT such that
A9: len a = len t and
A10: len b = len t and
A11: for n being Nat
st 1 <= n & n <= len t
holds t.n = a.n + b.n and
A12: for k being Nat
st 1 <= k & k < len t
holds b.k = -(a.(k+1));
A13: Sum t = (Sum p) + x by GR_CY_1:20;
per cases;
suppose A14: len p = 0;
A15: Sum p = 0 by A14,FINSEQ_1:25,GR_CY_1:22;
A16: t = <*x*>
proof
p = {} by A14,FINSEQ_1:25;
hence thesis by FINSEQ_1:47;
end;
A17: len t = 1 by A16,FINSEQ_1:56;
reconsider egy = 1 as Nat;
A18: egy <= len t by A16,FINSEQ_1:56;
t.egy = a.egy + b.egy by A11,A18;
hence thesis by A13,A15,A16,A17,FINSEQ_1:57;
end;
suppose A19: len p > 0;
set m = len p;
set a' = a|m;
set b' = b|m;
A20: m <= len a & m <= len b by A9,A10,CALCUL_1:6;
A21: len a' = len p by A20,FINSEQ_1:80;
A22: len b' = len p by A20,FINSEQ_1:80;
A23: for n being Nat
st 1 <= n & n <= len p
holds p.n = a'.n + b'.n
proof
let n be Nat such that
A24: 1 <= n and
A25: n <= len p;
A26: len p <= len t by CALCUL_1:6;
A27: n <= len t by A25,A26,XXREAL_0:2;
A28: dom p = Seg len p by FINSEQ_1:def 3;
A29: n in dom p by A24,A25,A28,FINSEQ_1:3;
reconsider n as Element of NAT by ORDINAL1:def 13;
p.n = t.n by A29,FINSEQ_1:def 7
.= a.n + b.n by A11,A24,A27
.= a'.n + b.n by A25,FINSEQ_3:121
.= a'.n + b'.n by A25,FINSEQ_3:121;
hence thesis;
end;
A30: for n being Nat
st 1 <= n & n < len p
holds b'.n = -(a'.(n+1))
proof
let n be Nat such that
A31: 1 <= n and
A32: n < len p;
reconsider n as Element of NAT by ORDINAL1:def 13;
A33: b'.n = b.n by A32,FINSEQ_3:121;
A34: n + 1 <= len p by A32,INT_1:20;
A35: len p <= len t by CALCUL_1:6;
A36: n < len t by A32,A35,XXREAL_0:2;
a'.(n+1) = a.(n+1) by A34,FINSEQ_3:121;
hence thesis by A12,A31,A33,A36;
end;
A37: Sum p = a'.1 + b'.(len p) by A8,A19,A21,A22,A23,A30;
A38: a'.1 = a.1
proof
reconsider egy = 1 as Element of NAT;
A39: 0 + 1 = 1;
egy <= len p by A19,A39,INT_1:20;
hence thesis by FINSEQ_3:121;
end;
x = -(b'.(len p)) + b.(len t)
proof
A40: len t = (len p) + 1
proof
len <*x*> = 1 by FINSEQ_1:56;
hence thesis by FINSEQ_1:35;
end;
A41: 1 <= len t
proof
0 + 1 = 1;
hence thesis by A40,XREAL_1:8;
end;
A42: a.(len t) = -(b'.(len p))
proof
A43: len p < len t
proof
0 + len p = len p;
hence thesis by A40,XREAL_1:8;
end;
A44: 1 <= len p by A19,Lm1;
A45: b.(len p) = -(a.(len p + 1)) by A12,A43,A44;
b.(len p) = b'.(len p) by FINSEQ_3:121;
hence thesis by A40,A45;
end;
x = t.(len p + 1) by FINSEQ_1:59
.= -(b'.(len p)) + b.(len t) by A11,A40,A41,A42;
hence thesis;
end;
hence thesis by A13,A37,A38;
end;
end;
for p being FinSequence of INT holds P[p] from FINSEQ_2:sch 2(A6,A7);
hence thesis by A1,A2,A3,A4,A5;
end;
theorem Th16:
for p,q,r being FinSequence holds
len (p ^ q ^ r) = (len p) + (len q) + (len r)
proof
let p,q,r be FinSequence;
len (p ^ q ^ r) = (len (p ^ q)) + (len r) by FINSEQ_1:35
.= ((len p) + (len q)) + (len r) by FINSEQ_1:35;
hence thesis;
end;
theorem Th17:
for x being set,
p,q being FinSequence
holds (<*x*> ^ p ^ q).1 = x
proof
let x be set,
p,q be FinSequence;
<*x*> ^ p ^ q = <*x*> ^ (p ^ q) by FINSEQ_1:45;
hence thesis by FINSEQ_1:58;
end;
theorem Th18:
for x being set,
p,q being FinSequence
holds (p ^ q ^ <*x*>).((len p) + (len q) + 1) = x
proof
let x be set,
p,q be FinSequence;
set s = p ^ q;
(s ^ <*x*>).((len s) + 1) = x by FINSEQ_1:59;
hence thesis by FINSEQ_1:35;
end;
theorem Th19:
for p,q,r being FinSequence,
k being Nat
st len p < k & k <= len (p ^ q)
holds (p ^ q ^ r).k = q.(k - (len p))
proof
let p,q,r be FinSequence,
k be Nat such that
A1: len p < k and
A2: k <= len (p ^ q);
A3: len (p ^ q) <= len (p ^ (q ^ r)) by Th11;
A4: k <= len (p ^ (q ^ r)) by A2,A3,XXREAL_0:2;
A5: (p ^ (q ^ r)).k = (q ^ r).(k - (len p)) by A1,A4,FINSEQ_1:37;
set n = k - (len p);
A6: (len p) - (len p) = 0;
A7: 0 < n by A1,A6,XREAL_1:11;
A8: 0 + 1 = 1;
A9: 1 <= n by A7,A8,INT_1:20;
reconsider n as Nat by A9,Th3;
A10: k <= (len p) + (len q) by A2,FINSEQ_1:35;
A11: n <= len q
proof
((len p) + (len q)) - (len p) = len q;
hence thesis by A10,XREAL_1:11;
end;
A12: n in Seg (len q) by A9,A11,FINSEQ_1:3;
A13: n in dom q by A12,FINSEQ_1:def 3;
reconsider n as Element of NAT by ORDINAL1:def 13;
(q ^ r).n = q.n by A13,FINSEQ_1:def 7;
hence thesis by A5,FINSEQ_1:45;
end;
definition
let a be Integer;
redefine func
<*a*> -> FinSequence of INT;
coherence
proof
set s = <*a*>;
A1: rng s = {a} by FINSEQ_1:55;
A2: a in INT by INT_1:def 2;
{a} c= INT by A2,ZFMISC_1:37;
hence thesis by A1,FINSEQ_1:def 4;
end;
end;
definition
let a,b be Integer;
redefine func
<*a,b*> -> FinSequence of INT;
coherence
proof
set s = <*a,b*>;
A1: rng s = {a,b} by FINSEQ_2:147;
{a,b} c= INT
proof
a in INT & b in INT by INT_1:def 2;
hence thesis by ZFMISC_1:38;
end;
hence thesis by A1,FINSEQ_1:def 4;
end;
end;
definition
let a,b,c be Integer;
redefine func
<*a,b,c*> -> FinSequence of INT;
coherence
proof
set s = <*a,b,c*>;
A1: rng s = {a,b,c} by FINSEQ_2:148;
{a,b,c} c= INT
proof
A2: a in INT by INT_1:def 2;
A3: b in INT by INT_1:def 2;
c in INT by INT_1:def 2;
hence thesis by A2,A3,JORDAN16:2;
end;
hence thesis by A1,FINSEQ_1:def 4;
end;
end;
definition
let p,q be FinSequence of INT;
redefine func
p ^ q -> FinSequence of INT;
coherence by FINSEQ_1:96;
end;
theorem Th20:
for p,q being FinSequence of INT
holds Sum (p ^ q) = (Sum p) + (Sum q)
proof
let p,q be FinSequence of INT;
A1: rng p c= REAL by NUMBERS:15,XBOOLE_1:1;
A2: rng q c= REAL by NUMBERS:15,XBOOLE_1:1;
reconsider p,q as real-yielding FinSequence by A1,A2,SEQ_1:def 1;
Sum (p ^ q) = (Sum p) + (Sum q) by RVSUM_1:105;
hence thesis;
end;
theorem Th21:
for k being Integer,
p being FinSequence of INT
holds Sum (<*k*> ^ p) = k + (Sum p)
proof
let k be Integer,
p be FinSequence of INT;
reconsider k as Element of INT by INT_1:def 2;
Sum (<*k*> ^ p) = (Sum p) + (Sum <*k*>) by Th20
.= Sum (p ^ <*k*>) by Th20
.= k + (Sum p) by GR_CY_1:20;
hence thesis;
end;
theorem Th22:
for p,q,r being FinSequence of INT
holds Sum (p ^ q ^ r) = (Sum p) + (Sum q) + (Sum r)
proof
let p,q,r be FinSequence of INT;
Sum (p ^ q ^ r) = (Sum (p ^ q)) + (Sum r) by Th20
.= ((Sum p) + (Sum q)) + Sum r by Th20;
hence thesis;
end;
theorem
for a being Element of Z_2
holds Sum <*a*> = a by FINSOP_1:12;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Polyhedra and Incidence Matrices
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
:: An incidence matrix is a function that says of any two objects
:: (contained in some set) whether they are incidence to each other.
definition
let X,Y be set;
mode
incidence-matrix of X,Y
is
Element of Funcs([:X,Y:],{0.Z_2,1.Z_2});
end;
theorem Th24:
for X,Y being set
holds [:X,Y:] --> 1.Z_2 is incidence-matrix of X,Y
proof
let X,Y be set;
set f = [:X,Y:] --> 1.Z_2;
A1: dom f = [:X,Y:] by FUNCOP_1:19;
A2: rng f c= {1.Z_2} by FUNCOP_1:19;
A3: {1.Z_2} c= {0.Z_2,1.Z_2} by ZFMISC_1:12;
rng f c= {0.Z_2,1.Z_2} by A2,A3,XBOOLE_1:1;
hence thesis by A1,FUNCT_2:def 2;
end;
:: A polyhedron (one might call it an abstract polyhedron) consists of
:: two pieces of data: a sequence of ordered sets, representing the
:: polytope sets (they are ordered for convenience's sake) and a
:: sequence of incidence matrices, which lays out the incidence
:: relation between the (k-1)-polytopes and the k-polytopes.
definition
mode
polyhedron
means :Def1:
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence st
len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
it = [F,I];
existence
proof
reconsider F = <*<*{}*>*> as FinSequence-yielding FinSequence;
reconsider I = <*>{} as Function-yielding FinSequence;
A1: len F = 1 by FINSEQ_1:56;
A2: len I = 1-1 by FINSEQ_1:32;
A3: for n being Nat
st 1 <= n & n < 1
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1));
A4: for n being Nat
st 1 <= n & n <= 1
holds F.n is non empty & F.n is one-to-one
proof
let n be Nat such that
A5: 1 <= n and
A6: n <= 1;
n = 1 by A5,A6,XXREAL_0:1;
hence thesis by FINSEQ_1:def 8;
end;
take [F,I];
thus thesis by A1,A2,A3,A4;
end;
end;
reserve p for polyhedron,
k for Integer,
n for Nat;
:: The dimension dim(p) of a polyhedron p is just the number of
:: polytope sets that it has.
definition
let p be polyhedron;
func
dim(p) -> Element of NAT
means :Def2:
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence
st len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
p = [F,I] &
it = len F;
existence
proof
consider F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence such that
A1: len I = len F - 1 and
A2: for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
A3: for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one and
A4: p = [F,I] by Def1;
take len F;
thus thesis by A1,A2,A3,A4;
end;
uniqueness by ZFMISC_1:33;
end;
:: For integers k such that 0 <= k <= dim(p), the set of k-polytopes
:: is data already given by the polyhedron. For k = dim(p), the set
:: is the singleton {p}, which seems clear enough. For k = -1, it is
:: convenient to define the set of k-polytopes to be {{}}. Doing this
:: ensures that, if p is simply connected, then any two vertices are
:: connected by a system of edges.
::
:: For k < -1 and k > dim(p), the set of k-polytopes of p is empty.
definition
let p be polyhedron,
k be Integer;
func
k-polytopes(p) -> finite set
means :Def3:
(k < -1 implies it = {}) &
(k = -1 implies it = {{}}) &
(-1 < k & k < dim(p) implies
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence
st len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
p = [F,I] &
it = rng (F.(k+1))) &
(k = dim(p) implies it = {p}) &
(k > dim(p) implies it = {});
existence
proof
consider F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence such that
A1: len I = len F - 1 and
A2: for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
A3: for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one and
A4: p = [F,I] by Def1;
per cases by XXREAL_0:1;
suppose A5: k < -1;
take {};
thus thesis by A5;
end;
suppose A6: k = -1;
take {{}};
thus thesis by A6;
end;
suppose A7: -1 < k & k < dim(p);
A8: -1 + 1 = 0;
A9: 0 <= k by A7,A8,INT_1:20;
reconsider k as Element of NAT by A9,INT_1:16;
set n = k + 1;
reconsider Fn = F.n as FinSequence;
take rng Fn;
thus thesis by A1,A2,A3,A4,A7;
end;
suppose A10: k = dim(p);
take {p};
thus thesis by A10;
end;
suppose A11: k > dim(p);
take {};
thus thesis by A11;
end;
end;
uniqueness
proof
let X,Y be finite set such that
A12: k < -1 implies X = {} and
A13: k = -1 implies X = {{}} and
A14: (-1 < k & k < dim(p)) implies
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence
st len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
p = [F,I] &
X = rng (F.(k+1)) and
A15: k = dim(p) implies X = {p} and
A16: k > dim(p) implies X = {} and
A17: k < -1 implies Y = {} and
A18: k = -1 implies Y = {{}} and
A19: (-1 < k & k < dim(p)) implies
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence
st len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
p = [F,I] &
Y = rng (F.(k+1)) and
A20: k = dim(p) implies Y = {p} and
A21: k > dim(p) implies Y = {};
per cases by XXREAL_0:1;
suppose k < -1;
hence thesis by A12,A17;
end;
suppose k = -1;
hence thesis by A13,A18;
end;
suppose A22: -1 < k & k < dim(p);
consider dX being Nat,
FX being FinSequence-yielding FinSequence,
IX being Function-yielding FinSequence such that
len FX = dX and
len IX = dX - 1 and
for n being Nat
st 1 <= n & n < dX
holds IX.n is incidence-matrix of rng (FX.n),rng (FX.(n+1)) and
for n being Nat
st 1 <= n & n <= dX
holds FX.n is non empty & FX.n is one-to-one and
A23: p = [FX,IX] and
A24: X = rng (FX.(k+1)) by A14,A22;
consider dY being Nat,
FY being FinSequence-yielding FinSequence,
IY being Function-yielding FinSequence such that
len FY = dY and
len IY = dY - 1 and
for n being Nat
st 1 <= n & n < dY
holds IY.n is incidence-matrix of rng (FY.n),rng (FY.(n+1)) and
for n being Nat
st 1 <= n & n <= dY
holds FY.n is non empty & FY.n is one-to-one and
A25: p = [FY,IY] and
A26: Y = rng (FY.(k+1)) by A19,A22;
thus thesis by A23,A24,A25,A26,ZFMISC_1:33;
end;
suppose k = dim(p);
hence thesis by A15,A20;
end;
suppose k > dim(p);
hence thesis by A16,A21;
end;
end;
end;
theorem Th25:
-1 < k & k < dim(p)
implies k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim(p)
proof
assume A1: -1 < k;
assume A2: k < dim(p);
A3: -1 + 1 = 0;
A4: 0 < k + 1 by A1,A3,XREAL_1:8;
reconsider n = k + 1 as Element of NAT by A4,INT_1:16;
A5: n is Nat;
0 + 1 = 1;
hence thesis by A2,A4,A5,INT_1:20;
end;
theorem Th26:
k-polytopes(p) is non empty iff (-1 <= k & k <= dim(p))
proof
set X = k-polytopes(p);
thus X is non empty implies -1 <= k & k <= dim(p) by Def3;
thus -1 <= k & k <= dim(p) implies k-polytopes(p) is non empty
proof
assume A1: -1 <= k;
assume A2: k <= dim(p);
per cases by A1,A2,XXREAL_0:1;
suppose k = -1;
hence thesis by Def3;
end;
suppose A3: -1 < k & k < dim(p);
consider F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence such that
A4: len I = len F - 1 and
A5: for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
A6: for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one and
A7: p = [F,I] and
A8: k-polytopes(p) = rng (F.(k+1)) by A3,Def3;
set n = k + 1;
A9: 1 <= n by A3,Th25;
A10: n <= dim(p) by A3,Th25;
A11: len F = dim(p) by A4,A5,A6,A7,Def2;
reconsider n as Element of NAT by A9,INT_1:16;
reconsider n as Nat;
F.n is non empty & F.n is one-to-one by A6,A9,A10,A11;
hence thesis by A8,RELAT_1:64;
end;
suppose k = dim(p);
then k-polytopes(p) = {p} by Def3;
hence thesis;
end;
end;
end;
theorem Th27:
k < dim(p) implies k - 1 < dim(p)
proof
assume A1: k < dim(p);
k - 1 < k by XREAL_1:148;
hence thesis by A1,XXREAL_0:2;
end;
:: As we defined the set of k-polytopes for all integers k, we define
:: the an incidence matrix, eta(p,k), for any integer k. Naturally,
:: for almost all k, this is the empty matrix (empty function). The
:: two cases in which we extend the data already given by the
:: polyhedron itself is for k = 0 and k = dim(p). For the latter, we
:: declare that the empty set (the unique -1-dimensional polytope) is
:: incident to all 0-polytopes. For the latter, we declare that every
:: (dim(p)-1)-polytope is incidence to p, the unique dim(p)-polytope
:: of p.
definition
let p be polyhedron,
k be Integer;
func
eta(p,k) -> incidence-matrix of (k-1)-polytopes(p),k-polytopes(p)
means :Def4:
(k < 0 implies it = {}) &
(k = 0 implies it = [:{{}},0-polytopes(p):] --> 1.Z_2) &
(0 < k & k < dim(p) implies
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence
st len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
p = [F,I] &
it = I.k) &
(k = dim(p) implies
it = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1.Z_2) &
(k > dim(p) implies it = {});
existence
proof
per cases by XXREAL_0:1;
suppose A1: k < 0;
A2: (k-1)-polytopes(p) = {}
proof
k - 1 < 0 - 1 by A1,XREAL_1:11;
hence thesis by Th26;
end;
A3: [:(k-1)-polytopes(p),k-polytopes(p):] = {} by A2,ZFMISC_1:113;
set f = {};
reconsider f as Function;
reconsider f as
Function of [:(k-1)-polytopes(p),k-polytopes(p):],{0.Z_2,1.Z_2}
by A3,FUNCT_2:55,RELAT_1:60;
reconsider f as
Element of Funcs([:(k-1)-polytopes(p),k-polytopes(p):],{0.Z_2,1.Z_2})
by FUNCT_2:11;
take f;
thus thesis by A1;
end;
suppose A4: k > dim(p);
A5: k-polytopes(p) = {} by A4,Th26;
A6: [:(k-1)-polytopes(p),k-polytopes(p):] = {} by A5,ZFMISC_1:113;
set f = {};
reconsider f as Function;
reconsider f as
Function of [:(k-1)-polytopes(p),k-polytopes(p):],{0.Z_2,1.Z_2}
by A6,FUNCT_2:55,RELAT_1:60;
reconsider f as
Element of Funcs([:(k-1)-polytopes(p),k-polytopes(p):],{0.Z_2,1.Z_2})
by FUNCT_2:11;
take f;
thus thesis by A4;
end;
suppose A7: 0 < k & k < dim(p);
consider F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence such that
A8: len I = len F - 1 and
A9: for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
A10: for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one and
A11: p = [F,I] by Def1;
A12: 0 + 1 = 1;
A13: 1 <= k by A7,A12,INT_1:20;
A14: 1 - 1 = 0;
A15: -1 < k - 1 & k - 1 < dim(p) by A7,A13,A14,Th27,XREAL_1:11;
A16: (k-1)-polytopes(p) = rng (F.((k-1)+1))
by A8,A9,A10,A11,A15,Def3;
A17: k-polytopes(p) = rng (F.(k+1)) by A7,A8,A9,A10,A11,Def3;
reconsider k' = k as Nat by A13,Th3;
len F = dim(p) by A8,A9,A10,A11,Def2;
then reconsider Ik = I.k' as incidence-matrix of (k-1)-polytopes(p),
k-polytopes(p)
by A7,A9,A13,A16,A17;
take Ik;
thus thesis by A7,A8,A9,A10,A11;
end;
suppose A18: k = 0;
per cases;
suppose A19: k = dim(p);
A20: (k-1)-polytopes(p) = {{}} by A18,Def3;
set f = [:{{}},{p}:] --> 1.Z_2;
reconsider f as incidence-matrix of {{}},{p} by Th24;
reconsider f as incidence-matrix of (k-1)-polytopes(p),
k-polytopes(p) by A19,A20,Def3;
take f;
thus thesis by A18,A19,Def3;
end;
suppose A21: k <> dim(p);
set f = [:{{}},0-polytopes(p):] --> 1.Z_2;
reconsider f as incidence-matrix of {{}},0-polytopes(p) by Th24;
reconsider f as incidence-matrix of (k-1)-polytopes(p),
k-polytopes(p) by A18,Def3;
take f;
thus thesis by A18,A21;
end;
end;
suppose A22: k = dim(p);
per cases;
suppose A23: k = 0;
A24: (k-1)-polytopes(p) = {{}} by A23,Def3;
set f = [:{{}},{p}:] --> 1.Z_2;
reconsider f as incidence-matrix of {{}},{p} by Th24;
reconsider f as incidence-matrix of (k-1)-polytopes(p),
k-polytopes(p) by A22,A24,Def3;
take f;
thus thesis by A22,A23,Def3;
end;
suppose A25: k <> 0;
set f = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1.Z_2;
reconsider f as incidence-matrix of (dim(p) - 1)-polytopes(p),{p}
by Th24;
reconsider f as incidence-matrix of (k-1)-polytopes(p),
k-polytopes(p) by A22,Def3;
take f;
thus thesis by A22,A25;
end;
end;
end;
uniqueness
proof
let s,t be incidence-matrix of (k-1)-polytopes(p),k-polytopes(p) such that
A26: (k < 0 implies s = {}) and
A27: (k = 0 implies s = [:{{}},0-polytopes(p):] --> 1.Z_2) and
A28: (0 < k & k < dim(p) implies
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence
st len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
p = [F,I] &
s = I.k) and
A29: (k = dim(p) implies
s = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1.Z_2) and
A30: (k > dim(p) implies s = {}) and
A31: (k < 0 implies t = {}) and
A32: (k = 0 implies t = [:{{}},0-polytopes(p):] --> 1.Z_2) and
A33: (0 < k & k < dim(p) implies
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence
st len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
p = [F,I] &
t = I.k) and
A34: (k = dim(p) implies
t = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1.Z_2) and
A35: (k > dim(p) implies t = {});
per cases by XXREAL_0:1;
suppose k < 0;
hence thesis by A26,A31;
end;
suppose k = 0;
hence thesis by A27,A32;
end;
suppose A36: 0 < k & k < dim(p);
consider ds being Nat,
Fs being FinSequence-yielding FinSequence,
Is being Function-yielding FinSequence such that
len Fs = ds and
len Is = ds - 1 and
for n being Nat
st 1 <= n & n < ds
holds Is.n is incidence-matrix of rng (Fs.n),rng (Fs.(n+1)) and
for n being Nat
st 1 <= n & n <= ds
holds Fs.n is non empty & Fs.n is one-to-one and
A37: p = [Fs,Is] and
A38: s = Is.k by A28,A36;
consider dt being Nat,
Ft being FinSequence-yielding FinSequence,
It being Function-yielding FinSequence such that
len Ft = dt and
len It = dt - 1 and
for n being Nat
st 1 <= n & n < dt
holds It.n is incidence-matrix of rng (Ft.n),rng (Ft.(n+1)) and
for n being Nat
st 1 <= n & n <= dt
holds Ft.n is non empty & Ft.n is one-to-one and
A39: p = [Ft,It] and
A40: t = It.k by A33,A36;
thus thesis by A37,A38,A39,A40,ZFMISC_1:33;
end;
suppose k = dim(p);
hence thesis by A29,A34;
end;
suppose k > dim(p);
hence thesis by A30,A35;
end;
end;
end;
definition
let p be polyhedron,
k be Integer;
func
k-polytope-seq(p) -> FinSequence
means :Def5:
(k < -1 implies it = <*>{}) &
(k = -1 implies it = <*{}*>) &
(-1 < k & k < dim(p) implies
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence
st len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
p = [F,I] &
it = F.(k+1)) &
(k = dim(p) implies it = <*p*>) &
(k > dim(p) implies it = <*>{});
existence
proof
per cases by XXREAL_0:1;
suppose A1: k < -1;
take <*>{};
thus thesis by A1;
end;
suppose A2: k = -1;
take <*{}*>;
thus thesis by A2;
end;
suppose A3: -1 < k & k < dim(p);
consider F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence such that
A4: len I = len F - 1 and
A5: for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
A6: for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one and
A7: p = [F,I] by Def1;
take F.(k+1);
thus thesis by A3,A4,A5,A6,A7;
end;
suppose A8: k = dim(p);
take <*p*>;
thus thesis by A8;
end;
suppose A9: k > dim(p);
take <*>{};
thus thesis by A9;
end;
end;
uniqueness
proof
let s,t be FinSequence such that
A10: (k < -1 implies s = <*>{}) and
A11: (k = -1 implies s = <*{}*>) and
A12: (-1 < k & k < dim(p) implies
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence
st len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
p = [F,I] &
s = F.(k+1)) and
A13: (k = dim(p) implies s = <*p*>) and
A14: (k > dim(p) implies s = <*>{}) and
A15: (k < -1 implies t = <*>{}) and
A16: (k = -1 implies t = <*{}*>) and
A17: (-1 < k & k < dim(p) implies
ex F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence
st len I = len F - 1 &
(for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1))) &
(for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one) &
p = [F,I] &
t = F.(k+1)) and
A18: (k = dim(p) implies t = <*p*>) and
A19: (k > dim(p) implies t = <*>{});
per cases by XXREAL_0:1;
suppose k < -1;
hence thesis by A10,A15;
end;
suppose k = -1;
hence thesis by A11,A16;
end;
suppose A20: -1 < k & k < dim(p);
consider ds being Nat,
Fs being FinSequence-yielding FinSequence,
Is being Function-yielding FinSequence such that
len Fs = ds and
len Is = ds - 1 and
for n being Nat
st 1 <= n & n < ds
holds Is.n is incidence-matrix of rng (Fs.n),rng (Fs.(n+1)) and
for n being Nat
st 1 <= n & n <= ds
holds Fs.n is non empty & Fs.n is one-to-one and
A21: p = [Fs,Is] and
A22: s = Fs.(k+1) by A12,A20;
consider dt being Nat,
Ft being FinSequence-yielding FinSequence,
It being Function-yielding FinSequence such that
len Ft = dt and
len It = dt - 1 and
for n being Nat
st 1 <= n & n < dt
holds It.n is incidence-matrix of rng (Ft.n),rng (Ft.(n+1)) and
for n being Nat
st 1 <= n & n <= dt
holds Ft.n is non empty & Ft.n is one-to-one and
A23: p = [Ft,It] and
A24: t = Ft.(k+1) by A17,A20;
thus thesis by A21,A22,A23,A24,ZFMISC_1:33;
end;
suppose k = dim(p);
hence thesis by A13,A18;
end;
suppose k > dim(p);
hence thesis by A14,A19;
end;
end;
end;
definition
let p be polyhedron,
k be Integer;
func
num-polytopes(p,k) -> Element of NAT
equals
card(k-polytopes(p));
coherence;
end;
:: It will be convenient to use these in the cases of Euler's
:: polyhedron formula that interest us.
definition
let p be polyhedron;
func
num-vertices(p) -> Element of NAT
equals
num-polytopes(p,0);
correctness;
func
num-edges(p) -> Element of NAT
equals
num-polytopes(p,1);
correctness;
func
num-faces(p) -> Element of NAT
equals
num-polytopes(p,2);
correctness;
end;
theorem Th28:
dom (k-polytope-seq(p)) = Seg (num-polytopes(p,k))
proof
consider F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence such that
A1: len I = len F - 1 and
A2: for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
A3: for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one and
A4: p = [F,I] by Def1;
per cases;
suppose A5: k < -1;
A6: k-polytope-seq(p) = <*>{} by A5,Def5;
k-polytopes(p) = {} by A5,Def3;
hence thesis by A6,FINSEQ_1:def 3;
end;
suppose A7: -1 <= k & k <= dim(p);
per cases by A7,XXREAL_0:1;
suppose A8: k = -1;
A9: k-polytopes(p) = {{}} by A8,Def3;
A10: k-polytope-seq(p) = <*{}*> by A8,Def5;
A11: num-polytopes(p,k) = 1 by A9,CARD_2:60;
len (k-polytope-seq(p)) = 1 by A10,FINSEQ_1:56;
hence thesis by A11,FINSEQ_1:def 3;
end;
suppose A12: -1 < k & k < dim(p);
A13: len F = dim(p) by A1,A2,A3,A4,Def2;
A14: k-polytope-seq(p) = F.(k+1) by A1,A2,A3,A4,A12,Def5;
A15: k-polytopes(p) = rng (F.(k+1)) by A1,A2,A3,A4,A12,Def3;
set n = k + 1;
reconsider n as Nat by A12,Th25;
reconsider Fn = F.n as FinSequence;
A16: 1 <= n & n <= dim(p) by A12,Th25;
A17: Fn is one-to-one by A3,A13,A16;
A18: num-polytopes(p,k) = card (dom Fn) by A15,A17,Th2;
len Fn = num-polytopes(p,k) by A18,PRE_CIRC:21;
hence thesis by A14,FINSEQ_1:def 3;
end;
suppose A19: k = dim(p);
A20: k-polytopes(p) = {p} by A19,Def3;
A21: k-polytope-seq(p) = <*p*> by A19,Def5;
A22: num-polytopes(p,k) = 1 by A20,CARD_2:60;
len (k-polytope-seq(p)) = 1 by A21,FINSEQ_1:56;
hence thesis by A22,FINSEQ_1:def 3;
end;
end;
suppose A23: k > dim(p);
A24: k-polytope-seq(p) = <*>{} by A23,Def5;
k-polytopes(p) = {} by A23,Def3;
hence thesis by A24,FINSEQ_1:def 3;
end;
end;
theorem Th29:
len (k-polytope-seq(p)) = num-polytopes(p,k)
proof
dom (k-polytope-seq(p)) = Seg (num-polytopes(p,k)) by Th28;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th30:
rng (k-polytope-seq(p)) = k-polytopes(p)
proof
consider F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence such that
A1: len I = len F - 1 and
A2: for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
A3: for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one and
A4: p = [F,I] by Def1;
per cases;
suppose A5: k < -1;
k-polytopes(p) = {} by A5,Def3;
hence thesis by A5,Def5,RELAT_1:60;
end;
suppose A6: -1 <= k & k <= dim(p);
per cases by A6,XXREAL_0:1;
suppose A7: k = -1;
A8: k-polytopes(p) = {{}} by A7,Def3;
k-polytope-seq(p) = <*{}*> by A7,Def5;
hence thesis by A8,FINSEQ_1:55;
end;
suppose A9: -1 < k & k < dim(p);
k-polytopes(p) = rng (F.(k+1)) by A1,A2,A3,A4,A9,Def3;
hence thesis by A1,A2,A3,A4,A9,Def5;
end;
suppose A10: k = dim(p);
A11: k-polytopes(p) = {p} by A10,Def3;
k-polytope-seq(p) = <*p*> by A10,Def5;
hence thesis by A11,FINSEQ_1:55;
end;
end;
suppose A12: k > dim(p); then
k-polytopes(p) = {} by Def3;
hence thesis by A12,Def5,RELAT_1:60;
end;
end;
theorem Th31:
num-polytopes(p,-1) = 1
proof
reconsider minusone = -1 as Integer;
minusone-polytopes(p) = {{}} by Def3;
hence thesis by CARD_1:79;
end;
theorem Th32:
num-polytopes(p,dim(p)) = 1
proof
dim(p)-polytopes(p) = {p} by Def3;
hence thesis by CARD_1:79;
end;
:: The k-polytope sets aren't really sets: they're ordered sets
:: (finite sequences).
::
:: Since the k-polytope sets are empty for k < -1 and k > dim(p), we
:: have to put a condition on n and k for the definition to make
:: sense.
definition
let p be polyhedron,
k be Integer,
n be Nat;
assume A1: 1 <= n & n <= num-polytopes(p,k) & -1 <= k & k <= dim(p);
func
n-th-polytope(p,k) -> Element of k-polytopes(p)
equals :Def10:
(k-polytope-seq(p)).n;
coherence
proof
A2: n in Seg num-polytopes(p,k) by A1,FINSEQ_1:3;
A3: n in dom (k-polytope-seq(p)) by A2,Th28;
(k-polytope-seq(p)).n in rng (k-polytope-seq(p)) by A3,FUNCT_1:12;
hence thesis by Th30;
end;
end;
theorem Th33:
-1 <= k & k <= dim(p)
implies for x being Element of k-polytopes(p)
ex n being Nat st x = n-th-polytope(p,k)
& 1 <= n
& n <= num-polytopes(p,k)
proof
assume A1: -1 <= k & k <= dim(p);
let x be Element of k-polytopes(p);
per cases by A1,XXREAL_0:1;
suppose A2: k = -1;
A3: k-polytopes(p) = {{}} by A2,Def3;
A4: x = {} by A3,TARSKI:def 1;
reconsider n = 1 as Nat;
A5: k-polytope-seq(p) = <*{}*> by A2,Def5;
A6: (k-polytope-seq(p)).n = {} by A5,FINSEQ_1:def 8;
A7: n <= num-polytopes(p,k) by A3,CARD_1:50;
take n;
thus thesis by A1,A4,A6,A7,Def10;
end;
suppose A8: k = dim(p);
A9: k-polytopes(p) = {p} by A8,Def3;
A10: x = p by A9,TARSKI:def 1;
reconsider n = 1 as Nat;
A11: num-polytopes(p,k) = 1 by A9,CARD_1:50;
A12: k-polytope-seq(p) = <*p*> by A8,Def5;
A13: (k-polytope-seq(p)).n = p by A12,FINSEQ_1:def 8;
take n;
thus thesis by A1,A10,A11,A13,Def10;
end;
suppose A14: -1 < k & k < dim(p);
consider F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence such that
A15: len I = len F - 1 and
A16: for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
A17: for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one and
A18: p = [F,I] and
A19: k-polytopes(p) = rng (F.(k+1)) by A14,Def3;
A20: k-polytope-seq(p) = F.(k+1) by A14,A15,A16,A17,A18,Def5;
A21: num-polytopes(p,k) = len (F.(k+1)) by A20,Th29;
A22: len F = dim(p) by A15,A16,A17,A18,Def2;
A23: -1 + 1 < k + 1 by A14,XREAL_1:8;
A24: k + 1 <= dim(p) by A14,INT_1:20;
A25: 0 + 1 <= k + 1 by A23,INT_1:20;
reconsider k' = k + 1 as Element of NAT by A23,INT_1:16;
A26: F.k' is non empty by A17,A22,A24,A25;
A27: rng (F.k') is non empty by A26,RELAT_1:64;
consider m being set such that
A28: m in dom (F.k') and
A29: (F.k').m = x by A19,A27,FUNCT_1:def 5;
reconsider Fk' = F.k' as FinSequence;
A30: dom Fk' = Seg (len Fk') by FINSEQ_1:def 3;
now
consider a being Nat such that
A31: dom Fk' = Seg a by FINSEQ_1:def 2;
thus m is Element of NAT by A28,A31;
end;
then reconsider m as Element of NAT;
A32: 1 <= m & m <= len Fk' by A28,A30,FINSEQ_1:3;
take m;
thus thesis by A14,A20,A21,A29,A32,Def10;
end;
end;
theorem Th34:
k-polytope-seq(p) is one-to-one
proof
set s = k-polytope-seq(p);
per cases by XXREAL_0:1;
suppose k < -1;
hence thesis by Def5;
end;
suppose k = -1;
hence thesis by Def5;
end;
suppose A1: -1 < k & k < dim(p);
consider F being FinSequence-yielding FinSequence,
I being Function-yielding FinSequence such that
A2: len I = len F - 1 and
A3: for n being Nat
st 1 <= n & n < len F
holds I.n is incidence-matrix of rng (F.n),rng (F.(n+1)) and
A4: for n being Nat
st 1 <= n & n <= len F
holds F.n is non empty & F.n is one-to-one and
A5: p = [F,I] and
A6: s = F.(k+1) by A1,Def5;
A7: len F = dim(p) by A2,A3,A4,A5,Def2;
A8: -1 + 1 < k + 1 by A1,XREAL_1:8;
reconsider m = k + 1 as Element of NAT by A8,INT_1:16;
A9: 0 + 1 <= m by A8,INT_1:20;
m <= dim(p) by A1,INT_1:20;
hence thesis by A4,A6,A7,A9;
end;
suppose k = dim(p);
then s = <*p*> by Def5;
hence thesis;
end;
suppose k > dim(p);
hence thesis by Def5;
end;
end;
theorem Th35:
-1 <= k & k <= dim(p)
implies for m,n being Nat
st 1 <= n & n <= num-polytopes(p,k)
& 1 <= m & m <= num-polytopes(p,k)
& n-th-polytope(p,k) = m-th-polytope(p,k)
holds m = n
proof
assume A1: -1 <= k & k <= dim(p);
let m,n be Nat such that
A2: 1 <= n and
A3: n <= num-polytopes(p,k) and
A4: 1 <= m and
A5: m <= num-polytopes(p,k) and
A6: n-th-polytope(p,k) = m-th-polytope(p,k);
set s = k-polytope-seq(p);
A7: n-th-polytope(p,k) = s.n by A1,A2,A3,Def10;
A8: m-th-polytope(p,k) = s.m by A1,A4,A5,Def10;
A9: n in Seg (num-polytopes(p,k)) by A2,A3,FINSEQ_1:3;
A10: n in dom s by A9,Th28;
A11: m in Seg (num-polytopes(p,k)) by A4,A5,FINSEQ_1:3;
A12: m in dom s by A11,Th28;
s is one-to-one by Th34;
hence thesis by A6,A7,A8,A10,A12,FUNCT_1:def 8;
end;
definition
let p be polyhedron,
k be Integer,
x be Element of (k-1)-polytopes(p),
y be Element of k-polytopes(p);
assume A1: 0 <= k & k <= dim(p);
func
incidence-value(x,y) -> Element of Z_2
equals :Def11:
eta(p,k).(x,y);
coherence
proof
set n = eta(p,k);
A2: dom n = [:(k-1)-polytopes(p),k-polytopes(p):] by FUNCT_2:169;
A3: (k-1)-polytopes(p) <> {}
proof
set m = k - 1;
A4: 0 - 1 = -1;
A5: -1 <= m by A1,A4,XREAL_1:11;
m <= dim(p) - 0 by A1,XREAL_1:15;
hence thesis by A5,Th26;
end;
A6: k-polytopes(p) <> {} by A1,Th26;
A7: [x,y] in dom n by A2,A3,A6,ZFMISC_1:106;
A8: rng n c= {0.Z_2,1.Z_2} by FUNCT_2:169;
n.[x,y] in rng n by A7,FUNCT_1:12;
hence thesis by A8,BSPACE:3,5,6;
end;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The Chain Spaces and their Subspaces. Boundary of a k-chain.
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
:: The set of subsets of the k-polytopes naturally forms a vector
:: space over the field Z_2. Addition is disjoint union, and scalar
:: multiplication is defined by the equations 1*x = x, 0*x = 0.
definition
let p be polyhedron,
k be Integer;
func
k-chain-space(p) -> finite-dimensional VectSp of Z_2
equals
bspace(k-polytopes(p));
coherence;
end;
theorem
for x being Element of k-polytopes(p)
holds (0.(k-chain-space(p)))@x = 0.Z_2 by BSPACE:14;
theorem Th37:
num-polytopes(p,k) = dim (k-chain-space(p))
proof
A1: singletons(k-polytopes(p)) is Basis of k-chain-space(p) by BSPACE:41;
set n = dim (k-chain-space(p));
n = Card (singletons(k-polytopes(p))) by A1,VECTSP_9:def 2;
hence thesis by BSPACE:42;
end;
:: A k-chain is a set of k-polytopes.
definition
let p be polyhedron,
k be Integer;
func
k-chains(p) -> non empty finite set
equals
bool (k-polytopes(p));
coherence;
end;
definition
let p be polyhedron,
k be Integer,
x be Element of (k-1)-polytopes(p),
v be Element of k-chain-space(p);
func
incidence-sequence(x,v) -> FinSequence of Z_2
means :Def14:
((k-1)-polytopes(p) is empty implies it = <*>{}) &
((k-1)-polytopes(p) is non empty implies
len it = num-polytopes(p,k)
& for n being Nat
st 1 <= n & n <= num-polytopes(p,k)
holds
it.n =
(v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,k)));
existence
proof
per cases;
suppose A1: (k-1)-polytopes(p) is empty;
set s = <*>{};
A2: rng s c= the carrier of Z_2 by XBOOLE_1:2;
reconsider s as FinSequence of Z_2 by A2,FINSEQ_1:def 4;
take s;
thus thesis by A1;
end;
suppose A3: (k-1)-polytopes(p) is non empty;
deffunc F(Nat) =
(v@($1-th-polytope(p,k)))*incidence-value(x,$1-th-polytope(p,k));
consider s being FinSequence of Z_2 such that
A4: len s = num-polytopes(p,k) and
A5: for n being Nat
st n in Seg num-polytopes(p,k)
holds s.n = F(n) from FINSEQ_2:sch 1;
A6: for n being Nat
st 1 <= n & n <= num-polytopes(p,k)
holds s.n =
(v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,k))
proof
let n be Nat such that
A7: 1 <= n and
A8: n <= num-polytopes(p,k);
A9: n in Seg num-polytopes(p,k) by A7,A8,FINSEQ_1:3;
reconsider n as Element of NAT by ORDINAL1:def 13;
thus thesis by A5,A9;
end;
take s;
thus thesis by A3,A4,A6;
end;
end;
uniqueness
proof
let s,t be FinSequence of Z_2 such that
A10: (k-1)-polytopes(p) is empty implies s = <*>{} and
A11: (k-1)-polytopes(p) is non empty implies
len(s) = num-polytopes(p,k) &
(for n being Nat
st 1 <= n & n <= num-polytopes(p,k)
holds s.n =
(v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,k))) and
A12: (k-1)-polytopes(p) is empty implies t = <*>{} and
A13: (k-1)-polytopes(p) is non empty implies
len(t) = num-polytopes(p,k) &
for n being Nat
st 1 <= n & n <= num-polytopes(p,k)
holds t.n =
(v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,k));
per cases;
suppose (k-1)-polytopes(p) is empty;
hence thesis by A10,A12;
end;
suppose A14: (k-1)-polytopes(p) is non empty;
for n being Nat
st 1 <= n & n <= len s
holds s.n = t.n
proof
let n be Nat such that
A15: 1 <= n and
A16: n <= len s;
reconsider n as Nat;
s.n = (v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,k))
by A11,A14,A15,A16;
hence thesis by A11,A13,A14,A15,A16;
end;
hence thesis by A11,A13,A14,FINSEQ_1:18;
end;
end;
end;
theorem Th38:
for c,d being Element of k-chain-space(p),
x being Element of k-polytopes(p)
holds (c+d)@x = (c@x) + (d@x)
proof
let c,d be Element of k-chain-space(p),
x be Element of k-polytopes(p);
c+d = c \+\ d by BSPACE:def 5;
hence thesis by BSPACE:15;
end;
theorem Th39:
for c,d being Element of k-chain-space(p),
x being Element of (k-1)-polytopes(p)
holds incidence-sequence(x,c+d)
= incidence-sequence(x,c) + incidence-sequence(x,d)
proof
let c,d be Element of k-chain-space(p),
x be Element of (k-1)-polytopes(p);
set n = num-polytopes(p,k);
set l = incidence-sequence(x,c+d);
set isc = incidence-sequence(x,c);
set isd = incidence-sequence(x,d);
set r = isc + isd;
per cases;
suppose A1: (k-1)-polytopes(p) is empty;
A2: isc = <*>(the carrier of Z_2) by A1,Def14;
A3: isd = <*>(the carrier of Z_2) by A1,Def14;
reconsider isc as Element of 0-tuples_on the carrier of Z_2
by A2,FINSEQ_2:114;
reconsider isd as Element of 0-tuples_on the carrier of Z_2
by A3,FINSEQ_2:114;
A4: isc + isd is Element of 0-tuples_on the carrier of Z_2;
r = <*>(the carrier of Z_2) by A4,FINSEQ_2:113;
hence thesis by A1,Def14;
end;
suppose A5: (k-1)-polytopes(p) is non empty;
A6: len(l) = n & len(r) = n
proof
A7: len isc = n by A5,Def14;
A8: len isd = n by A5,Def14;
reconsider isc as Element of n-tuples_on the carrier of Z_2
by A7,FINSEQ_2:110;
reconsider isd as Element of n-tuples_on the carrier of Z_2
by A8,FINSEQ_2:110;
reconsider s = isc + isd as Element of n-tuples_on the carrier of Z_2;
len s = n by FINSEQ_2:109;
hence thesis by A5,Def14;
end;
for n being Nat st 1 <= n & n <= len l
holds l.n = r.n
proof
let m be Nat such that
A9: 1 <= m and
A10: m <= len l;
set a = m-th-polytope(p,k);
set iva = incidence-value(x,a);
A11: len l = n by A5,Def14;
A12: l.m = ((c+d)@a)*iva by A5,A9,A10,A11,Def14;
A13: isc.m = (c@a)*iva by A5,A9,A10,A11,Def14;
A14: isd.m = (d@a)*iva by A5,A9,A10,A11,Def14;
A15: dom r = Seg n by A6,FINSEQ_1:def 3;
A16: len l = n by A5,Def14;
m in NAT by ORDINAL1:def 13;
then
A17: m in dom r by A9,A10,A15,A16;
r.m = (c@a)*iva + (d@a)*iva by A13,A14,A17,FVSUM_1:21
.= (c@a + d@a)*iva by VECTSP_1:def 12
.= l.m by A12,Th38;
hence thesis;
end;
hence thesis by A6,FINSEQ_1:18;
end;
end;
theorem Th40:
for c,d being Element of k-chain-space(p),
x being Element of (k-1)-polytopes(p)
holds Sum (incidence-sequence(x,c) + incidence-sequence(x,d))
= (Sum incidence-sequence(x,c)) + (Sum incidence-sequence(x,d))
proof
let c,d be Element of k-chain-space(p),
x be Element of (k-1)-polytopes(p);
set isc = incidence-sequence(x,c);
set isd = incidence-sequence(x,d);
per cases;
suppose A1: (k-1)-polytopes(p) is empty;
A2: isc = <*>(the carrier of Z_2) by A1,Def14;
A3: isd = <*>(the carrier of Z_2) by A1,Def14;
reconsider isc as Element of 0-tuples_on the carrier of Z_2
by A2,FINSEQ_2:114;
reconsider isd as Element of 0-tuples_on the carrier of Z_2
by A3,FINSEQ_2:114;
A4: Sum isc = 0.Z_2 by FVSUM_1:93;
A5: Sum isd = 0.Z_2 by FVSUM_1:93;
reconsider s = isc + isd as Element of 0-tuples_on the carrier of Z_2;
Sum s = 0.Z_2 by FVSUM_1:93;
hence thesis by A4,A5,RLVECT_1:def 7;
end;
suppose A6: (k-1)-polytopes(p) is non empty;
reconsider n = num-polytopes(p,k) as Element of NAT;
A7: len isc = n by A6,Def14;
A8: len isd = n by A6,Def14;
reconsider isc' = isc
as Element of n-tuples_on the carrier of Z_2 by A7,FINSEQ_2:110;
reconsider isd' = isd
as Element of n-tuples_on the carrier of Z_2 by A8,FINSEQ_2:110;
Sum (isc + isd) = Sum (isc' + isd')
.= Sum (isc) + Sum (isd) by FVSUM_1:95;
hence thesis;
end;
end;
theorem Th41:
for c,d being Element of k-chain-space(p),
x being Element of (k-1)-polytopes(p)
holds
Sum incidence-sequence(x,c+d)
= (Sum incidence-sequence(x,c)) + (Sum incidence-sequence(x,d))
proof
let c,d be Element of k-chain-space(p),
x be Element of (k-1)-polytopes(p);
Sum incidence-sequence(x,c+d)
= Sum (incidence-sequence(x,c) + incidence-sequence(x,d)) by Th39
.= (Sum incidence-sequence(x,c)) + (Sum incidence-sequence(x,d)) by Th40;
hence thesis;
end;
theorem Th42:
for c being Element of k-chain-space(p),
a being Element of Z_2,
x being Element of k-polytopes(p)
holds (a*c)@x = a*(c@x)
proof
let c be Element of k-chain-space(p),
a be Element of Z_2,
x be Element of k-polytopes(p);
per cases by BSPACE:8;
suppose A1: a = 0.Z_2;
A2: a*(c@x) = 0.Z_2 by A1,VECTSP_1:39;
a*c = 0.(k-chain-space(p)) by A1,VECTSP_1:59;
hence thesis by A2,BSPACE:14;
end;
suppose A3: a = 1.Z_2;
A4: a*(c@x) = c@x by A3,VECTSP_1:def 16;
1.Z_2 = 1_Z_2;
hence thesis by A3,A4,VECTSP_1:def 26;
end;
end;
theorem Th43:
for c being Element of k-chain-space(p),
a being Element of Z_2,
x being Element of (k-1)-polytopes(p)
holds incidence-sequence(x,a*c) = a*incidence-sequence(x,c)
proof
let c be Element of k-chain-space(p),
a be Element of Z_2,
x be Element of (k-1)-polytopes(p);
set l = incidence-sequence(x,a*c);
set isc = incidence-sequence(x,c);
set r = a*isc;
per cases;
suppose A1: (k-1)-polytopes(p) is empty;
A2: isc = <*>(the carrier of Z_2) by A1,Def14;
reconsider isc as Element of 0-tuples_on the carrier of Z_2
by A2,FINSEQ_2:114;
A3: a*isc is Element of 0-tuples_on the carrier of Z_2;
reconsider r as Element of 0-tuples_on the carrier of Z_2 by A3;
r = <*>(the carrier of Z_2) by FINSEQ_2:113;
hence thesis by A1,Def14;
end;
suppose A4: (k-1)-polytopes(p) is non empty;
set n = num-polytopes(p,k);
A5: len l = n & len r = n
proof
A6: len isc = n by A4,Def14;
reconsider isc as Element of n-tuples_on the carrier of Z_2
by A6,FINSEQ_2:110;
set r = a*isc;
reconsider r as Element of n-tuples_on the carrier of Z_2;
len r = n by FINSEQ_2:109;
hence thesis by A4,Def14;
end;
for m being Nat st 1 <= m & m <= len l
holds l.m = r.m
proof
let m be Nat such that
A7: 1 <= m and
A8: m <= len l;
set s = m-th-polytope(p,k);
set ivs = incidence-value(x,s);
A9: len l = n by A4,Def14;
A10: l.m = ((a*c)@s)*ivs by A4,A7,A8,A9,Def14;
A11: isc.m = (c@s)*ivs by A4,A7,A8,A9,Def14;
A12: dom r = Seg n by A5,FINSEQ_1:def 3;
A13: len l = n by A4,Def14;
m in NAT by ORDINAL1:def 13;
then
A14: m in Seg n by A7,A8,A13;
r.m = a*((c@s)*ivs) by A11,A12,A14,FVSUM_1:62
.= (a*(c@s))*ivs by GROUP_1:def 4
.= l.m by A10,Th42;
hence thesis;
end;
hence thesis by A5,FINSEQ_1:18;
end;
end;
theorem Th44:
for c,d being Element of k-chain-space(p)
holds c = d iff for x being Element of k-polytopes(p) holds c@x = d@x
proof
let c,d be Element of k-chain-space(p);
thus c = d implies for x being Element of k-polytopes(p) holds c@x = d@x;
thus (for x being Element of k-polytopes(p) holds c@x = d@x) implies c = d
proof
assume A1: for x being Element of k-polytopes(p) holds c@x = d@x;
thus c c= d
proof
let x be set such that A2: x in c;
reconsider c as Subset of k-polytopes(p);
reconsider x as Element of k-polytopes(p) by A2;
c@x = 1.Z_2 by A2,BSPACE:def 3;
then d@x = 1.Z_2 by A1;
hence thesis by BSPACE:9;
end;
thus d c= c
proof
let x be set such that A3: x in d;
reconsider d as Subset of k-polytopes(p);
reconsider x as Element of k-polytopes(p) by A3;
d@x = 1.Z_2 by A3,BSPACE:def 3;
then c@x = 1.Z_2 by A1;
hence thesis by BSPACE:9;
end;
end;
end;
theorem Th45:
for c,d being Element of k-chain-space(p)
holds c = d
iff
for x being Element of k-polytopes(p) holds x in c iff x in d
proof
let c,d be Element of k-chain-space(p);
thus c = d
implies for x being Element of k-polytopes(p) holds x in c iff x in d;
thus (for x being Element of k-polytopes(p) holds x in c iff x in d)
implies c = d
proof
assume A1: for x being Element of k-polytopes(p) holds x in c iff x in d;
assume A2: c <> d;
consider x being Element of k-polytopes(p) such that
A3: c@x <> d@x by A2,Th44;
not (x in c iff x in d) by A3,BSPACE:13;
hence thesis by A1;
end;
end;
scheme
ChainEx { p() -> polyhedron,
k() -> Integer,
P[Element of k()-polytopes(p())] } :
ex c being Subset of k()-polytopes(p())
st for x being Element of k()-polytopes(p())
holds x in c iff (P[x] & x in k()-polytopes(p()))
proof
set c =
{ x where x is Element of k()-polytopes(p()) :
P[x] & x in k()-polytopes(p()) };
c c= k()-polytopes(p())
proof
let x be set such that A1: x in c;
consider y being Element of k()-polytopes(p()) such that
A2: x = y and
P[y] and
A3: y in k()-polytopes(p()) by A1;
thus thesis by A2,A3;
end;
then reconsider c as Subset of k()-polytopes(p());
A4: for x being Element of k()-polytopes(p()) holds
x in c iff (P[x] & x in k()-polytopes(p()))
proof
let x be Element of k()-polytopes(p());
thus x in c implies (P[x] & x in k()-polytopes(p()))
proof
assume x in c;
then consider y being Element of k()-polytopes(p()) such that
A5: y = x and
A6: P[y] and
A7: y in k()-polytopes(p());
thus thesis by A5,A6,A7;
end;
thus (P[x] & x in k()-polytopes(p())) implies x in c;
end;
take c;
thus thesis by A4;
end;
:: The boundary of a k-chain v is the (k-1)-chain consisting of the
:: (k-1)-polytopes that are on the "perimeter" of v. Being on the
:: perimeter amounts the sum of the incidence sequence being non-zero,
:: i.e., being equal to 1.
definition
let p be polyhedron,
k be Integer,
v be Element of k-chain-space(p);
func
Boundary(v) -> Element of (k-1)-chain-space(p)
means :Def15:
((k-1)-polytopes(p) is empty implies it = 0.((k-1)-chain-space(p))) &
((k-1)-polytopes(p) is non empty implies
for x being Element of (k-1)-polytopes(p)
holds x in it iff Sum incidence-sequence(x,v) = 1.Z_2);
existence
proof
per cases;
suppose A1: (k-1)-polytopes(p) is empty;
take 0.((k-1)-chain-space(p));
thus thesis by A1;
end;
suppose A2: (k-1)-polytopes(p) is non empty;
defpred Q[Element of (k-1)-polytopes(p)] means
Sum incidence-sequence($1,v) = 1.Z_2;
consider c being Subset of (k-1)-polytopes(p) such that
A3: for x being Element of (k-1)-polytopes(p)
holds x in c iff (Q[x] & x in (k-1)-polytopes(p)) from ChainEx;
reconsider c as Element of (k-1)-chain-space(p);
take c;
thus thesis by A2,A3;
end;
end;
uniqueness
proof
let c,d be Element of (k-1)-chain-space(p) such that
A4: (k-1)-polytopes(p) is empty implies c = 0.((k-1)-chain-space(p)) and
A5: (k-1)-polytopes(p) is non empty implies
for x being Element of (k-1)-polytopes(p)
holds x in c iff Sum incidence-sequence(x,v) = 1.Z_2 and
A6: (k-1)-polytopes(p) is empty implies d = 0.((k-1)-chain-space(p)) and
A7: (k-1)-polytopes(p) is non empty implies
for x being Element of (k-1)-polytopes(p)
holds x in d iff Sum incidence-sequence(x,v) = 1.Z_2;
per cases;
suppose (k-1)-polytopes(p) is empty;
hence thesis by A4,A6;
end;
suppose A8: (k-1)-polytopes(p) is non empty;
for x being Element of (k-1)-polytopes(p)
holds x in c iff x in d
proof
let x be Element of (k-1)-polytopes(p);
thus x in c implies x in d
proof
assume x in c;
then Sum incidence-sequence(x,v) = 1.Z_2 by A5;
hence thesis by A7,A8;
end;
thus x in d implies x in c
proof
assume x in d;
then Sum incidence-sequence(x,v) = 1.Z_2 by A7;
hence thesis by A5,A8;
end;
end;
hence thesis by Th45;
end;
end;
end;
theorem Th46:
for c being Element of k-chain-space(p),
x being Element of (k-1)-polytopes(p)
holds (Boundary(c))@x = Sum incidence-sequence(x,c)
proof
let c be Element of k-chain-space(p),
x be Element of (k-1)-polytopes(p);
set b = Boundary(c);
per cases;
suppose A1: (k-1)-polytopes(p) is empty;
A2: Boundary(c) = 0.((k-1)-chain-space(p)) by A1,Def15;
set iscx = incidence-sequence(x,c);
A3: iscx = <*>(the carrier of Z_2) by A1,Def14;
Sum iscx = 0.Z_2 by A3,RLVECT_1:60;
hence thesis by A2,BSPACE:14;
end;
suppose A4: (k-1)-polytopes(p) is non empty;
A5: x in b iff Sum incidence-sequence(x,c) = 1.Z_2 by A4,Def15;
per cases;
suppose x in b;
hence thesis by A5,BSPACE:def 3;
end;
suppose A6: not x in b;
A7: Sum incidence-sequence(x,c) <> 1.Z_2 by A4,A6,Def15;
Sum incidence-sequence(x,c) = 0.Z_2 by A7,BSPACE:8;
hence thesis by A6,BSPACE:def 3;
end;
end;
end;
:: Every dimension k has its own boundary operation.
definition
let p be polyhedron,
k be Integer;
func
k-boundary(p) -> Function of k-chain-space(p),(k-1)-chain-space(p)
means :Def16:
for c being Element of k-chain-space(p) holds it.c = Boundary(c);
existence
proof
defpred Q[set,set] means
ex c being Element of k-chain-space(p) st $1 = c & $2 = Boundary(c);
A1: for x being set st x in k-chains(p) holds
ex y being set st y in (k-1)-chains(p) & Q[x,y]
proof
let x be set such that
A2: x in k-chains(p);
reconsider x as Element of k-chain-space(p) by A2;
set b = Boundary(x);
take b;
thus thesis;
end;
consider f being Function of k-chains(p),
(k-1)-chains(p) such that
A3: for x being set st x in k-chains(p) holds Q[x,f.x]
from FUNCT_2:sch 1(A1);
reconsider f as Function of k-chain-space(p),(k-1)-chain-space(p);
A4: for c being Element of k-chain-space(p) holds f.c = Boundary(c)
proof
let c be Element of k-chain-space(p);
Q[c,f.c] by A3;
hence thesis;
end;
take f;
thus thesis by A4;
end;
uniqueness
proof
let f,g be Function of k-chain-space(p),(k-1)-chain-space(p) such that
A5: for c being Element of k-chain-space(p) holds f.c = Boundary(c) and
A6: for c being Element of k-chain-space(p) holds g.c = Boundary(c);
A7: dom f = [#](k-chain-space(p)) by FUNCT_2:def 1;
A8: dom f = dom g by A7,FUNCT_2:def 1;
for x being set st x in dom f holds f.x = g.x
proof
let x be set such that A9: x in dom f;
reconsider x as Element of k-chain-space(p) by A9;
f.x = Boundary(x) by A5;
hence thesis by A6;
end;
hence thesis by A8,FUNCT_1:9;
end;
end;
theorem Th47:
for c,d being Element of k-chain-space(p)
holds Boundary(c+d) = Boundary(c) + Boundary(d)
proof
let c,d be Element of k-chain-space(p);
set bc = Boundary(c);
set bd = Boundary(d);
set s = c+d;
set l = Boundary(s);
set r = bc+bd;
for x being Element of (k-1)-polytopes(p) holds l@x = r@x
proof
let x be Element of (k-1)-polytopes(p);
A1: l@x = Sum incidence-sequence(x,s) by Th46;
set a = bc@x;
set b = bd@x;
A2: r@x = a+b by Th38;
A3: a = Sum incidence-sequence(x,c) by Th46;
b = Sum incidence-sequence(x,d) by Th46;
hence thesis by A1,A2,A3,Th41;
end;
hence thesis by Th44;
end;
theorem Th48:
for a being Element of Z_2,
c being Element of k-chain-space(p)
holds Boundary(a*c) = a*(Boundary(c))
proof
let a be Element of Z_2,
c be Element of k-chain-space(p);
set lsm = a*c;
set l = Boundary(lsm);
set rb = Boundary(c);
set r = a*rb;
for x being Element of (k-1)-polytopes(p) holds l@x = r@x
proof
let x be Element of (k-1)-polytopes(p);
A1: l@x = Sum incidence-sequence(x,lsm) by Th46;
A2: rb@x = Sum incidence-sequence(x,c) by Th46;
set b = rb@x;
A3: r@x = a*b by Th42;
incidence-sequence(x,lsm) = a*incidence-sequence(x,c) by Th43;
hence thesis by A1,A2,A3,FVSUM_1:92;
end;
hence thesis by Th44;
end;
:: As defined, the k-boundary operator gives rise to a linear
:: transformation.
theorem Th49:
k-boundary(p) is
linear-transformation of k-chain-space(p),(k-1)-chain-space(p)
proof
set V = k-chain-space(p);
set b = k-boundary(p);
A1: for x,y being Element of V holds b.(x+y) = (b.x) + (b.y)
proof
let x,y be Element of V;
b.(x+y) = Boundary(x+y) by Def16
.= Boundary(x) + Boundary(y) by Th47
.= (b.x) + Boundary(y) by Def16
.= (b.x) + (b.y) by Def16;
hence thesis;
end;
for a being Element of Z_2,
x being Element of V
holds b.(a*x) = a*(b.x)
proof
let a be Element of Z_2,
x be Element of V;
b.(a*x) = Boundary(a*x) by Def16
.= a*(Boundary(x)) by Th48
.= a*(b.x) by Def16;
hence thesis;
end;
hence thesis by A1,MOD_2:def 5;
end;
definition
let p be polyhedron,
k be Integer;
redefine func
k-boundary(p) -> linear-transformation of k-chain-space(p),
(k-1)-chain-space(p);
coherence by Th49;
end;
:: The term "circuit" is used in Lakatos. (A more customary term is
:: "cycle".)
definition
let p be polyhedron,
k be Integer;
func
k-circuit-space(p) -> Subspace of k-chain-space(p)
equals
ker (k-boundary(p));
coherence;
end;
definition
let p be polyhedron,
k be Integer;
func
k-circuits(p) -> non empty Subset of k-chains(p)
equals
[#](k-circuit-space(p));
coherence by VECTSP_4:def 2;
end;
definition
let p be polyhedron,
k be Integer;
func
k-bounding-chain-space(p) -> Subspace of k-chain-space(p)
equals
im ((k+1)-boundary(p));
coherence;
end;
definition
let p be polyhedron,
k be Integer;
func
k-bounding-chains(p) -> non empty Subset of k-chains(p)
equals
[#](k-bounding-chain-space(p));
coherence by VECTSP_4:def 2;
end;
definition
let p be polyhedron,
k be Integer;
func
k-bounding-circuit-space(p) -> Subspace of k-chain-space(p)
equals
(k-bounding-chain-space(p)) /\ (k-circuit-space(p));
coherence;
end;
definition
let p be polyhedron,
k be Integer;
func
k-bounding-circuits(p) -> non empty Subset of k-chains(p)
equals
[#](k-bounding-circuit-space(p));
coherence by VECTSP_4:def 2;
end;
theorem
dim (k-chain-space(p))
= rank (k-boundary(p)) + nullity (k-boundary(p)) by RANKNULL:44;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: Simply Connected and Eulerian Polyhedra
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
:: The property of being simply connected is that circuits are
:: bounding, and vice versa (any bounding chain is a circuit).
definition
let p be polyhedron;
attr
p is simply-connected
means :Def23:
for k being Integer holds k-circuits(p) = k-bounding-chains(p);
end;
theorem Th51:
p is simply-connected
iff for n being Integer
holds n-circuit-space(p)
= n-bounding-chain-space(p)
proof
defpred Q[polyhedron] means
for n being Integer
holds n-circuit-space($1)
= n-bounding-chain-space($1);
thus p is simply-connected implies Q[p]
proof
assume A1: p is simply-connected;
let n be Integer;
n-circuits(p) = n-bounding-chains(p) by A1,Def23;
hence thesis by VECTSP_4:37;
end;
thus Q[p] implies p is simply-connected
proof
assume A2: Q[p];
let n be Integer;
thus thesis by A2;
end;
end;
definition
let p be polyhedron;
func
alternating-f-vector(p) -> FinSequence of INT
means :Def24:
len(it) = dim(p) + 2
& (for k being Nat st 1 <= k & k <= dim(p) + 2
holds it.k = ((-1)|^k)*num-polytopes(p,k-2));
existence
proof
deffunc F(Nat) = ((-1)|^$1)*num-polytopes(p,$1-2);
consider s being FinSequence of INT such that
A1: len s = dim(p) + 2 and
A2: for j being Nat
st j in Seg (dim(p) + 2)
holds s.j = F(j) from FINSEQ_2:sch 1;
A3: for j being Nat
st 1 <= j & j <= dim(p) + 2
holds s.j = ((-1)|^j)*num-polytopes(p,j-2)
proof
let j be Nat such that
A4: 1 <= j and
A5: j <= dim(p) + 2;
A6: j in Seg (dim(p) + 2) by A4,A5,FINSEQ_1:3;
reconsider j as Element of NAT by ORDINAL1:def 13;
thus thesis by A2,A6;
end;
take s;
thus thesis by A1,A3;
end;
uniqueness
proof
let s,t be FinSequence of INT such that
A7: len(s) = dim(p) + 2 and
A8: for k being Nat
st 1 <= k & k <= dim(p) + 2
holds s.k = ((-1)|^k)*num-polytopes(p,k-2) and
A9: len(t) = dim(p) + 2 and
A10: for k being Nat
st 1 <= k & k <= dim(p) + 2
holds t.k = ((-1)|^k)*num-polytopes(p,k-2);
for k being Nat st 1 <= k & k <= len s
holds s.k = t.k
proof
let k be Nat such that
A11: 1 <= k and
A12: k <= len s;
reconsider k as Nat;
s.k = ((-1)|^k)*num-polytopes(p,k-2) by A7,A8,A11,A12;
hence thesis by A7,A10,A11,A12;
end;
hence thesis by A7,A9,FINSEQ_1:18;
end;
end;
definition
let p be polyhedron;
func
alternating-proper-f-vector(p) -> FinSequence of INT
means :Def25:
len(it) = dim(p)
& (for k being Nat st 1 <= k & k <= dim(p)
holds it.k = ((-1)|^(k+1))*num-polytopes(p,k-1));
existence
proof
deffunc F(Nat) =
((-1)|^($1+1))*num-polytopes(p,$1-1);
consider s being FinSequence of INT such that
A1: len s = dim(p) and
A2: for j being Nat
st j in Seg dim(p)
holds s.j = F(j) from FINSEQ_2:sch 1;
A3: for j being Nat
st 1 <= j & j <= dim(p)
holds s.j = ((-1)|^(j+1))*num-polytopes(p,j-1)
proof
let j be Nat such that
A4: 1 <= j and
A5: j <= dim(p);
A6: j in Seg dim(p) by A4,A5,FINSEQ_1:3;
reconsider j as Element of NAT by ORDINAL1:def 13;
thus thesis by A2,A6;
end;
take s;
thus thesis by A1,A3;
end;
uniqueness
proof
let s,t be FinSequence of INT such that
A7: len(s) = dim(p) and
A8: for k being Nat
st 1 <= k & k <= dim(p)
holds s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) and
A9: len(t) = dim(p) and
A10: for k being Nat
st 1 <= k & k <= dim(p)
holds t.k = ((-1)|^(k+1))*num-polytopes(p,k-1);
for k being Nat
st 1 <= k & k <= len s
holds s.k = t.k
proof
let k be Nat such that
A11: 1 <= k and
A12: k <= len s;
reconsider k as Nat;
s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) by A7,A8,A11,A12;
hence thesis by A7,A10,A11,A12;
end;
hence thesis by A7,A9,FINSEQ_1:18;
end;
end;
definition
let p be polyhedron;
func
alternating-semi-proper-f-vector(p) -> FinSequence of INT
means :Def26:
len(it) = dim(p) + 1
& (for k being Nat st 1 <= k & k <= dim(p) + 1
holds it.k = ((-1)|^(k+1))*num-polytopes(p,k-1));
existence
proof
deffunc F(Nat) =
((-1)|^($1+1))*num-polytopes(p,$1-1);
consider s being FinSequence of INT such that
A1: len s = dim(p) + 1 and
A2: for j being Nat
st j in Seg (dim(p) + 1)
holds s.j = F(j) from FINSEQ_2:sch 1;
A3: for j being Nat
st 1 <= j & j <= dim(p) + 1
holds s.j = ((-1)|^(j+1))*num-polytopes(p,j-1)
proof
let j be Nat such that
A4: 1 <= j and
A5: j <= dim(p) + 1;
A6: j in Seg (dim(p) + 1) by A4,A5,FINSEQ_1:3;
reconsider j as Element of NAT by ORDINAL1:def 13;
thus thesis by A2,A6;
end;
take s;
thus thesis by A1,A3;
end;
uniqueness
proof
let s,t be FinSequence of INT such that
A7: len(s) = dim(p) + 1 and
A8: for k being Nat
st 1 <= k & k <= dim(p) + 1
holds s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) and
A9: len(t) = dim(p) + 1 and
A10: for k being Nat
st 1 <= k & k <= dim(p) + 1
holds t.k = ((-1)|^(k+1))*num-polytopes(p,k-1);
for k being Nat
st 1 <= k & k <= len s
holds s.k = t.k
proof
let k be Nat such that
A11: 1 <= k and
A12: k <= len s;
reconsider k as Nat;
s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) by A7,A8,A11,A12;
hence thesis by A7,A10,A11,A12;
end;
hence thesis by A7,A9,FINSEQ_1:18;
end;
end;
theorem Th52:
1 <= n & n <= len (alternating-proper-f-vector(p))
implies (alternating-proper-f-vector(p)).n
= ((-1)|^(n+1))*(dim ((n-2)-bounding-chain-space(p)))
+ ((-1)|^(n+1))*(dim ((n-1)-circuit-space(p)))
proof
set apcs = alternating-proper-f-vector(p);
assume A1: 1 <= n;
assume A2: n <= len apcs;
A3: n <= dim(p) by A2,Def25;
set a = (-1)|^(n+1);
apcs.n = a*num-polytopes(p,n-1) by A1,A3,Def25
.= a*(dim ((n-1)-chain-space(p))) by Th37
.= a*(rank ((n-1)-boundary p) + nullity ((n-1)-boundary p))
by RANKNULL:44
.= (a*dim ((n-2)-bounding-chain-space(p)))
+ (a*dim ((n-1)-circuit-space(p)));
hence thesis;
end;
:: The term "eulerian" comes from Lakatos.
definition
let p be polyhedron;
attr
p is eulerian
means :Def27:
Sum (alternating-proper-f-vector(p)) = 1 + (-1)|^(dim(p)+1);
end;
theorem Th53:
alternating-semi-proper-f-vector(p)
= alternating-proper-f-vector(p) ^ <*(-1)|^(dim(p))*>
proof
set d = dim(p);
set aspcs = alternating-semi-proper-f-vector(p);
set apcs = alternating-proper-f-vector(p);
set r = apcs ^ <*(-1)|^(dim(p))*>;
A1: len aspcs = d + 1 by Def26;
A2: len r = (len apcs) + (len <*(-1)|^(dim(p))*>) by FINSEQ_1:35
.= d + (len <*(-1)|^(dim(p))*>) by Def25
.= d + 1 by FINSEQ_1:57;
A3: len aspcs = len r by A2,Def26;
for n being Nat st 1 <= n & n <= len aspcs
holds aspcs.n = r.n
proof
let n be Nat such that
A4: 1 <= n and
A5: n <= len aspcs;
per cases by A1,A5,NAT_1:8;
suppose A6: n <= d;
A7: len apcs = d by Def25;
A8: dom apcs = Seg (len apcs) by FINSEQ_1:def 3;
n in NAT by ORDINAL1:def 13;
then
A9: n in dom apcs by A4,A6,A7,A8;
r.n = apcs.n by A9,FINSEQ_1:def 7
.= ((-1)|^(n+1))*num-polytopes(p,n-1) by A4,A6,Def25;
hence thesis by A1,A4,A5,Def26;
end;
suppose A10: n = d + 1;
A11: aspcs.n = ((-1)|^(n+1))*num-polytopes(p,n-1) by A4,A10,Def26
.= ((-1)|^(n+1))*1 by A10,Th32
.= (-1)|^(n+1);
A12: n = (len apcs) + 1 by A10,Def25;
r.n = (-1)|^d by A12,FINSEQ_1:59
.= (-1)|^(d+2) by Th14;
hence thesis by A10,A11;
end;
end;
hence thesis by A3,FINSEQ_1:18;
end;
:: Another characterization of Eulerian polyhedra
definition
let p be polyhedron;
redefine attr
p is eulerian
means :Def28:
Sum (alternating-semi-proper-f-vector(p)) = 1;
compatibility
proof
set apcs = alternating-proper-f-vector(p);
set aspcs = alternating-semi-proper-f-vector(p);
A1: aspcs = apcs ^ <*(-1)|^(dim(p))*> by Th53;
A2: Sum aspcs = (Sum apcs) + (-1)|^(dim(p)) by A1,GR_CY_1:20;
A3: p is eulerian implies Sum aspcs = 1
proof
assume A4: p is eulerian;
Sum aspcs = 1 + (-1)|^(dim(p)+1) + (-1)|^(dim(p)) by A2,A4,Def27
.= 1 + (-1)*((-1)|^(dim(p))) + (-1)|^(dim(p)) by NEWTON:11
.= 1;
hence thesis;
end;
Sum aspcs = 1 implies p is eulerian
proof
assume A5: Sum aspcs = 1;
Sum apcs = 1 + (-1)*((-1)|^(dim(p))) by A2,A5
.= 1 + (-1)|^(dim(p)+1) by NEWTON:11;
hence thesis by Def27;
end;
hence thesis by A3;
end;
end;
theorem Th54:
alternating-f-vector(p)
= <*-1*> ^ alternating-semi-proper-f-vector(p)
proof
set acs = alternating-f-vector(p);
set aspcs = alternating-semi-proper-f-vector(p);
set d = dim(p);
set r = <*-1*> ^ aspcs;
A1: len r = (len <*-1*>) + (len aspcs) by FINSEQ_1:35
.= (len <*-1*>) + (d + 1) by Def26
.= 1 + (d + 1) by FINSEQ_1:57
.= d + 2;
A2: len acs = len r by A1,Def24;
for n being Nat st 1 <= n & n <= len acs
holds acs.n = r.n
proof
let n be Nat such that
A3: 1 <= n and
A4: n <= len acs;
A5: n <= d + 2 by A4,Def24;
per cases by A3,XXREAL_0:1;
suppose A6: n = 1;
acs.n = ((-1)|^1)*num-polytopes(p,1-2) by A5,A6,Def24
.= (-1)*num-polytopes(p,-1) by NEWTON:10
.= (-1)*1 by Th31
.= -1;
hence thesis by A6,FINSEQ_1:58;
end;
suppose A7: n > 1;
A8: 1 - 1 < n - 1 by A7,XREAL_1:11;
reconsider m = n - 1 as Element of NAT by A8,INT_1:16;
A9: 0 < 0 + m by A8;
A10: 1 <= m by A9,NAT_1:19;
A11: n - 1 <= (d + 2) - 1 by A5,XREAL_1:11;
A12: m <= d + 1 by A11;
A13: r.n = aspcs.(n-1)
proof
len <*-1*> = 1 by FINSEQ_1:56;
hence thesis by A1,A5,A7,FINSEQ_1:37;
end;
aspcs.m = ((-1)|^(m+1))*num-polytopes(p,m-1) by A10,A12,Def26
.= ((-1)|^n)*(num-polytopes(p,n-2));
hence thesis by A3,A5,A13,Def24;
end;
end;
hence thesis by A2,FINSEQ_1:18;
end;
:: Yet another characterization of eulerian polyhedra
definition
let p be polyhedron;
redefine attr
p is eulerian
means :Def29:
Sum (alternating-f-vector(p)) = 0;
compatibility
proof
set acs = alternating-f-vector(p);
set aspcs = alternating-semi-proper-f-vector(p);
A1: acs = <*-1*> ^ aspcs by Th54;
A2: Sum acs = -1 + (Sum aspcs) by A1,Th21;
p is eulerian implies Sum acs = 0
proof
assume A3: p is eulerian;
Sum acs = -1 + 1 by A2,A3,Def28
.= 0;
hence thesis;
end;
hence thesis by A2,Def28;
end;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: The Extremal Chain Spaces
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
theorem Th55:
0-polytopes(p) is non empty
proof
set d = dim(p);
per cases;
suppose d = 0;
then 0-polytopes(p) = {p} by Def3;
hence thesis;
end;
suppose d > 0;
hence thesis by Th26;
end;
end;
theorem Th56:
Card [#]((-1)-chain-space(p)) = 2
proof
A1: (-1)-polytopes(p) = {{}} by Def3;
A2: Card ((-1)-polytopes(p)) = 1 by A1,CARD_1:50;
Card [#]((-1)-chain-space(p)) = exp(2,1) by A2,BSPACE:43
.= 2 by CARD_2:40;
hence thesis;
end;
theorem Th57:
[#]((-1)-chain-space(p)) = { {}, {{}} }
proof
(-1)-polytopes(p) = {{}} by Def3;
hence thesis by ZFMISC_1:30;
end;
theorem Th58:
for x being Element of k-polytopes(p),
e being Element of (k-1)-polytopes(p)
st k = 0 & e = {}
holds incidence-value(e,x) = 1.Z_2
proof
let x be Element of k-polytopes(p),
e be Element of (k-1)-polytopes(p) such that
A1: k = 0 and
A2: e = {};
A3: 0 <= k & k <= dim(p) by A1;
A4: eta(p,k) = [:{{}},0-polytopes(p):] --> 1.Z_2 by A1,Def4;
A5: {} in {{}} by TARSKI:def 1;
A6: 0-polytopes(p) is non empty by A3,Th26;
A7: [{},x] in [:{{}},0-polytopes(p):] by A1,A5,A6,ZFMISC_1:106;
incidence-value(e,x) = eta(p,k).(e,x) by A3,Def11
.= 1.Z_2 by A2,A4,A7,FUNCOP_1:13;
hence thesis;
end;
theorem Th59:
for k being Integer,
x being Element of k-polytopes(p),
v being Element of k-chain-space(p),
e being Element of (k-1)-polytopes(p),
n being Nat
st k = 0 & v = {x} & e = {} & x = n-th-polytope(p,k)
& 1 <= n & n <= num-polytopes(p,k)
holds incidence-sequence(e,v).n = 1.Z_2
proof
let k be Integer,
x be Element of k-polytopes(p),
v be Element of k-chain-space(p),
e be Element of (k-1)-polytopes(p),
n be Nat such that
A1: k = 0 and
A2: v = {x} and
A3: e = {} and
A4: x = n-th-polytope(p,k) and
A5: 1 <= n and
A6: n <= num-polytopes(p,k);
set iseq = incidence-sequence(e,v);
A7: (k-1)-polytopes(p) is non empty by A1,Def3;
A8: x in v by A2,TARSKI:def 1;
iseq.n = (v@x)*incidence-value(e,x) by A4,A5,A6,A7,Def14
.= (1.Z_2)*incidence-value(e,x) by A8,BSPACE:def 3
.= (1.Z_2)*(1.Z_2) by A1,A3,Th58
.= 1.Z_2 by VECTSP_1:def 16;
hence thesis;
end;
theorem Th60:
for k being Integer,
x being Element of k-polytopes(p),
e being Element of (k-1)-polytopes(p),
v being Element of k-chain-space(p),
m,n being Nat
st k = 0 &
v = {x} &
x = n-th-polytope(p,k) &
1 <= m &
m <= num-polytopes(p,k) &
1 <= n &
n <= num-polytopes(p,k) &
m <> n
holds incidence-sequence(e,v).m = 0.Z_2
proof
let k be Integer,
x be Element of k-polytopes(p),
e be Element of (k-1)-polytopes(p),
v be Element of k-chain-space(p),
m,n be Nat such that
A1: k = 0 and
A2: v = {x} and
A3: x = n-th-polytope(p,k) and
A4: 1 <= m and
A5: m <= num-polytopes(p,k) and
A6: 1 <= n and
A7: n <= num-polytopes(p,k) and
A8: m <> n;
set iseq = incidence-sequence(e,v);
-1 <= k & k <= dim(p) by A1;
then A9: m-th-polytope(p,k) <> x by A3,A4,A5,A6,A7,A8,Th35;
now
assume v@(m-th-polytope(p,k)) = 1.Z_2;
then m-th-polytope(p,k) in {x} by A2,BSPACE:9;
hence contradiction by A9,TARSKI:def 1;
end;
then A10: v@(m-th-polytope(p,k)) = 0.Z_2 by BSPACE:11;
A11: (k-1)-polytopes(p) is non empty by A1,Def3;
iseq.m = (0.Z_2)*(incidence-value(e,m-th-polytope(p,k)))
by A4,A5,A10,A11,Def14
.= 0.Z_2 by VECTSP_1:39;
hence thesis;
end;
theorem Th61:
for k being Integer,
x being Element of k-polytopes(p),
v being Element of k-chain-space(p),
e being Element of (k-1)-polytopes(p)
st k = 0 & v = {x} & e = {}
holds Sum incidence-sequence(e,v) = 1.Z_2
proof
let k be Integer,
x be Element of k-polytopes(p),
v be Element of k-chain-space(p),
e be Element of (k-1)-polytopes(p) such that
A1: k = 0 and
A2: v = {x} and
A3: e = {};
set iseq = incidence-sequence(e,v);
A4: -1 <= k & k <= dim(p) by A1;
consider n being Nat such that
A5: x = n-th-polytope(p,k) and
A6: 1 <= n and
A7: n <= num-polytopes(p,k) by A4,Th33;
A8: (k-1)-polytopes(p) is non empty by A1,Def3;
A9: len iseq = num-polytopes(p,k) by A8,Def14;
A10: dom iseq = Seg (len iseq) by FINSEQ_1:def 3;
A11: n in dom iseq by A6,A7,A9,A10,FINSEQ_1:3;
A12: iseq.n = 1.Z_2 by A1,A2,A3,A5,A6,A7,Th59;
for m being Nat st m in dom iseq & m <> n holds iseq.m = 0.Z_2
proof
let m be Nat such that
A13: m in dom iseq and
A14: m <> n;
A15: m in Seg (len iseq) by A13,FINSEQ_1:def 3;
1 <= m & m <= len iseq by A15,FINSEQ_1:3;
hence thesis by A1,A2,A5,A6,A7,A9,A14,Th60;
end;
hence thesis by A11,A12,MATRIX_3:14;
end;
theorem Th62:
for x being Element of 0-polytopes(p)
holds (0-boundary(p)).({x}) = {{}}
proof
let x be Element of 0-polytopes(p);
set T = 0-boundary(p);
reconsider minusone = 0 - 1 as Integer;
A1: 0-polytopes(p) is non empty by Th55;
reconsider v = {x} as Subset of 0-polytopes(p) by A1,ZFMISC_1:37;
reconsider v as Element of 0-chain-space(p);
A2: T.v = Boundary(v) by Def16;
reconsider bv = Boundary(v) as Element of minusone-chain-space(p);
A3: minusone-polytopes(p) is non empty by Def3;
(0-1)-polytopes(p) = {{}} by Def3;
then reconsider null = {} as Element of (0-1)-polytopes(p) by TARSKI:def 1;
A4: null in bv iff Sum incidence-sequence(null,v) = 1.Z_2 by A3,Def15;
A5: {null} c= bv by A4,Th61,ZFMISC_1:37;
bv c= {null}
proof
let y be set such that A6: y in bv;
A7: [#](minusone-chain-space(p)) = { {}, {{}} } by Th57;
per cases by A7,TARSKI:def 2;
suppose bv = {};
hence thesis by A6;
end;
suppose bv = {{}};
hence thesis by A6;
end;
end;
hence thesis by A2,A5,XBOOLE_0:def 10;
end;
theorem Th63:
k = -1 implies dim(k-bounding-chain-space(p)) = 1
proof
assume A1: k = -1;
set T = 0-boundary(p);
set V = k-bounding-chain-space(p);
Card [#]V = 2
proof
A2: T.(0.(0-chain-space(p))) = 0.(k-chain-space(p)) by A1,RANKNULL:9
.= {};
A3: 0-polytopes(p) <> {} by Th55;
consider x being set such that
A4: x in 0-polytopes(p) by A3,XBOOLE_0:def 1;
reconsider x as Element of 0-polytopes(p) by A4;
set v = {x};
A5: T.v = {{}} by Th62;
A6: dom T = [#](0-chain-space(p)) by RANKNULL:7;
reconsider v as Subset of 0-polytopes(p) by A4,ZFMISC_1:37;
reconsider v as Element of 0-chain-space(p);
A7: v in dom T by A6;
A8: {} in rng T by A2,A6,FUNCT_1:12;
A9: {{}} in rng T by A5,A7,FUNCT_1:12;
A10: {{},{{}}} c= rng T by A8,A9,ZFMISC_1:38;
A11: Card {{},{{}}} = 2 by CARD_2:76;
A12: 2 <=` Card rng T by A10,A11,CARD_1:27;
A13: Card rng T = Card (T .: [#](0-chain-space(p))) by FUNCT_2:45
.= Card [#]V by A1,RANKNULL:def 2;
A14: [#]V c= [#](k-chain-space(p)) by VECTSP_4:def 2;
Card [#]V <=` Card [#](k-chain-space(p)) by A14,CARD_1:27; then
Card [#]V <=` 2 by A1,Th56;
hence thesis by A12,A13,XBOOLE_0:def 10;
end;
hence thesis by RANKNULL:6;
end;
theorem Th64:
Card [#](dim(p)-chain-space(p)) = 2
proof
A1: dim(p)-polytopes(p) = {p} by Def3;
A2: Card (dim(p)-polytopes(p)) = 1 by A1,CARD_1:50;
Card [#]((dim(p))-chain-space(p)) = exp(2,1) by A2,BSPACE:43
.= 2 by CARD_2:40;
hence thesis;
end;
theorem Th65:
{p} is Element of dim(p)-chain-space(p)
proof
dim(p)-polytopes(p) = {p} by Def3;
hence thesis by ZFMISC_1:def 1;
end;
theorem Th66:
{p} in [#](dim(p)-chain-space(p))
proof
{p} is Element of dim(p)-chain-space(p) by Th65;
hence thesis;
end;
theorem Th67:
(dim(p) - 1)-polytopes(p) is non empty
proof
set n = dim(p) - 1;
A1: -1 <= n
proof
0 - 1 = -1;
hence thesis by XREAL_1:11;
end;
n <= dim(p) by XREAL_1:148;
hence thesis by A1,Th26;
end;
registration
let p be polyhedron;
cluster
(dim(p)-1)-polytopes(p) -> non empty;
coherence by Th67;
end;
theorem Th68:
[#](dim(p)-chain-space(p))
= { 0.(dim(p)-chain-space(p)), {p} }
proof
set V = dim(p)-chain-space(p);
set X = { 0.V, {p} };
set C = [#]V;
A1: Card C = 2 by Th64;
reconsider C as finite set;
consider a,b being set such that
A2: a <> b and
A3: C = {a,b} by A1,CARD_2:79;
{p} in C by Th66;
hence thesis by A2,A3,Th1;
end;
theorem Th69:
for x being Element of dim(p)-chain-space(p)
holds x = 0.(dim(p)-chain-space(p))
or x = {p}
proof
set V = dim(p)-chain-space(p);
let x be Element of V;
A1: x in [#]V;
x in { 0.V, {p} } by A1,Th68;
hence thesis by TARSKI:def 2;
end;
theorem Th70:
for x,y being Element of dim(p)-chain-space(p)
st x <> y
holds x = 0.(dim(p)-chain-space(p))
or y = 0.(dim(p)-chain-space(p))
proof
set V = dim(p)-chain-space(p);
let x,y be Element of V such that
A1: x <> y;
assume A2: x <> 0.V;
assume A3: y <> 0.V;
x = {p} by A2,Th69;
hence contradiction by A1,A3,Th69;
end;
theorem
dim(p)-polytope-seq(p) = <*p*> by Def5;
theorem Th72:
1-th-polytope(p,dim(p)) = p
proof
reconsider egy = 1 as Nat;
A1: egy <= num-polytopes(p,dim(p)) by Th32;
set s = dim(p)-polytope-seq(p);
A2: s = <*p*> by Def5;
egy-th-polytope(p,dim(p)) = s.egy by A1,Def10
.= p by A2,FINSEQ_1:57;
hence thesis;
end;
theorem Th73:
for c being Element of dim(p)-chain-space(p),
x being Element of dim(p)-polytopes(p)
st c = {p}
holds c@x = 1.Z_2
proof
let c be Element of dim(p)-chain-space(p),
x be Element of dim(p)-polytopes(p) such that
A1: c = {p};
dim(p)-polytopes(p) = {p} by Def3;
hence thesis by A1,BSPACE:def 3;
end;
theorem Th74:
for x being Element of (dim(p)-1)-polytopes(p),
c being Element of dim(p)-polytopes(p)
st c = p
holds incidence-value(x,c) = 1.Z_2
proof
let x be Element of (dim(p)-1)-polytopes(p),
c be Element of dim(p)-polytopes(p) such that
A1: c = p;
set f = [:(dim(p)-1)-polytopes(p),{p}:] --> 1.Z_2;
A2: eta(p,dim(p)) = f by Def4;
A3: dom f = [:(dim(p)-1)-polytopes(p),{p}:] by FUNCOP_1:19;
A4: c in {p} by A1,TARSKI:def 1;
A5: [x,c] in dom f by A3,A4,ZFMISC_1:106;
A6: f.(x,c) in rng f by A5,FUNCT_1:12;
A7: f.(x,c) in {1.Z_2} by A6,FUNCOP_1:14;
f.(x,c) = 1.Z_2 by A7,TARSKI:def 1;
hence thesis by A2,Def11;
end;
theorem Th75:
for x being Element of (dim(p)-1)-polytopes(p),
c being Element of dim(p)-chain-space(p)
st c = {p}
holds incidence-sequence(x,c) = <*1.Z_2*>
proof
let x be Element of (dim(p)-1)-polytopes(p),
c be Element of dim(p)-chain-space(p) such that
A1: c = {p};
set iseq = incidence-sequence(x,c);
A2: num-polytopes(p,dim(p))= 1 by Th32;
A3: len iseq = 1 by A2,Def14;
iseq.1 = 1.Z_2
proof
reconsider egy = 1 as Nat;
A4: egy <= num-polytopes(p,dim(p)) by Th32;
set z = egy-th-polytope(p,dim(p));
A5: z = p by Th72;
A6: iseq.egy = (c@z)*(incidence-value(x,z)) by A4,Def14;
A7: c@z = 1.Z_2 by A1,Th73;
incidence-value(x,z) = 1.Z_2 by A5,Th74;
hence thesis by A6,A7,VECTSP_1:def 16;
end;
hence thesis by A3,FINSEQ_1:57;
end;
theorem Th76:
for x being Element of (dim(p)-1)-polytopes(p),
c being Element of dim(p)-chain-space(p)
st c = {p}
holds Sum incidence-sequence(x,c) = 1.Z_2
proof
let x be Element of (dim(p)-1)-polytopes(p),
c be Element of dim(p)-chain-space(p) such that
A1: c = {p};
incidence-sequence(x,c) = <*1.Z_2*> by A1,Th75;
hence thesis by FINSOP_1:12;
end;
:: The boundary operation applied to the unique non-zero vector of the
:: dim(p)-chain space gives the "top" vector of the (dim(p)-1)-chain
:: space. In other words, every (dim(p)-1)-polytope is incidence to
:: the whole polyhedron.
theorem Th77:
(dim(p)-boundary(p)).{p} = (dim(p)-1)-polytopes(p)
proof
set T = dim(p)-boundary(p);
set X = (dim(p)-1)-polytopes(p);
reconsider c = {p} as Element of dim(p)-chain-space(p) by Th65;
reconsider d = X as Element of (dim(p)-1)-chain-space(p) by ZFMISC_1:def 1;
reconsider Tc = T.c as Element of (dim(p)-1)-chain-space(p);
for x being Element of X
holds x in Tc iff x in d
proof
let x be Element of X;
thus x in Tc implies x in d;
thus x in d implies x in Tc
proof
assume x in d;
A1: Sum incidence-sequence(x,c) = 1.Z_2 by Th76;
x in Boundary(c) by A1,Def15;
hence thesis by Def16;
end;
end;
hence thesis by SUBSET_1:8;
end;
theorem Th78:
dim(p)-boundary(p) is one-to-one
proof
set T = dim(p)-boundary(p);
set U = (dim(p) - 1)-chain-space(p);
set V = dim(p)-chain-space(p);
set A = (dim(p) - 1)-polytopes(p);
set B = {p};
assume A1: not T is one-to-one;
consider x1,x2 being set such that
A2: x1 in dom T and
A3: x2 in dom T and
A4: T.x1 = T.x2 and
A5: x1 <> x2 by A1,FUNCT_1:def 8;
reconsider x1 as Element of V by A2;
reconsider x2 as Element of V by A3;
per cases by A5,Th70;
suppose A6: x1 = 0.V;
A7: x2 = B by A5,A6,Th69;
T.x1 = 0.U by A6,RANKNULL:9;
hence thesis by A4,A7,Th77;
end;
suppose A8: x2 = 0.V;
A9: x1 = B by A5,A8,Th69;
T.x2 = 0.U by A8,RANKNULL:9;
hence thesis by A4,A9,Th77;
end;
end;
theorem Th79:
dim ((dim(p)-1)-bounding-chain-space(p)) = 1
proof
set d = dim(p);
set T = d-boundary(p);
set U = d-chain-space(p);
set V = (d-1)-bounding-chain-space(p);
A1: T is one-to-one by Th78;
A2: Card [#]V = Card (T .: [#]U) by RANKNULL:def 2
.= Card (rng T) by FUNCT_2:45;
A3: Card (dom T) = Card [#]U by RANKNULL:7
.= 2 by Th64;
Card [#]V = 2 by A1,A2,A3,Th2;
hence thesis by RANKNULL:6;
end;
theorem Th80:
p is simply-connected implies dim ((dim(p)-1)-circuit-space(p)) = 1
proof
assume A1: p is simply-connected;
set d = dim(p);
set U = (d-1)-bounding-chain-space(p);
set V = (d-1)-circuit-space(p);
U = V by A1,Th51;
hence thesis by Th79;
end;
theorem Th81:
1 < n & n < dim(p) + 2
implies (alternating-f-vector(p)).n
= (alternating-proper-f-vector(p)).(n-1)
proof
assume A1: 1 < n;
assume A2: n < dim(p) + 2;
set acs = alternating-f-vector(p);
set apcs = alternating-proper-f-vector(p);
A3: acs.n = ((-1)|^n)*num-polytopes(p,n-2) by A1,A2,Def24;
A4: 0 <= n - 1
proof
1 - 1 = 0;
hence thesis by A1,XREAL_1:15;
end;
reconsider m = n - 1 as Element of NAT by A4,INT_1:16;
reconsider m as Nat;
A5: 1 <= m
proof
A6: 2 <= n
proof
1 + 1 = 2;
hence thesis by A1,INT_1:20;
end;
2 - 1 = 1;
hence thesis by A6,XREAL_1:15;
end;
A7: m <= dim(p)
proof
A8: n < (dim(p) + 1) + 1 by A2;
A9: n <= dim(p) + 1 by A8,NAT_1:13;
n - 1 <= (dim(p) + 1) - 1 by A9,XREAL_1:11;
hence thesis;
end;
apcs.m = ((-1)|^(m+1))*num-polytopes(p,m-1) by A5,A7,Def25;
hence thesis by A3;
end;
theorem Th82:
alternating-f-vector(p)
= <*-1*> ^ alternating-proper-f-vector(p) ^ <*(-1)|^(dim(p))*>
proof
set acs = alternating-f-vector(p);
set apcs = alternating-proper-f-vector(p);
set r = <*-1*> ^ apcs ^ <*(-1)|^(dim(p))*>;
set n = dim(p);
A1: len acs = n + 2 by Def24;
A2: len apcs = n by Def25;
A3: len r = (len <*-1*>) + (len apcs) + (len <*(-1)|^(dim(p))*>) by Th16;
A4: len <*-1*> = 1 by FINSEQ_1:56;
A5: len <*(-1)|^(dim(p))*> = 1 by FINSEQ_1:56;
for k being Nat
st 1 <= k & k <= len acs
holds acs.k = r.k
proof
let k be Nat such that
A6: 1 <= k and
A7: k <= len acs;
per cases by A1,A6,A7,XXREAL_0:1;
suppose A8: k = 1;
A9: 1 <= n + 2 by Th12;
reconsider o = 1 as Nat;
A10: o - 2 = -1;
A11: acs.o = ((-1)|^o)*num-polytopes(p,-1) by A9,A10,Def24;
A12: (-1)|^1 = -1 by Th4,Th9;
num-polytopes(p,-1) = 1 by Th31;
hence thesis by A8,A11,A12,Th17;
end;
suppose A13: k = n + 2;
A14: 1 <= k by A13,Th12;
A15: acs.k = ((-1)|^k)*num-polytopes(p,k-2) by A13,A14,Def24;
A16: r.k = (-1)|^k
proof
A17: k = (len <*-1*> + len (apcs) + 1)
proof
len <*-1*> = 1 by FINSEQ_1:56;
hence thesis by A2,A13;
end;
r.k = (-1)|^(dim(p)) by A17,Th18
.= (-1)|^k by A13,Th14;
hence thesis;
end;
num-polytopes(p,k-2) = 1 by A13,Th32;
hence thesis by A15,A16;
end;
suppose A18: 1 < k & k < n + 2;
set m = k - 1;
A19: len <*-1*> = 1 by FINSEQ_1:56;
A20: k <= len (<*-1*> ^ apcs)
proof
A21: len (<*-1*> ^ apcs) = (len <*-1*> + len apcs) by FINSEQ_1:35
.= n + 1 by A2,FINSEQ_1:56;
A22: k + 1 <= n + 2 by A18,INT_1:20;
A23: (k + 1) - 1 = k;
(n + 2) - 1 = n + 1;
hence thesis by A21,A22,A23,XREAL_1:11;
end;
r.k = apcs.m by A18,A19,A20,Th19;
hence thesis by A18,Th81;
end;
end;
hence thesis by A1,A2,A3,A4,A5,FINSEQ_1:18;
end;
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
:: A Generalized Euler Relation and its 1-, 2-, and 3-dimensional
:: Special Cases
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
begin
theorem Th83:
dim(p) is odd
implies Sum (alternating-f-vector(p))
= Sum (alternating-proper-f-vector(p)) - 2
proof
assume A1: dim(p) is odd;
set acs = alternating-f-vector(p);
set apcs = alternating-proper-f-vector(p);
A2: acs = <*-1*> ^ apcs ^ <*(-1)|^(dim(p))*> by Th82;
A3: (-1)|^(dim(p)) = -1 by A1,Th9;
reconsider minusone = -1 as Integer;
reconsider lastterm = (-1)|^(dim(p)) as Integer;
Sum acs = (Sum <*minusone*>) + (Sum apcs) + (Sum <*lastterm*>) by A2,Th22
.= (Sum <*minusone*>) + (Sum apcs) + (-1) by A3,RVSUM_1:103
.= (-1) + (Sum apcs) + (-1) by RVSUM_1:103
.= (Sum apcs) - 2;
hence thesis;
end;
theorem Th84:
dim(p) is even
implies Sum (alternating-f-vector(p))
= Sum (alternating-proper-f-vector(p))
proof
assume A1: dim(p) is even;
set acs = alternating-f-vector(p);
set apcs = alternating-proper-f-vector(p);
A2: acs = <*-1*> ^ apcs ^ <*(-1)|^(dim(p))*> by Th82;
A3: (-1)|^(dim(p)) = 1 by A1,Th8;
reconsider minusone = -1 as Integer;
reconsider plusone = 1 as Integer;
reconsider lastterm = (-1)|^(dim(p)) as Integer;
Sum acs = (Sum <*minusone*>) + (Sum apcs) + (Sum <*lastterm*>) by A2,Th22
.= (Sum <*minusone*>) + (Sum apcs) + 1 by A3,RVSUM_1:103
.= (-1) + (Sum apcs) + 1 by RVSUM_1:103
.= Sum apcs;
hence thesis;
end;
theorem Th85:
dim(p) = 1 implies
Sum alternating-proper-f-vector(p)
= num-polytopes(p,0)
proof
assume A1: dim(p) = 1;
set apcs = alternating-proper-f-vector(p);
A2: len apcs = 1 by A1,Def25;
reconsider egy = 1 as Nat;
A3: apcs.egy = (-1)|^(egy+1)*num-polytopes(p,egy-1) by A1,Def25;
A4: (-1)|^(egy+1) = 1 by Th5,Th8;
apcs = <*num-polytopes(p,0)*> by A2,A3,A4,FINSEQ_1:57;
hence thesis by RVSUM_1:103;
end;
theorem Th86:
dim(p) = 2 implies
Sum alternating-proper-f-vector(p)
= num-polytopes(p,0) - num-polytopes(p,1)
proof
assume A1: dim(p) = 2;
set apcs = alternating-proper-f-vector(p);
A2: len apcs = 2 by A1,Def25;
reconsider o = 1 as Nat;
reconsider t = 2 as Nat;
reconsider mo = -1 as Integer;
A3: apcs.o = ((-1)|^(o+1))*num-polytopes(p,o-1) by A1,Def25;
A4: apcs.t = ((-1)|^(t+1))*num-polytopes(p,t-1) by A1,Def25;
A5: (-1)|^(o+1) = 1 by Th5,Th8;
A6: (-1)|^(t+1) = -1 by Th6,Th9;
reconsider apcso = apcs.o as Integer;
reconsider apcst = apcs.t as Integer;
A7: apcs = <*apcso,apcst*> by A2,FINSEQ_1:61;
reconsider apcsonetwo = <*apcso,apcst*> as FinSequence of INT;
Sum apcs = apcso + apcst by A7,RVSUM_1:107
.= num-polytopes(p,0) - num-polytopes(p,1) by A3,A4,A5,A6;
hence thesis;
end;
theorem Th87:
dim(p) = 3 implies
Sum alternating-proper-f-vector(p)
= num-polytopes(p,0) - num-polytopes(p,1) + num-polytopes(p,2)
proof
assume A1: dim(p) = 3;
set apcs = alternating-proper-f-vector(p);
A2: len apcs = 3 by A1,Def25;
reconsider o = 1 as Nat;
reconsider tw = 2 as Nat;
reconsider th = 3 as Nat;
reconsider mo = -1 as Integer;
A3: (-1)|^(o+1) = 1 by Th5,Th8;
A4: (-1)|^(tw+1) = -1 by Th6,Th9;
A5: (-1)|^(th+1) = 1 by Th7,Th8;
A6: apcs.o = o*num-polytopes(p,o-1) by A1,A3,Def25;
A7: apcs.tw = mo*num-polytopes(p,tw-1) by A1,A4,Def25;
A8: apcs.th = o*num-polytopes(p,th-1) by A1,A5,Def25;
reconsider apcson = apcs.o as Integer;
reconsider apcstw = apcs.tw as Integer;
reconsider apcsth = apcs.th as Integer;
A9: apcs = <*apcson,apcstw,apcsth*> by A2,FINSEQ_1:62;
reconsider apcsonetwothree = <*apcson,apcstw,apcsth*> as FinSequence of INT;
Sum apcs = apcson + apcstw + apcsth by A9,RVSUM_1:108
.= num-polytopes(p,0)
- num-polytopes(p,1)
+ num-polytopes(p,2) by A6,A7,A8;
hence thesis;
end;
:: A trivial special case
theorem Th88:
dim(p) = 0 implies p is eulerian
proof
set d = dim(p);
assume A1: d = 0;
set apcs = alternating-proper-f-vector(p);
A2: (-1)|^(d+1) = -1 by A1,NEWTON:10;
A3: 1 + (-1)|^(d+1) = 0 by A2;
A4: len apcs = 0 by A1,Def25;
apcs = <*>INT by A4,FINSEQ_1:32;
hence thesis by A3,Def27,GR_CY_1:22;
end;
theorem Th89:
p is simply-connected implies p is eulerian
proof
assume A1: p is simply-connected;
set apcs = alternating-proper-f-vector(p);
per cases;
suppose dim(p) = 0;
hence thesis by Th88;
end;
suppose A2: dim(p) > 0;
A3: len apcs > 0 by A2,Def25;
:: Split the alternating characteristic sequence into a sum of two
:: sequences, a and b
deffunc A(Nat)
= ((-1)|^($1+1))*(dim (($1-2)-bounding-chain-space(p)));
deffunc B(Nat)
= ((-1)|^($1+1))*(dim (($1-1)-circuit-space(p)));
consider a being FinSequence such that
A4: len a = len apcs and
A5: for n being Nat st n in Seg len apcs
holds a.n = A(n) from FINSEQ_1:sch 2;
consider b being FinSequence such that
A6: len b = len apcs and
A7: for n being Nat st n in Seg (len apcs)
holds b.n = B(n) from FINSEQ_1:sch 2;
A8: rng a c= INT & rng b c= INT
proof
thus rng a c= INT
proof
let y be set such that
A9: y in rng a;
consider x being set such that
A10: x in dom a and
A11: y = a.x by A9,FUNCT_1:def 5;
A12: x in Seg (len apcs) by A4,A10,FINSEQ_1:def 3;
reconsider x as Element of NAT by A12;
a.x = ((-1)|^(x+1))*(dim ((x-2)-bounding-chain-space(p))) by A5,A12;
hence thesis by A11;
end;
thus rng b c= INT
proof
let y be set such that
A13: y in rng b;
consider x being set such that
A14: x in dom b and
A15: y = b.x by A13,FUNCT_1:def 5;
A16: x in Seg (len apcs) by A6,A14,FINSEQ_1:def 3;
reconsider x as Element of NAT by A16;
b.x = ((-1)|^(x+1))*(dim ((x-1)-circuit-space(p))) by A7,A16;
hence thesis by A15;
end;
end;
reconsider a,b as FinSequence of INT by A8,FINSEQ_1:def 4;
A17: for n being Nat
st 1 <= n & n <= len apcs
holds apcs.n = a.n + b.n
proof
let n be Nat such that
A18: 1 <= n and
A19: n <= len apcs;
A20: apcs.n = ((-1)|^(n+1))*(dim ((n-2)-bounding-chain-space(p)))
+ ((-1)|^(n+1))*(dim ((n-1)-circuit-space(p))) by A18,A19,Th52;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
A21: n' in Seg (len apcs) by A18,A19;
a.n' = ((-1)|^(n'+1))*(dim ((n'-2)-bounding-chain-space(p)))
by A5,A21;
hence thesis by A7,A20,A21;
end;
:: Now we want to how that the alternating characterstic sequence is
:: a telescoping sum of the sequences a and b. First, we establish
:: the necessary relation among the sequences a and b.
A22: for n being Nat
st 1 <= n & n < len apcs
holds b.n = -(a.(n+1))
proof
let n be Nat such that
A23: 1 <= n and
A24: n < len apcs;
A25: n in Seg (len apcs) by A23,A24,FINSEQ_1:3;
reconsider n as Element of NAT by ORDINAL1:def 13;
A26: b.n = ((-1)|^(n+1))*(dim ((n-1)-circuit-space(p))) by A7,A25;
A27: n + 1 <= len apcs by A24,INT_1:20;
A28: 1 <= n + 1 by NAT_1:11;
A29: n + 1 in Seg (len apcs) by A27,A28;
a.(n+1) = A(n+1) by A5,A29
.= (((-1)|^(n+1))*((-1)|^1))*(dim ((n-1)-bounding-chain-space(p)))
by NEWTON:13
.= ((-1)|^(n+1))*(-1)*(dim ((n-1)-bounding-chain-space(p)))
by NEWTON:10
.= -((-1)|^(n+1))*(dim ((n-1)-bounding-chain-space(p)))
.= -(b.n) by A1,A26,Th51;
hence thesis;
end;
A30: Sum apcs = (a.1) + (b.(len apcs)) by A3,A4,A6,A17,A22,Th15;
A31: a.1 = 1
proof
reconsider egy = 1 as Element of NAT;
A32: 1 <= 0 + 1;
A33: egy <= len apcs by A3,A32,NAT_1:13;
A34: egy in Seg (len apcs) by A33;
a.egy = ((-1)|^(1+1))*(dim ((egy-2)-bounding-chain-space(p))) by A5,A34
.= 1*(dim ((egy-2)-bounding-chain-space(p))) by Th5,Th8
.= 1 by Th63;
hence thesis;
end;
b.(len apcs) = (-1)|^(dim(p)+1)
proof
reconsider n = len apcs as Element of NAT;
A35: n = dim(p) by Def25;
A36: 0 + 1 = 1;
A37: 1 <= len apcs by A3,A36,NAT_1:13;
A38: n in Seg (len apcs) by A37;
b.n = B(n) by A7,A38
.= ((-1)|^(n+1))*1 by A1,A35,Th80
.= (-1)|^(n+1);
hence thesis by Def25;
end;
hence thesis by A30,A31,Def27;
end;
end;
:: Euler's Polyhedron Formula in One Dimension: simply-connected
:: 1-dimensional polyhedra are just line segments.
theorem
p is simply-connected & dim(p) = 1
implies num-vertices(p) = 2
proof
assume A1: p is simply-connected;
assume A2: dim(p) = 1;
set acs = alternating-f-vector(p);
set apcs = alternating-proper-f-vector(p);
A3: p is eulerian by A1,Th89;
0 = Sum acs by A3,Def29
.= Sum apcs - 2 by A2,Th4,Th83
.= num-polytopes(p,0) - 2 by A2,Th85;
hence thesis;
end;
:: Euler's Polyhedron Formula in Two Dimensions: polygons have exactly
:: as many vertices as edges.
theorem
p is simply-connected & dim(p) = 2
implies num-vertices(p) = num-edges(p)
proof
assume A1: p is simply-connected;
assume A2: dim(p) = 2;
A3: p is eulerian by A1,Th89;
set s = num-polytopes(p,0) - num-polytopes(p,1);
A4: s = Sum(alternating-proper-f-vector(p)) by A2,Th86;
set c = alternating-f-vector(p);
0 = Sum c by A3,Def29
.= s by A2,A4,Th5,Th84;
hence thesis;
end;
:: Euler's Polyhedron Formula in Three Dimensions: V - E + F = 2.
theorem
p is simply-connected & dim(p) = 3
implies num-vertices(p) - num-edges(p) + num-faces(p) = 2
proof
assume A1: p is simply-connected;
assume A2: dim(p) = 3;
A3: p is eulerian by A1,Th89;
set s = num-polytopes(p,0) - num-polytopes(p,1) + num-polytopes(p,2);
A4: s = Sum(alternating-proper-f-vector(p)) by A2,Th87;
set c = alternating-f-vector(p);
0 = Sum c by A3,Def29
.= s - 2 by A2,A4,Th6,Th83;
hence thesis;
end;