:: Euler's Polyhedron Formula
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem Th1: :: POLYFORM:1
for X, c, d being set st ex a, b being set st
( a <> b &amp; X = {a,b} ) &amp; c in X &amp; d in X &amp; c <> d holds
X = {c,d}
proofend;

begin

theorem :: POLYFORM:2
canceled;

theorem Th3: :: POLYFORM:3
for k being Integer st 1 <= k holds
k is Nat
proofend;

definition
let a be Integer;
let b be Nat;
:: original:*
redefine funca * b ->  Element of INT ;
coherence
 a * b is Element of INT by INT_1:def_2;
end;

theorem Th4: :: POLYFORM:4
1 is odd
proofend;

theorem Th5: :: POLYFORM:5
2 is even
proofend;

theorem Th6: :: POLYFORM:6
3 is odd
proofend;

theorem Th7: :: POLYFORM:7
4 is even
proofend;

theorem Th8: :: POLYFORM:8
for n being Nat st n is even holds
(- 1) |^ n = 1
proofend;

theorem Th9: :: POLYFORM:9
for n being Nat st n is odd holds
(- 1) |^ n = - 1
proofend;

theorem Th10: :: POLYFORM:10
for n being Nat holds (- 1) |^ n is Integer
proofend;

definition
let a be Integer;
let n be Nat;
:: original:|^
redefine funca |^ n ->  Element of INT ;
coherence
 a |^ n is Element of INT
proofend;
end;

Lm1:  for x being Element of NAT st 0 < x holds
0 + 1 <= x
by NAT_1:13;

theorem Th11: :: POLYFORM:11
for p, q, r being FinSequence holds len (p ^ q) <= len (p ^ (q ^ r))
proofend;

theorem Th12: :: POLYFORM:12
for n being Nat holds 1 < n + 2
proofend;

theorem Th13: :: POLYFORM:13
(- 1) |^ 2 = 1
proofend;

theorem Th14: :: POLYFORM:14
for n being Nat holds (- 1) |^ n = (- 1) |^ (n + 2)
proofend;

begin

:: A theorem on telescoping sequences of integers.
theorem Th15: :: POLYFORM:15
for a, b, s being FinSequence of INT st len s > 0 &amp; len a = len s &amp; len b = len s &amp; ( for n being Nat st 1 <= n &amp; n <= len s holds
s . n = (a . n) + (b . n) ) &amp; ( for k being Nat st 1 <= k &amp; k < len s holds
b . k = - (a . (k + 1)) ) holds
Sum s = (a . 1) + (b . (len s))
proofend;

theorem Th16: :: POLYFORM:16
for p, q, r being FinSequence holds len ((p ^ q) ^ r) = ((len p) + (len q)) + (len r)
proofend;

theorem Th17: :: POLYFORM:17
for x being set
for p, q being FinSequence holds ((<*x*> ^ p) ^ q) . 1 = x
proofend;

theorem Th18: :: POLYFORM:18
for x being set
for p, q being FinSequence holds ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x
proofend;

theorem Th19: :: POLYFORM:19
for p, q, r being FinSequence
for k being Nat st len p < k &amp; k <= len (p ^ q) holds
((p ^ q) ^ r) . k = q . (k - (len p))
proofend;

definition
let a be Integer;
:: original:<*
redefine func<*a*> ->  FinSequence of INT ;
coherence
 <*a*> is FinSequence of INT
proofend;
end;

definition
let a, b be Integer;
:: original:<*
redefine func<*a,b*> ->  FinSequence of INT ;
coherence
 <*a,b*> is FinSequence of INT
proofend;
end;

definition
let a, b, c be Integer;
:: original:<*
redefine func<*a,b,c*> ->  FinSequence of INT ;
coherence
 <*a,b,c*> is FinSequence of INT
proofend;
end;

definition
let p, q be FinSequence of INT ;
:: original:^
redefine funcp ^ q ->  FinSequence of INT ;
coherence
 p ^ q is FinSequence of INT by FINSEQ_1:75;
end;

theorem Th20: :: POLYFORM:20
for k being Integer
for p being FinSequence of INT holds Sum (<*k*> ^ p) = k + (Sum p)
proofend;

theorem Th21: :: POLYFORM:21
for p, q, r being FinSequence of INT holds Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r)
proofend;

theorem :: POLYFORM:22
for a being Element of Z_2 holds Sum <*a*> = a by FINSOP_1:11;

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 Th23: :: POLYFORM:23
for X, Y being set holds [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y
proofend;

:: 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
attrc1 is strict ;
struct PolyhedronStr  -> ;
aggrPolyhedronStr(# PolytopsF, IncidenceF #) ->  PolyhedronStr ;
sel PolytopsF c1 ->  FinSequence-yielding FinSequence;
sel IncidenceF c1 ->  Function-yielding FinSequence;
end;

:: The following properties, `polyhedron_1', `polyhedron_2', and
:: `polyhedron_3' are admittedly a bit contrived. However, they ensure
:: that a PolyhedronStr is a polyhedron: that there is one more polytope set
:: than incidence matrix, that the incidience matrices are incidence matrices
:: of the right sets, and that each term of the polytope sequence is an
:: enumeration of the respective polytope set.
definition
let p be PolyhedronStr ;
attrp is polyhedron_1  means :Def1: :: POLYFORM:def 1
 len the IncidenceF of p = (len the PolytopsF of p) - 1;
attrp is polyhedron_2  means :Def2: :: POLYFORM:def 2
 for n being Nat st 1 <= n &amp; n < len the PolytopsF of p holds
the IncidenceF of p . n is incidence-matrix of (rng ( the PolytopsF of p . n)),(rng ( the PolytopsF of p . (n + 1)));
attrp is polyhedron_3  means :Def3: :: POLYFORM:def 3
 for n being Nat st 1 <= n &amp; n <= len the PolytopsF of p holds
( not the PolytopsF of p . n is empty &amp; the PolytopsF of p . n is one-to-one );
end;

:: deftheorem Def1 defines polyhedron_1 POLYFORM:def_1_:_
 for p being PolyhedronStr holds
( p is polyhedron_1 iff len the IncidenceF of p = (len the PolytopsF of p) - 1 );

:: deftheorem Def2 defines polyhedron_2 POLYFORM:def_2_:_
 for p being PolyhedronStr holds
( p is polyhedron_2 iff for n being Nat st 1 <= n &amp; n < len the PolytopsF of p holds
the IncidenceF of p . n is incidence-matrix of (rng ( the PolytopsF of p . n)),(rng ( the PolytopsF of p . (n + 1))) );

:: deftheorem Def3 defines polyhedron_3 POLYFORM:def_3_:_
 for p being PolyhedronStr holds
( p is polyhedron_3 iff for n being Nat st 1 <= n &amp; n <= len the PolytopsF of p holds
( not the PolytopsF of p . n is empty &amp; the PolytopsF of p . n is one-to-one ) );

registration
cluster polyhedron_1 polyhedron_2 polyhedron_3 for PolyhedronStr ;
existence
 ex b1 being PolyhedronStr st
( b1 is polyhedron_1 &amp; b1 is polyhedron_2 &amp; b1 is polyhedron_3 )
proofend;
end;

definition
mode polyhedron is polyhedron_1 polyhedron_2 polyhedron_3 PolyhedronStr ;
end;

:: 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  equals :: POLYFORM:def 4
 len the PolytopsF of p;
coherence
 len the PolytopsF of p is Element of NAT ;
end;

:: deftheorem  defines dim POLYFORM:def_4_:_
 for p being polyhedron holds dim p = len the PolytopsF of p;

:: 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;
let k be Integer;
funck -polytopes p ->  finite set  means :Def5: :: POLYFORM:def 5
( ( k < - 1 implies it = {} ) &amp; ( k = - 1 implies it = {{}} ) &amp; ( - 1 < k &amp; k < dim p implies it = rng ( the PolytopsF of p . (k + 1)) ) &amp; ( k = dim p implies it = {p} ) &amp; ( k > dim p implies it = {} ) );
existence
 ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) &amp; ( k = - 1 implies b1 = {{}} ) &amp; ( - 1 < k &amp; k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) &amp; ( k = dim p implies b1 = {p} ) &amp; ( k > dim p implies b1 = {} ) )
proofend;
uniqueness
 for b1, b2 being finite set st ( k < - 1 implies b1 = {} ) &amp; ( k = - 1 implies b1 = {{}} ) &amp; ( - 1 < k &amp; k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) &amp; ( k = dim p implies b1 = {p} ) &amp; ( k > dim p implies b1 = {} ) &amp; ( k < - 1 implies b2 = {} ) &amp; ( k = - 1 implies b2 = {{}} ) &amp; ( - 1 < k &amp; k < dim p implies b2 = rng ( the PolytopsF of p . (k + 1)) ) &amp; ( k = dim p implies b2 = {p} ) &amp; ( k > dim p implies b2 = {} ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines -polytopes POLYFORM:def_5_:_
 for p being polyhedron
for k being Integer
for b3 being finite set holds
( b3 = k -polytopes p iff ( ( k < - 1 implies b3 = {} ) &amp; ( k = - 1 implies b3 = {{}} ) &amp; ( - 1 < k &amp; k < dim p implies b3 = rng ( the PolytopsF of p . (k + 1)) ) &amp; ( k = dim p implies b3 = {p} ) &amp; ( k > dim p implies b3 = {} ) ) );

theorem Th24: :: POLYFORM:24
for p being polyhedron
for k being Integer st - 1 < k &amp; k < dim p holds
( k + 1 is Nat &amp; 1 <= k + 1 &amp; k + 1 <= dim p )
proofend;

theorem Th25: :: POLYFORM:25
for p being polyhedron
for k being Integer holds
( not k -polytopes p is empty iff ( - 1 <= k &amp; k <= dim p ) )
proofend;

theorem :: POLYFORM:26
for p being polyhedron
for k being Integer st k < dim p holds
k - 1 < dim p by XREAL_1:146, XXREAL_0:2;

:: 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;
let k be Integer;
func eta (p,k) ->  incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) means :Def6: :: POLYFORM:def 6
( ( k < 0 implies it = {} ) &amp; ( k = 0 implies it = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) &amp; ( 0 < k &amp; k < dim p implies it = the IncidenceF of p . k ) &amp; ( k = dim p implies it = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) &amp; ( k > dim p implies it = {} ) );
existence
 ex b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) &amp; ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) &amp; ( 0 < k &amp; k < dim p implies b1 = the IncidenceF of p . k ) &amp; ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) &amp; ( k > dim p implies b1 = {} ) )
proofend;
uniqueness
 for b1, b2 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st ( k < 0 implies b1 = {} ) &amp; ( k = 0 implies b1 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) &amp; ( 0 < k &amp; k < dim p implies b1 = the IncidenceF of p . k ) &amp; ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) &amp; ( k > dim p implies b1 = {} ) &amp; ( k < 0 implies b2 = {} ) &amp; ( k = 0 implies b2 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) &amp; ( 0 < k &amp; k < dim p implies b2 = the IncidenceF of p . k ) &amp; ( k = dim p implies b2 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) &amp; ( k > dim p implies b2 = {} ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines eta POLYFORM:def_6_:_
 for p being polyhedron
for k being Integer
for b3 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) holds
( b3 = eta (p,k) iff ( ( k < 0 implies b3 = {} ) &amp; ( k = 0 implies b3 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) &amp; ( 0 < k &amp; k < dim p implies b3 = the IncidenceF of p . k ) &amp; ( k = dim p implies b3 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) &amp; ( k > dim p implies b3 = {} ) ) );

definition
let p be polyhedron;
let k be Integer;
funck -polytope-seq p ->  FinSequence means :Def7: :: POLYFORM:def 7
( ( k < - 1 implies it = <*> {} ) &amp; ( k = - 1 implies it = <*{}*> ) &amp; ( - 1 < k &amp; k < dim p implies it = the PolytopsF of p . (k + 1) ) &amp; ( k = dim p implies it = <*p*> ) &amp; ( k > dim p implies it = <*> {} ) );
existence
 ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) &amp; ( k = - 1 implies b1 = <*{}*> ) &amp; ( - 1 < k &amp; k < dim p implies b1 = the PolytopsF of p . (k + 1) ) &amp; ( k = dim p implies b1 = <*p*> ) &amp; ( k > dim p implies b1 = <*> {} ) )
proofend;
uniqueness
 for b1, b2 being FinSequence st ( k < - 1 implies b1 = <*> {} ) &amp; ( k = - 1 implies b1 = <*{}*> ) &amp; ( - 1 < k &amp; k < dim p implies b1 = the PolytopsF of p . (k + 1) ) &amp; ( k = dim p implies b1 = <*p*> ) &amp; ( k > dim p implies b1 = <*> {} ) &amp; ( k < - 1 implies b2 = <*> {} ) &amp; ( k = - 1 implies b2 = <*{}*> ) &amp; ( - 1 < k &amp; k < dim p implies b2 = the PolytopsF of p . (k + 1) ) &amp; ( k = dim p implies b2 = <*p*> ) &amp; ( k > dim p implies b2 = <*> {} ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines -polytope-seq POLYFORM:def_7_:_
 for p being polyhedron
for k being Integer
for b3 being FinSequence holds
( b3 = k -polytope-seq p iff ( ( k < - 1 implies b3 = <*> {} ) &amp; ( k = - 1 implies b3 = <*{}*> ) &amp; ( - 1 < k &amp; k < dim p implies b3 = the PolytopsF of p . (k + 1) ) &amp; ( k = dim p implies b3 = <*p*> ) &amp; ( k > dim p implies b3 = <*> {} ) ) );

definition
let p be polyhedron;
let k be Integer;
func num-polytopes (p,k) ->  Element of NAT  equals :: POLYFORM:def 8
 card (k -polytopes p);
coherence
 card (k -polytopes p) is Element of NAT ;
end;

:: deftheorem  defines num-polytopes POLYFORM:def_8_:_
 for p being polyhedron
for k being Integer holds num-polytopes (p,k) = card (k -polytopes p);

:: 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 :: POLYFORM:def 9
 num-polytopes (p,0);
correctness
coherence
num-polytopes (p,0) is Element of NAT ;
;
func num-edges p ->  Element of NAT  equals :: POLYFORM:def 10
 num-polytopes (p,1);
correctness
coherence
num-polytopes (p,1) is Element of NAT ;
;
func num-faces p ->  Element of NAT  equals :: POLYFORM:def 11
 num-polytopes (p,2);
correctness
coherence
num-polytopes (p,2) is Element of NAT ;
;
end;

:: deftheorem  defines num-vertices POLYFORM:def_9_:_
 for p being polyhedron holds num-vertices p = num-polytopes (p,0);

:: deftheorem  defines num-edges POLYFORM:def_10_:_
 for p being polyhedron holds num-edges p = num-polytopes (p,1);

:: deftheorem  defines num-faces POLYFORM:def_11_:_
 for p being polyhedron holds num-faces p = num-polytopes (p,2);

theorem Th27: :: POLYFORM:27
for p being polyhedron
for k being Integer holds dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
proofend;

theorem Th28: :: POLYFORM:28
for p being polyhedron
for k being Integer holds len (k -polytope-seq p) = num-polytopes (p,k)
proofend;

theorem Th29: :: POLYFORM:29
for p being polyhedron
for k being Integer holds rng (k -polytope-seq p) = k -polytopes p
proofend;

theorem Th30: :: POLYFORM:30
for p being polyhedron holds num-polytopes (p,(- 1)) = 1
proofend;

theorem Th31: :: POLYFORM:31
for p being polyhedron holds num-polytopes (p,(dim p)) = 1
proofend;

:: 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;
let k be Integer;
let n be Nat;
assume A1: ( 1 <= n &amp; n <= num-polytopes (p,k) ) ;
funcn -th-polytope (p,k) ->  Element of k -polytopes p equals :Def12: :: POLYFORM:def 12
(k -polytope-seq p) . n;
coherence
 (k -polytope-seq p) . n is Element of k -polytopes p
proofend;
end;

:: deftheorem Def12 defines -th-polytope POLYFORM:def_12_:_
 for p being polyhedron
for k being Integer
for n being Nat st 1 <= n &amp; n <= num-polytopes (p,k) holds
n -th-polytope (p,k) = (k -polytope-seq p) . n;

theorem Th32: :: POLYFORM:32
for p being polyhedron
for k being Integer st - 1 <= k &amp; k <= dim p holds
for x being Element of k -polytopes p ex n being Nat st
( x = n -th-polytope (p,k) &amp; 1 <= n &amp; n <= num-polytopes (p,k) )
proofend;

theorem Th33: :: POLYFORM:33
for p being polyhedron
for k being Integer holds k -polytope-seq p is one-to-one
proofend;

theorem Th34: :: POLYFORM:34
for p being polyhedron
for k being Integer
for m, n being Nat st 1 <= n &amp; n <= num-polytopes (p,k) &amp; 1 <= m &amp; m <= num-polytopes (p,k) &amp; n -th-polytope (p,k) = m -th-polytope (p,k) holds
m = n
proofend;

definition
let p be polyhedron;
let k be Integer;
let x be Element of (k - 1) -polytopes p;
let y be Element of k -polytopes p;
assume that
A1: 0 <= k and
A2: k <= dim p ;
func incidence-value (x,y) ->  Element of Z_2 equals :Def13: :: POLYFORM:def 13
(eta (p,k)) . (x,y);
coherence
 (eta (p,k)) . (x,y) is Element of Z_2
proofend;
end;

:: deftheorem Def13 defines incidence-value POLYFORM:def_13_:_
 for p being polyhedron
for k being Integer
for x being Element of (k - 1) -polytopes p
for y being Element of k -polytopes p st 0 <= k &amp; k <= dim p holds
incidence-value (x,y) = (eta (p,k)) . (x,y);

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;
let k be Integer;
funck -chain-space p ->  finite-dimensional VectSp of Z_2  equals :: POLYFORM:def 14
 bspace (k -polytopes p);
coherence
 bspace (k -polytopes p) is finite-dimensional VectSp of Z_2 ;
end;

:: deftheorem  defines -chain-space POLYFORM:def_14_:_
 for p being polyhedron
for k being Integer holds k -chain-space p = bspace (k -polytopes p);

theorem :: POLYFORM:35
for p being polyhedron
for k being Integer
for x being Element of k -polytopes p holds (0. (k -chain-space p)) @ x = 0. Z_2 by BSPACE:14;

theorem Th36: :: POLYFORM:36
for p being polyhedron
for k being Integer holds num-polytopes (p,k) = dim (k -chain-space p)
proofend;

:: A k-chain is a set of k-polytopes.
definition
let p be polyhedron;
let k be Integer;
funck -chains p ->  non empty finite set  equals :: POLYFORM:def 15
 bool (k -polytopes p);
coherence
 bool (k -polytopes p) is non empty finite set ;
end;

:: deftheorem  defines -chains POLYFORM:def_15_:_
 for p being polyhedron
for k being Integer holds k -chains p = bool (k -polytopes p);

definition
let p be polyhedron;
let k be Integer;
let x be Element of (k - 1) -polytopes p;
let v be Element of (k -chain-space p);
func incidence-sequence (x,v) ->  FinSequence of Z_2 means :Def16: :: POLYFORM:def 16
( ( (k - 1) -polytopes p is empty implies it = <*> {} ) &amp; ( not (k - 1) -polytopes p is empty implies ( len it = num-polytopes (p,k) &amp; ( for n being Nat st 1 <= n &amp; n <= num-polytopes (p,k) holds
it . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) );
existence
 ex b1 being FinSequence of Z_2 st
( ( (k - 1) -polytopes p is empty implies b1 = <*> {} ) &amp; ( not (k - 1) -polytopes p is empty implies ( len b1 = num-polytopes (p,k) &amp; ( for n being Nat st 1 <= n &amp; n <= num-polytopes (p,k) holds
b1 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of Z_2 st ( (k - 1) -polytopes p is empty implies b1 = <*> {} ) &amp; ( not (k - 1) -polytopes p is empty implies ( len b1 = num-polytopes (p,k) &amp; ( for n being Nat st 1 <= n &amp; n <= num-polytopes (p,k) holds
b1 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) &amp; ( (k - 1) -polytopes p is empty implies b2 = <*> {} ) &amp; ( not (k - 1) -polytopes p is empty implies ( len b2 = num-polytopes (p,k) &amp; ( for n being Nat st 1 <= n &amp; n <= num-polytopes (p,k) holds
b2 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines incidence-sequence POLYFORM:def_16_:_
 for p being polyhedron
for k being Integer
for x being Element of (k - 1) -polytopes p
for v being Element of (k -chain-space p)
for b5 being FinSequence of Z_2 holds
( b5 = incidence-sequence (x,v) iff ( ( (k - 1) -polytopes p is empty implies b5 = <*> {} ) &amp; ( not (k - 1) -polytopes p is empty implies ( len b5 = num-polytopes (p,k) &amp; ( for n being Nat st 1 <= n &amp; n <= num-polytopes (p,k) holds
b5 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ) );

theorem Th37: :: POLYFORM:37
for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p)
for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)
proofend;

theorem Th38: :: POLYFORM:38
for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
proofend;

theorem Th39: :: POLYFORM:39
for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p)
for 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)))
proofend;

theorem Th40: :: POLYFORM:40
for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p)
for 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)))
proofend;

theorem Th41: :: POLYFORM:41
for p being polyhedron
for k being Integer
for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
proofend;

theorem Th42: :: POLYFORM:42
for p being polyhedron
for k being Integer
for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
proofend;

theorem Th43: :: POLYFORM:43
for p being polyhedron
for k being Integer
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 )
proofend;

theorem Th44: :: POLYFORM:44
for p being polyhedron
for k being Integer
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 ) )
proofend;

scheme :: POLYFORM:sch 1
ChainEx{ F1() ->  polyhedron, F2() ->  Integer, P1[ Element of F2() -polytopes F1()] } :
 ex c being Subset of (F2() -polytopes F1()) st
for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] &amp; x in F2() -polytopes F1() ) )
proofend;

:: 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;
let k be Integer;
let v be Element of (k -chain-space p);
func Boundary v ->  Element of ((k - 1) -chain-space p) means :Def17: :: POLYFORM:def 17
( ( (k - 1) -polytopes p is empty implies it = 0. ((k - 1) -chain-space p) ) &amp; ( not (k - 1) -polytopes p is 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
 ex b1 being Element of ((k - 1) -chain-space p) st
( ( (k - 1) -polytopes p is empty implies b1 = 0. ((k - 1) -chain-space p) ) &amp; ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in b1 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) )
proofend;
uniqueness
 for b1, b2 being Element of ((k - 1) -chain-space p) st ( (k - 1) -polytopes p is empty implies b1 = 0. ((k - 1) -chain-space p) ) &amp; ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in b1 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) &amp; ( (k - 1) -polytopes p is empty implies b2 = 0. ((k - 1) -chain-space p) ) &amp; ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in b2 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines Boundary POLYFORM:def_17_:_
 for p being polyhedron
for k being Integer
for v being Element of (k -chain-space p)
for b4 being Element of ((k - 1) -chain-space p) holds
( b4 = Boundary v iff ( ( (k - 1) -polytopes p is empty implies b4 = 0. ((k - 1) -chain-space p) ) &amp; ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in b4 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) ) );

theorem Th45: :: POLYFORM:45
for p being polyhedron
for k being Integer
for c being Element of (k -chain-space p)
for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))
proofend;

:: Every dimension k has its own boundary operation.
definition
let p be polyhedron;
let k be Integer;
funck -boundary p ->  Function of (k -chain-space p),((k - 1) -chain-space p) means :Def18: :: POLYFORM:def 18
 for c being Element of (k -chain-space p) holds it . c = Boundary c;
existence
 ex b1 being Function of (k -chain-space p),((k - 1) -chain-space p) st
for c being Element of (k -chain-space p) holds b1 . c = Boundary c
proofend;
uniqueness
 for b1, b2 being Function of (k -chain-space p),((k - 1) -chain-space p) st ( for c being Element of (k -chain-space p) holds b1 . c = Boundary c ) &amp; ( for c being Element of (k -chain-space p) holds b2 . c = Boundary c ) holds
b1 = b2
proofend;
end;

:: deftheorem Def18 defines -boundary POLYFORM:def_18_:_
 for p being polyhedron
for k being Integer
for b3 being Function of (k -chain-space p),((k - 1) -chain-space p) holds
( b3 = k -boundary p iff for c being Element of (k -chain-space p) holds b3 . c = Boundary c );

theorem Th46: :: POLYFORM:46
for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p) holds Boundary (c + d) = (Boundary c) + (Boundary d)
proofend;

theorem Th47: :: POLYFORM:47
for p being polyhedron
for k being Integer
for a being Element of Z_2
for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)
proofend;

:: As defined, the k-boundary operator gives rise to a linear
:: transformation.
theorem Th48: :: POLYFORM:48
for p being polyhedron
for k being Integer holds k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)
proofend;

registration
let p be polyhedron;
let k be Integer;
clusterk -boundary p ->  additive homogeneous ;
coherence
 ( k -boundary p is homogeneous &amp; k -boundary p is additive ) by Th48;
end;

:: The term "circuit" is used in Lakatos. (A more customary term is
:: "cycle".)
definition
let p be polyhedron;
let k be Integer;
funck -circuit-space p ->  Subspace of k -chain-space p equals :: POLYFORM:def 19
 ker (k -boundary p);
coherence
 ker (k -boundary p) is Subspace of k -chain-space p ;
end;

:: deftheorem  defines -circuit-space POLYFORM:def_19_:_
 for p being polyhedron
for k being Integer holds k -circuit-space p = ker (k -boundary p);

definition
let p be polyhedron;
let k be Integer;
funck -circuits p ->  non empty Subset of (k -chains p) equals :: POLYFORM:def 20
 [#] (k -circuit-space p);
coherence
 [#] (k -circuit-space p) is non empty Subset of (k -chains p) by VECTSP_4:def_2;
end;

:: deftheorem  defines -circuits POLYFORM:def_20_:_
 for p being polyhedron
for k being Integer holds k -circuits p = [#] (k -circuit-space p);

definition
let p be polyhedron;
let k be Integer;
funck -bounding-chain-space p ->  Subspace of k -chain-space p equals :: POLYFORM:def 21
 im ((k + 1) -boundary p);
coherence
 im ((k + 1) -boundary p) is Subspace of k -chain-space p ;
end;

:: deftheorem  defines -bounding-chain-space POLYFORM:def_21_:_
 for p being polyhedron
for k being Integer holds k -bounding-chain-space p = im ((k + 1) -boundary p);

definition
let p be polyhedron;
let k be Integer;
funck -bounding-chains p ->  non empty Subset of (k -chains p) equals :: POLYFORM:def 22
 [#] (k -bounding-chain-space p);
coherence
 [#] (k -bounding-chain-space p) is non empty Subset of (k -chains p) by VECTSP_4:def_2;
end;

:: deftheorem  defines -bounding-chains POLYFORM:def_22_:_
 for p being polyhedron
for k being Integer holds k -bounding-chains p = [#] (k -bounding-chain-space p);

definition
let p be polyhedron;
let k be Integer;
funck -bounding-circuit-space p ->  Subspace of k -chain-space p equals :: POLYFORM:def 23
(k -bounding-chain-space p) /\ (k -circuit-space p);
coherence
 (k -bounding-chain-space p) /\ (k -circuit-space p) is Subspace of k -chain-space p ;
end;

:: deftheorem  defines -bounding-circuit-space POLYFORM:def_23_:_
 for p being polyhedron
for k being Integer holds k -bounding-circuit-space p = (k -bounding-chain-space p) /\ (k -circuit-space p);

definition
let p be polyhedron;
let k be Integer;
funck -bounding-circuits p ->  non empty Subset of (k -chains p) equals :: POLYFORM:def 24
 [#] (k -bounding-circuit-space p);
coherence
 [#] (k -bounding-circuit-space p) is non empty Subset of (k -chains p) by VECTSP_4:def_2;
end;

:: deftheorem  defines -bounding-circuits POLYFORM:def_24_:_
 for p being polyhedron
for k being Integer holds k -bounding-circuits p = [#] (k -bounding-circuit-space p);

theorem :: POLYFORM:49
for p being polyhedron
for k being Integer holds dim (k -chain-space p) = (rank (k -boundary p)) + (nullity (k -boundary p)) by RANKNULL:44;

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;
attrp is simply-connected  means :Def25: :: POLYFORM:def 25
 for k being Integer holds k -circuits p = k -bounding-chains p;
end;

:: deftheorem Def25 defines simply-connected POLYFORM:def_25_:_
 for p being polyhedron holds
( p is simply-connected iff for k being Integer holds k -circuits p = k -bounding-chains p );

theorem Th50: :: POLYFORM:50
for p being polyhedron holds
( p is simply-connected iff for n being Integer holds n -circuit-space p = n -bounding-chain-space p )
proofend;

definition
let p be polyhedron;
func alternating-f-vector p ->  FinSequence of INT  means :Def26: :: POLYFORM:def 26
( len it = (dim p) + 2 &amp; ( for k being Nat st 1 <= k &amp; k <= (dim p) + 2 holds
it . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) );
existence
 ex b1 being FinSequence of INT st
( len b1 = (dim p) + 2 &amp; ( for k being Nat st 1 <= k &amp; k <= (dim p) + 2 holds
b1 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of INT st len b1 = (dim p) + 2 &amp; ( for k being Nat st 1 <= k &amp; k <= (dim p) + 2 holds
b1 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) &amp; len b2 = (dim p) + 2 &amp; ( for k being Nat st 1 <= k &amp; k <= (dim p) + 2 holds
b2 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def26 defines alternating-f-vector POLYFORM:def_26_:_
 for p being polyhedron
for b2 being FinSequence of INT holds
( b2 = alternating-f-vector p iff ( len b2 = (dim p) + 2 &amp; ( for k being Nat st 1 <= k &amp; k <= (dim p) + 2 holds
b2 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) ) );

definition
let p be polyhedron;
func alternating-proper-f-vector p ->  FinSequence of INT  means :Def27: :: POLYFORM:def 27
( len it = dim p &amp; ( for k being Nat st 1 <= k &amp; k <= dim p holds
it . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) );
existence
 ex b1 being FinSequence of INT st
( len b1 = dim p &amp; ( for k being Nat st 1 <= k &amp; k <= dim p holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of INT st len b1 = dim p &amp; ( for k being Nat st 1 <= k &amp; k <= dim p holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) &amp; len b2 = dim p &amp; ( for k being Nat st 1 <= k &amp; k <= dim p holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def27 defines alternating-proper-f-vector POLYFORM:def_27_:_
 for p being polyhedron
for b2 being FinSequence of INT holds
( b2 = alternating-proper-f-vector p iff ( len b2 = dim p &amp; ( for k being Nat st 1 <= k &amp; k <= dim p holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) );

definition
let p be polyhedron;
func alternating-semi-proper-f-vector p ->  FinSequence of INT  means :Def28: :: POLYFORM:def 28
( len it = (dim p) + 1 &amp; ( for k being Nat st 1 <= k &amp; k <= (dim p) + 1 holds
it . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) );
existence
 ex b1 being FinSequence of INT st
( len b1 = (dim p) + 1 &amp; ( for k being Nat st 1 <= k &amp; k <= (dim p) + 1 holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of INT st len b1 = (dim p) + 1 &amp; ( for k being Nat st 1 <= k &amp; k <= (dim p) + 1 holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) &amp; len b2 = (dim p) + 1 &amp; ( for k being Nat st 1 <= k &amp; k <= (dim p) + 1 holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def28 defines alternating-semi-proper-f-vector POLYFORM:def_28_:_
 for p being polyhedron
for b2 being FinSequence of INT holds
( b2 = alternating-semi-proper-f-vector p iff ( len b2 = (dim p) + 1 &amp; ( for k being Nat st 1 <= k &amp; k <= (dim p) + 1 holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) );

theorem Th51: :: POLYFORM:51
for p being polyhedron
for n being Nat st 1 <= n &amp; n <= len (alternating-proper-f-vector p) holds
(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)))
proofend;

:: The term "eulerian" comes from Lakatos.
definition
let p be polyhedron;
attrp is eulerian  means :Def29: :: POLYFORM:def 29
 Sum (alternating-proper-f-vector p) = 1 + ((- 1) |^ ((dim p) + 1));
end;

:: deftheorem Def29 defines eulerian POLYFORM:def_29_:_
 for p being polyhedron holds
( p is eulerian iff Sum (alternating-proper-f-vector p) = 1 + ((- 1) |^ ((dim p) + 1)) );

theorem Th52: :: POLYFORM:52
for p being polyhedron holds alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>
proofend;

:: Another characterization of Eulerian polyhedra
definition
let p be polyhedron;
redefine attr p is eulerian  means :Def30: :: POLYFORM:def 30
 Sum (alternating-semi-proper-f-vector p) = 1;
compatibility
 ( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 )
proofend;
end;

:: deftheorem Def30 defines eulerian POLYFORM:def_30_:_
 for p being polyhedron holds
( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 );

theorem Th53: :: POLYFORM:53
for p being polyhedron holds alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p)
proofend;

:: Yet another characterization of eulerian polyhedra
definition
let p be polyhedron;
redefine attr p is eulerian  means :Def31: :: POLYFORM:def 31
 Sum (alternating-f-vector p) = 0 ;
compatibility
 ( p is eulerian iff Sum (alternating-f-vector p) = 0 )
proofend;
end;

:: deftheorem Def31 defines eulerian POLYFORM:def_31_:_
 for p being polyhedron holds
( p is eulerian iff Sum (alternating-f-vector p) = 0 );

begin

theorem Th54: :: POLYFORM:54
for p being polyhedron holds not 0 -polytopes p is empty
proofend;

theorem Th55: :: POLYFORM:55
for p being polyhedron holds card ([#] ((- 1) -chain-space p)) = 2
proofend;

theorem Th56: :: POLYFORM:56
for p being polyhedron holds [#] ((- 1) -chain-space p) = {{},{{}}}
proofend;

theorem Th57: :: POLYFORM:57
for p being polyhedron
for k being Integer
for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p st k = 0 &amp; e = {} holds
incidence-value (e,x) = 1. Z_2
proofend;

theorem Th58: :: POLYFORM:58
for p being polyhedron
for k being Integer
for x being Element of k -polytopes p
for v being Element of (k -chain-space p)
for e being Element of (k - 1) -polytopes p
for n being Nat st k = 0 &amp; v = {x} &amp; e = {} &amp; x = n -th-polytope (p,k) &amp; 1 <= n &amp; n <= num-polytopes (p,k) holds
(incidence-sequence (e,v)) . n = 1. Z_2
proofend;

theorem Th59: :: POLYFORM:59
for p being polyhedron
for k being Integer
for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p
for v being Element of (k -chain-space p)
for m, n being Nat st k = 0 &amp; v = {x} &amp; x = n -th-polytope (p,k) &amp; 1 <= m &amp; m <= num-polytopes (p,k) &amp; 1 <= n &amp; n <= num-polytopes (p,k) &amp; m <> n holds
(incidence-sequence (e,v)) . m = 0. Z_2
proofend;

theorem Th60: :: POLYFORM:60
for p being polyhedron
for k being Integer
for x being Element of k -polytopes p
for v being Element of (k -chain-space p)
for e being Element of (k - 1) -polytopes p st k = 0 &amp; v = {x} &amp; e = {} holds
Sum (incidence-sequence (e,v)) = 1. Z_2
proofend;

theorem Th61: :: POLYFORM:61
for p being polyhedron
for x being Element of 0 -polytopes p holds (0 -boundary p) . {x} = {{}}
proofend;

theorem Th62: :: POLYFORM:62
for p being polyhedron
for k being Integer st k = - 1 holds
dim (k -bounding-chain-space p) = 1
proofend;

theorem Th63: :: POLYFORM:63
for p being polyhedron holds card ([#] ((dim p) -chain-space p)) = 2
proofend;

theorem Th64: :: POLYFORM:64
for p being polyhedron holds {p} is Element of ((dim p) -chain-space p)
proofend;

theorem Th65: :: POLYFORM:65
for p being polyhedron holds {p} in [#] ((dim p) -chain-space p)
proofend;

theorem Th66: :: POLYFORM:66
for p being polyhedron holds not ((dim p) - 1) -polytopes p is empty
proofend;

registration
let p be polyhedron;
cluster((dim p) - 1) -polytopes p ->  non empty finite ;
coherence
 not ((dim p) - 1) -polytopes p is empty by Th66;
end;

theorem Th67: :: POLYFORM:67
for p being polyhedron holds [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}}
proofend;

theorem Th68: :: POLYFORM:68
for p being polyhedron
for x being Element of ((dim p) -chain-space p) holds
( x = 0. ((dim p) -chain-space p) or x = {p} )
proofend;

theorem Th69: :: POLYFORM:69
for p being polyhedron
for x, y being Element of ((dim p) -chain-space p) holds
( not x <> y or x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )
proofend;

theorem :: POLYFORM:70
for p being polyhedron holds (dim p) -polytope-seq p = <*p*> by Def7;

theorem Th71: :: POLYFORM:71
for p being polyhedron holds 1 -th-polytope (p,(dim p)) = p
proofend;

theorem Th72: :: POLYFORM:72
for p being polyhedron
for c being Element of ((dim p) -chain-space p)
for x being Element of (dim p) -polytopes p st c = {p} holds
c @ x = 1. Z_2
proofend;

theorem Th73: :: POLYFORM:73
for p being polyhedron
for x being Element of ((dim p) - 1) -polytopes p
for c being Element of (dim p) -polytopes p st c = p holds
incidence-value (x,c) = 1. Z_2
proofend;

theorem Th74: :: POLYFORM:74
for p being polyhedron
for x being Element of ((dim p) - 1) -polytopes p
for c being Element of ((dim p) -chain-space p) st c = {p} holds
incidence-sequence (x,c) = <*(1. Z_2)*>
proofend;

theorem Th75: :: POLYFORM:75
for p being polyhedron
for x being Element of ((dim p) - 1) -polytopes p
for c being Element of ((dim p) -chain-space p) st c = {p} holds
Sum (incidence-sequence (x,c)) = 1. Z_2
proofend;

:: 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 Th76: :: POLYFORM:76
for p being polyhedron holds ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p
proofend;

theorem Th77: :: POLYFORM:77
for p being polyhedron holds (dim p) -boundary p is one-to-one
proofend;

theorem Th78: :: POLYFORM:78
for p being polyhedron holds dim (((dim p) - 1) -bounding-chain-space p) = 1
proofend;

theorem Th79: :: POLYFORM:79
for p being polyhedron st p is simply-connected holds
dim (((dim p) - 1) -circuit-space p) = 1
proofend;

theorem Th80: :: POLYFORM:80
for p being polyhedron
for n being Nat st 1 < n &amp; n < (dim p) + 2 holds
(alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)
proofend;

theorem Th81: :: POLYFORM:81
for p being polyhedron holds alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>
proofend;

begin

theorem Th82: :: POLYFORM:82
for p being polyhedron st dim p is odd holds
Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2
proofend;

theorem Th83: :: POLYFORM:83
for p being polyhedron st dim p is even holds
Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p)
proofend;

theorem Th84: :: POLYFORM:84
for p being polyhedron st dim p = 1 holds
Sum (alternating-proper-f-vector p) = num-polytopes (p,0)
proofend;

theorem Th85: :: POLYFORM:85
for p being polyhedron st dim p = 2 holds
Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1))
proofend;

theorem Th86: :: POLYFORM:86
for p being polyhedron st dim p = 3 holds
Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2))
proofend;

:: A trivial special case
theorem Th87: :: POLYFORM:87
for p being polyhedron st dim p = 0 holds
p is eulerian
proofend;

theorem Th88: :: POLYFORM:88
for p being polyhedron st p is simply-connected holds
p is eulerian
proofend;

:: Euler's Polyhedron Formula in One Dimension: simply-connected
:: 1-dimensional polyhedra are just line segments.
theorem :: POLYFORM:89
for p being polyhedron st p is simply-connected &amp; dim p = 1 holds
num-vertices p = 2
proofend;

:: Euler's Polyhedron Formula in Two Dimensions: polygons have exactly
:: as many vertices as edges.
theorem :: POLYFORM:90
for p being polyhedron st p is simply-connected &amp; dim p = 2 holds
num-vertices p = num-edges p
proofend;

:: Euler's Polyhedron Formula in Three Dimensions: V - E + F = 2.
:: [WP: ] Euler's_Polyhedron_Formula
theorem :: POLYFORM:91
for p being polyhedron st p is simply-connected &amp; dim p = 3 holds
((num-vertices p) - (num-edges p)) + (num-faces p) = 2
proofend;