:: Euler's Polyhedron Formula
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, TARSKI, FUNCT_1, CARD_1, RELAT_1, NAT_1, INT_1,
XXREAL_0, SUBSET_1, ABIAN, ARYTM_3, ARYTM_1, NEWTON, POWER, FINSEQ_1,
ORDINAL4, CARD_3, XBOOLE_0, BSPACE, FUNCT_2, ZFMISC_1, SUPINF_2,
MESFUNC1, FUNCOP_1, PRE_POLY, RLVECT_5, FINSET_1, VECTSP_1, QC_LANG1,
RLVECT_3, STRUCT_0, FINSEQ_2, RANKNULL, RLSUB_1, VECTSP10, ORDINAL2,
POLYFORM, MSSUBFAM, UNIALG_1, FUNCT_7, VALUED_0;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1,
FUNCT_2, BINOP_1, CARD_1, ORDINAL1, NUMBERS, FUNCOP_1, FINSET_1,
XCMPLX_0, XXREAL_0, INT_1,
VALUED_0, CARD_2, FINSEQ_1, FINSEQ_2, POWER, RVSUM_1,
NEWTON, ABIAN, STRUCT_0, RLVECT_1, GROUP_1, VECTSP_1, VECTSP_4, VECTSP_5,
VECTSP_7, FVSUM_1, MATRLIN, VECTSP_9, RANKNULL, BSPACE, PRE_POLY, MOD_2;
constructors VECTSP_9, REALSET1, FINSOP_1, FVSUM_1, BSPACE, REAL_1, BINOP_2,
RANKNULL, VECTSP_7, VECTSP_5, NEWTON, GR_CY_1, ABIAN, POWER, CARD_2,
RELSET_1, BINOP_1;
registrations FINSET_1, XBOOLE_0, FUNCT_1, FUNCT_2, RELAT_1, SUBSET_1, NAT_1,
INT_1, VECTSP_1, STRUCT_0, FINSEQ_1, FINSEQ_2, CARD_1, MATRLIN, BSPACE,
ORDINAL1, NEWTON, FUNCOP_1, ABIAN, XREAL_0, NUMBERS, JORDAN23, PRE_POLY,
XCMPLX_0, XXREAL_0, VALUED_0, PARTFUN1, RELSET_1, WSIERP_1;
requirements NUMERALS, BOOLE, ARITHM, SUBSET, REAL;
definitions XBOOLE_0, TARSKI;
equalities BINOP_1, STRUCT_0, FVSUM_1, FINSEQ_1, BSPACE, RANKNULL, ALGSTR_0;
expansions XBOOLE_0, BINOP_1, TARSKI, FINSEQ_1;
theorems XBOOLE_0, FUNCT_1, RELAT_1, TARSKI, ZFMISC_1, FUNCT_2, GROUP_1,
RLVECT_1, VECTSP_1, FVSUM_1, FINSEQ_2, CARD_1, FINSEQ_1, NAT_1, FINSOP_1,
VECTSP_4, BSPACE, RANKNULL, VECTSP_9, ORDINAL1, NEWTON, RVSUM_1, GR_CY_1,
FUNCOP_1, XREAL_1, XXREAL_0, INT_1, POWER, FIB_NUM2, CARD_2, FINSEQ_3,
SUBSET_1, MOD_2, MATRIX_3, CALCUL_1, RELSET_1, RVSUM_2;
schemes FUNCT_2, FINSEQ_1, FINSEQ_2;
begin
theorem Th1:
for X being set, c,d being object
st (ex a,b being object st a <> b & X = {a,b}) &
c in X & d in X & c <> d holds X = {c,d}
proof
let X be set, c,d be object such that
A1: ex a,b being object st a <> b & X = {a,b} and
A2: c in X and
A3: d in X and
A4: c <> d;
consider a,b being object such that
a <> b and
A5: X = {a,b} by A1;
A6: X c= {c,d}
proof
A7: d = a or d = b by A3,A5,TARSKI:def 2;
A8: c = a or c = b by A2,A5,TARSKI:def 2;
let x be object such that
A9: x in X;
per cases by A5,A9,TARSKI:def 2;
suppose
x = a;
hence thesis by A4,A8,A7,TARSKI:def 2;
end;
suppose
x = b;
hence thesis by A4,A8,A7,TARSKI:def 2;
end;
end;
{c,d} c= X by A2,A3,ZFMISC_1:32;
hence thesis by A6;
end;
begin :: Arithmetical Preliminaries
reserve n for Nat,
k for Integer;
::$CT
theorem Th2:
1 <= k implies k is Nat
proof
assume 1 <= k;
then reconsider k as Element of NAT by INT_1:3;
k is Nat;
hence thesis;
end;
theorem Th3:
1 is odd
proof
1 = 2*0+1;
hence thesis;
end;
theorem Th4:
2 is even
proof
2 = 2*1;
hence thesis;
end;
theorem Th5:
3 is odd
proof
3 = 2*1 + 1;
hence thesis;
end;
theorem Th6:
4 is even
proof
4 = 2*2;
hence thesis;
end;
theorem Th7:
n is even implies (-1)|^n = 1
proof
(-1)|^n = (-1) to_power n by POWER:41;
hence thesis by FIB_NUM2:3;
end;
theorem Th8:
n is odd implies (-1)|^n = -1
proof
(-1)|^n = (-1) to_power n by POWER:41;
hence thesis by FIB_NUM2:2;
end;
::$CT
Lm1:
for x being Nat st 0 < x holds 0+1 <= x by NAT_1:13;
theorem Th9:
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:32;
hence thesis by CALCUL_1:6;
end;
theorem Th10:
1 < n + 2
proof
0 < n + 1 implies 1 < n + 2
proof
assume 0 < n + 1;
0 + 1 = 1;
hence thesis by XREAL_1:8;
end;
hence thesis;
end;
theorem Th11:
(-1)|^2 = 1
proof
(-1)|^2 = (-1)|^(1+1) .= ((-1)|^1)*((-1)|^1) by NEWTON:8
.= ((-1)|^1)*(-1)
.= (-1)*(-1);
hence thesis;
end;
theorem Th12:
for n being Nat holds (-1)|^n = (-1)|^(n+2)
proof
let n be Nat;
(-1)|^(n+2) = ((-1)|^n)*((-1)|^2) by NEWTON:8
.= (-1)|^n by Th11;
hence thesis;
end;
begin :: Preliminaries on Finite Sequences
:: A theorem on telescoping sequences of integers.
theorem Th13:
for a,b,s being complex-valued FinSequence 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
defpred P[FinSequence of COMPLEX] means len $1 > 0 implies for a,b being
FinSequence of COMPLEX 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);
A1: for p being FinSequence of COMPLEX, x being Element of COMPLEX st P[p]
holds P[p^<*x*>]
proof
let p be FinSequence of COMPLEX, x be Element of COMPLEX such that
A2: P[p];
set t = p ^ <*x*>;
assume len t > 0;
let a,b be FinSequence of COMPLEX such that
A3: len a = len t and
A4: len b = len t and
A5: for n being Nat st 1 <= n & n <= len t holds t.n = a.n + b.n and
A6: for k being Nat st 1 <= k & k < len t holds b.k = -(a.(k+1));
A7: Sum t = (Sum p) + x by RVSUM_2:31;
per cases;
suppose
A8: len p = 0;
reconsider egy = 1 as Nat;
p = {} by A8;
then
A9: t = <*x*> by FINSEQ_1:34;
then egy <= len t by FINSEQ_1:39;
then
A10: t.egy = a.egy + b.egy by A5;
A11: p = {} by A8;
len t = 1 by A9,FINSEQ_1:39;
hence thesis by A7,A11,A9,A10,GR_CY_1:3;
end;
suppose
A12: len p > 0;
set m = len p;
set a9 = a|m;
A13: a9.1 = a.1
proof
reconsider egy = 1 as Element of NAT;
0 + 1 = 1;
then egy <= len p by A12,INT_1:7;
hence thesis by FINSEQ_3:112;
end;
set b9 = b|m;
A14: b.(len p) = b9.(len p) by FINSEQ_3:112;
A15: for n being Nat st 1 <= n & n < len p holds b9.n = -(a9.(n+1))
proof
let n be Nat such that
A16: 1 <= n and
A17: n < len p;
reconsider n as Element of NAT by ORDINAL1:def 12;
A18: b9.n = b.n by A17,FINSEQ_3:112;
n + 1 <= len p by A17,INT_1:7;
then
A19: a9.(n+1) = a.(n+1) by FINSEQ_3:112;
len p <= len t by CALCUL_1:6;
then n < len t by A17,XXREAL_0:2;
hence thesis by A6,A16,A18,A19;
end;
A20: for n being Nat st 1 <= n & n <= len p holds p.n = a9.n + b9.n
proof
let n be Nat such that
A21: 1 <= n and
A22: n <= len p;
dom p = Seg len p by FINSEQ_1:def 3;
then
A23: n in dom p by A21,A22;
len p <= len t by CALCUL_1:6;
then
A24: n <= len t by A22,XXREAL_0:2;
reconsider n as Element of NAT by ORDINAL1:def 12;
p.n = t.n by A23,FINSEQ_1:def 7
.= a.n + b.n by A5,A21,A24
.= a9.n + b.n by A22,FINSEQ_3:112
.= a9.n + b9.n by A22,FINSEQ_3:112;
hence thesis;
end;
A25: 1 <= len p by A12,Lm1;
len <*x*> = 1 by FINSEQ_1:39;
then
A26: len t = (len p) + 1 by FINSEQ_1:22;
0 + len p = len p;
then len p < len t by A26,XREAL_1:6;
then
A27: b.(len p) = -(a.(len p + 1)) by A6,A25;
0 + 1 = 1;
then
A28: 1 <= len t by A26,XREAL_1:6;
A29: x = t.(len p + 1) by FINSEQ_1:42
.= -(b9.(len p)) + b.(len t) by A5,A26,A28,A27,A14;
m <= len b by A4,CALCUL_1:6;
then
A30: len b9 = len p by FINSEQ_1:59;
m <= len a by A3,CALCUL_1:6;
then len a9 = len p by FINSEQ_1:59;
then Sum p = a9.1 + b9.(len p) by A2,A12,A30,A20,A15;
hence thesis by A7,A13,A29;
end;
end;
A31: P[<*>COMPLEX];
A32: for p being FinSequence of COMPLEX holds P[p] from FINSEQ_2:sch 2(A31,A1);
let a,b,s be complex-valued FinSequence;
A33: a is FinSequence of COMPLEX & b is FinSequence of COMPLEX &
s is FinSequence of COMPLEX by FINSEQ_1:107;
assume 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));
hence thesis by A32,A33;
end;
theorem Th14:
for p,q,r being FinSequence holds
len (p ^ q ^ r) = (len p) + (len q) + (len r)
proof
let p,q,r be FinSequence;
thus len (p ^ q ^ r) = (len (p ^ q)) + (len r) by FINSEQ_1:22
.= ((len p) + (len q)) + (len r) by FINSEQ_1:22;
end;
theorem Th15:
for x being object, p,q being FinSequence holds (<*x*> ^ p ^ q).1 = x
proof
let x be object, p,q be FinSequence;
<*x*> ^ p ^ q = <*x*> ^ (p ^ q) by FINSEQ_1:32;
hence thesis by FINSEQ_1:41;
end;
theorem Th16:
for x being object, p,q being FinSequence holds
(p ^ q ^ <*x*>).((len p) + (len q) + 1) = x
proof
let x be object, p,q be FinSequence;
set s = p ^ q;
(s ^ <*x*>).((len s) + 1) = x by FINSEQ_1:42;
hence thesis by FINSEQ_1:22;
end;
theorem Th17:
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);
set n = k - (len p);
(len p) - (len p) = 0;
then
A3: 0 < n by A1,XREAL_1:9;
0 + 1 = 1;
then
A4: 1 <= n by A3,INT_1:7;
then reconsider n as Nat by Th2;
A5: ((len p) + (len q)) - (len p) = len q;
k <= (len p) + (len q) by A2,FINSEQ_1:22;
then n <= len q by A5,XREAL_1:9;
then n in Seg (len q) by A4;
then
A6: n in dom q by FINSEQ_1:def 3;
len (p ^ q) <= len (p ^ (q ^ r)) by Th9;
then k <= len (p ^ (q ^ r)) by A2,XXREAL_0:2;
then
A7: (p ^ (q ^ r)).k = (q ^ r).(k - (len p)) by A1,FINSEQ_1:24;
reconsider n as Element of NAT by ORDINAL1:def 12;
(q ^ r).n = q.n by A6,FINSEQ_1:def 7;
hence thesis by A7,FINSEQ_1:32;
end;
definition
let a be Integer;
redefine func <*a*> -> FinSequence of INT; :: redefines <* (FINSEQ_1, definition)
coherence
proof
set s = <*a*>;
a in INT by INT_1:def 2;
then rng s = {a} & {a} c= INT by FINSEQ_1:38,ZFMISC_1:31;
hence thesis by FINSEQ_1:def 4;
end;
end;
definition
let a,b be Integer;
redefine func <*a,b*> -> FinSequence of INT; :: redefines <* (FINSEQ_1, definition)
coherence
proof
set s = <*a,b*>;
a in INT & b in INT by INT_1:def 2;
then rng s = {a,b} & {a,b} c= INT by FINSEQ_2:127,ZFMISC_1:32;
hence thesis by FINSEQ_1:def 4;
end;
end;
definition
let a,b,c be Integer;
redefine func <*a,b,c*> -> FinSequence of INT; :: redefines <* (FINSEQ_1, definition)
coherence
proof
A1: c in INT by INT_1:def 2;
a in INT & b in INT by INT_1:def 2;
then rng <*a,b,c*> = {a,b,c} & {a,b,c} c= INT
by A1,FINSEQ_2:128,ZFMISC_1:133;
hence thesis by FINSEQ_1:def 4;
end;
end;
::$CT
theorem Th19:
for p,q,r being complex-valued FinSequence holds
Sum (p ^ q ^ r) = (Sum p) + (Sum q) + (Sum r)
proof
let p,q,r be complex-valued FinSequence;
thus Sum (p ^ q ^ r) = (Sum (p ^ q)) + (Sum r) by RVSUM_2:32
.= ((Sum p) + (Sum q)) + Sum r by RVSUM_2:32;
end;
theorem
for a being Element of Z_2 holds Sum <*a*> = a by FINSOP_1:11;
begin :: Polyhedra and Incidence Matrices
:: 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 Th21:
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;
rng f c= {1.Z_2} & {1.Z_2} c= {0.Z_2,1.Z_2} by FUNCOP_1:13,ZFMISC_1:7;
then dom f = [:X,Y:] & rng f c= {0.Z_2,1.Z_2};
hence thesis by 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
struct PolyhedronStr(# PolytopsF ->FinSequence-yielding FinSequence,
IncidenceF ->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;
attr p is polyhedron_1 means
len the IncidenceF of p = len(the PolytopsF of p) - 1;
attr p is polyhedron_2 means
:Def2:
for n being Nat st 1 <= n & 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));
attr p is polyhedron_3 means
:Def3:
for n being Nat st 1 <= n & n <= len the
PolytopsF of p holds (the PolytopsF of p).n is non empty & (the PolytopsF of p)
.n is one-to-one;
end;
registration
cluster polyhedron_1 polyhedron_2 polyhedron_3 for PolyhedronStr;
existence
proof
reconsider I = <*>{} as Function-yielding FinSequence;
reconsider F = <*<*{}*>*> as FinSequence-yielding FinSequence;
take p = PolyhedronStr(#F,I#);
A1: len F = 1 by FINSEQ_1:39;
thus p is polyhedron_1 by A1;
thus p is polyhedron_2 by A1;
let n be Nat;
assume 1 <= n & n <= len the PolytopsF of p;
then n = 1 by A1,XXREAL_0:1;
hence thesis;
end;
end;
definition
mode polyhedron is polyhedron_1 polyhedron_2 polyhedron_3 PolyhedronStr;
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 equals
len the PolytopsF of p;
coherence;
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
:Def5:
(k < -1 implies it = {}) & (k
= -1 implies it = {{}}) & (-1 < k & k < dim(p) implies it = rng ((the PolytopsF
of p).(k+1))) & (k = dim(p) implies it = {p}) & (k > dim(p) implies it = {});
existence
proof
set F = the PolytopsF of p;
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);
-1 + 1 = 0;
then 0 <= k by A3,INT_1:7;
then reconsider k as Element of NAT by INT_1:3;
set n = k + 1;
reconsider Fn = F.n as FinSequence;
take rng Fn;
thus thesis by A3;
end;
suppose
A4: k = dim(p);
take {p};
thus thesis by A4;
end;
suppose
A5: k > dim(p);
take {};
thus thesis by A5;
end;
end;
uniqueness
proof
set F = the PolytopsF of p;
let X,Y be finite set such that
A6: k < -1 implies X = {} and
A7: k = -1 implies X = {{}} and
A8: -1 < k & k < dim(p) implies X = rng (F.(k+1)) and
A9: k = dim(p) implies X = {p} and
A10: k > dim(p) implies X = {} and
A11: k < -1 implies Y = {} and
A12: k = -1 implies Y = {{}} and
A13: -1 < k & k < dim(p) implies Y = rng (F.(k+1)) and
A14: k = dim(p) implies Y = {p} and
A15: k > dim(p) implies Y = {};
per cases by XXREAL_0:1;
suppose
k < -1;
hence thesis by A6,A11;
end;
suppose
k = -1;
hence thesis by A7,A12;
end;
suppose
-1 < k & k < dim(p);
hence thesis by A8,A13;
end;
suppose
k = dim(p);
hence thesis by A9,A14;
end;
suppose
k > dim(p);
hence thesis by A10,A15;
end;
end;
end;
theorem Th22:
-1 < k & k < dim(p) implies k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim(p)
proof
A1: -1 + 1 = 0;
assume -1 < k;
then
A2: 0 < k + 1 by A1,XREAL_1:6;
then reconsider n = k + 1 as Element of NAT by INT_1:3;
A3: n is Nat & 0 + 1 = 1;
assume k < dim(p);
hence thesis by A2,A3,INT_1:7;
end;
theorem Th23:
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 Def5;
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 Def5;
end;
suppose
A3: -1 < k & k < dim(p);
set F = the PolytopsF of p;
A4: k-polytopes(p) = rng (F.(k+1)) by A3,Def5;
set n = k + 1;
A5: 1 <= n by A3,Th22;
A6: n <= dim(p) by A3,Th22;
reconsider n as Element of NAT by A5,INT_1:3;
reconsider n as Nat;
F.n is non empty by A5,A6,Def3;
hence thesis by A4;
end;
suppose
k = dim(p);
then k-polytopes(p) = {p} by Def5;
hence thesis;
end;
end;
end;
theorem
k < dim(p) implies 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, k be Integer;
func eta(p,k) -> incidence-matrix of (k-1)-polytopes(p),k-polytopes(p) means
:Def6:
(k < 0 implies it = {}) & (k = 0 implies it = [:{{}},0-polytopes(p):]
--> 1.Z_2) & (0 < k & k < dim(p) implies it = (the IncidenceF of p).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;
set f = {};
reconsider f as Function;
k - 1 < 0 - 1 by A1,XREAL_1:9;
then (k-1)-polytopes(p) = {} by Def5;
then [:(k-1)-polytopes(p),k-polytopes(p):] = {} by ZFMISC_1:90;
then reconsider
f as Function of [:(k-1)-polytopes(p),k-polytopes(p):],{0.Z_2
,1.Z_2} by RELSET_1:12;
reconsider f as Element of Funcs([:(k-1)-polytopes(p),k-polytopes(p):],{
0.Z_2,1.Z_2}) by FUNCT_2:8;
take f;
thus thesis by A1;
end;
suppose
A2: k > dim(p);
set f = {};
reconsider f as Function;
k-polytopes(p) = {} by A2,Th23;
then [:(k-1)-polytopes(p),k-polytopes(p):] = {} by ZFMISC_1:90;
then reconsider
f as Function of [:(k-1)-polytopes(p),k-polytopes(p):],{0.Z_2
,1.Z_2} by RELSET_1:12;
reconsider f as Element of Funcs([:(k-1)-polytopes(p),k-polytopes(p):],{
0.Z_2,1.Z_2}) by FUNCT_2:8;
take f;
thus thesis by A2;
end;
suppose
A3: 0 < k & k < dim(p);
set F = the PolytopsF of p, I = the IncidenceF of p;
A4: k-polytopes(p) = rng (F.(k+1)) by A3,Def5;
A5: k - 1 < dim(p) by A3,XREAL_1:146,XXREAL_0:2;
0 + 1 = 1;
then
A6: 1 <= k by A3,INT_1:7;
then reconsider k9 = k as Nat by Th2;
1 - 1 = 0;
then -1 < k - 1 by A6,XREAL_1:9;
then (k-1)-polytopes(p) = rng (F.((k-1)+1)) by A5,Def5;
then reconsider Ik = I.k9 as incidence-matrix of (k-1)-polytopes(p), k
-polytopes(p) by A3,A6,A4,Def2;
take Ik;
thus thesis by A3;
end;
suppose
A7: k = 0;
per cases;
suppose
A8: k = dim(p);
set f = [:{{}},{p}:] --> 1.Z_2;
reconsider f as incidence-matrix of {{}},{p} by Th21;
(k-1)-polytopes(p) = {{}} by A7,Def5;
then reconsider
f as incidence-matrix of (k-1)-polytopes(p), k-polytopes(p)
by A8,Def5;
take f;
thus thesis by A7,A8,Def5;
end;
suppose
A9: k <> dim(p);
set f = [:{{}},0-polytopes(p):] --> 1.Z_2;
reconsider f as incidence-matrix of {{}},0-polytopes(p) by Th21;
reconsider f as incidence-matrix of (k-1)-polytopes(p), k-polytopes(p)
by A7,Def5;
take f;
thus thesis by A7,A9;
end;
end;
suppose
A10: k = dim(p);
per cases;
suppose
A11: k = 0;
set f = [:{{}},{p}:] --> 1.Z_2;
reconsider f as incidence-matrix of {{}},{p} by Th21;
(k-1)-polytopes(p) = {{}} by A11,Def5;
then reconsider
f as incidence-matrix of (k-1)-polytopes(p), k-polytopes(p)
by A10,Def5;
take f;
thus thesis by A10,A11,Def5;
end;
suppose
A12: 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
Th21;
reconsider f as incidence-matrix of (k-1)-polytopes(p), k-polytopes(p)
by A10,Def5;
take f;
thus thesis by A10,A12;
end;
end;
end;
uniqueness
proof
set I = the IncidenceF of p;
let s,t be incidence-matrix of (k-1)-polytopes(p),k-polytopes(p) such that
A13: k < 0 implies s = {} and
A14: k = 0 implies s = [:{{}},0-polytopes(p):] --> 1.Z_2 and
A15: 0 < k & k < dim(p) implies s = I.k and
A16: k = dim(p) implies s = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1. Z_2 and
A17: k > dim(p) implies s = {} and
k < 0 implies t = {} and
A18: k = 0 implies t = [:{{}},0-polytopes(p):] --> 1.Z_2 and
A19: 0 < k & k < dim(p) implies t = I.k and
A20: k = dim(p) implies t = [:(dim(p) - 1)-polytopes(p),{p}:] --> 1. Z_2 and
k > dim(p) implies t = {};
per cases by XXREAL_0:1;
suppose
k < 0;
hence thesis by A13;
end;
suppose
k = 0;
hence thesis by A14,A18;
end;
suppose
0 < k & k < dim(p);
hence thesis by A15,A19;
end;
suppose
k = dim(p);
hence thesis by A16,A20;
end;
suppose
k > dim(p);
hence thesis by A17;
end;
end;
end;
definition
let p be polyhedron, k be Integer;
func k-polytope-seq(p) -> FinSequence means
:Def7:
(k < -1 implies it = <*>
{}) & (k = -1 implies it = <*{}*>) & (-1 < k & k < dim(p) implies it = (the
PolytopsF of p).(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);
set F = the PolytopsF of p;
take F.(k+1);
thus thesis by A3;
end;
suppose
A4: k = dim(p);
take <*p*>;
thus thesis by A4;
end;
suppose
A5: k > dim(p);
take <*>{};
thus thesis by A5;
end;
end;
uniqueness
proof
set F = the PolytopsF of p;
let s,t be FinSequence such that
A6: k < -1 implies s = <*>{} and
A7: k = -1 implies s = <*{}*> and
A8: -1 < k & k < dim(p) implies s = F.(k+1) and
A9: k = dim(p) implies s = <*p*> and
A10: k > dim(p) implies s = <*>{} and
A11: k < -1 implies t = <*>{} and
A12: k = -1 implies t = <*{}*> and
A13: -1 < k & k < dim(p) implies t = F.(k+1) and
A14: k = dim(p) implies t = <*p*> and
A15: k > dim(p) implies t = <*>{};
per cases by XXREAL_0:1;
suppose
k < -1;
hence thesis by A6,A11;
end;
suppose
k = -1;
hence thesis by A7,A12;
end;
suppose
-1 < k & k < dim(p);
hence thesis by A8,A13;
end;
suppose
k = dim(p);
hence thesis by A9,A14;
end;
suppose
k > dim(p);
hence thesis by A10,A15;
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 Th25:
dom (k-polytope-seq(p)) = Seg (num-polytopes(p,k))
proof
set F = the PolytopsF of p;
per cases;
suppose
k < -1;
then k-polytope-seq(p) = <*>{} & k-polytopes(p) = {} by Def5,Def7;
hence thesis by FINSEQ_1:def 3;
end;
suppose
A1: -1 <= k & k <= dim(p);
per cases by A1,XXREAL_0:1;
suppose
A2: k = -1;
then k-polytope-seq(p) = <*{}*> by Def7;
then
A3: len (k-polytope-seq(p)) = 1 by FINSEQ_1:39;
k-polytopes(p) = {{}} by A2,Def5;
then num-polytopes(p,k) = 1 by CARD_2:42;
hence thesis by A3,FINSEQ_1:def 3;
end;
suppose
A4: -1 < k & k < dim(p);
set n = k + 1;
reconsider n as Nat by A4,Th22;
reconsider Fn = F.n as FinSequence;
1 <= n & n <= dim(p) by A4,Th22;
then
A5: Fn is one-to-one by Def3;
k-polytopes(p) = rng (F.(k+1)) by A4,Def5;
then num-polytopes(p,k) = card (dom Fn) by A5,CARD_1:70;
then
A6: len Fn = num-polytopes(p,k) by CARD_1:62;
k-polytope-seq(p) = F.(k+1) by A4,Def7;
hence thesis by A6,FINSEQ_1:def 3;
end;
suppose
A7: k = dim(p);
then k-polytope-seq(p) = <*p*> by Def7;
then
A8: len (k-polytope-seq(p)) = 1 by FINSEQ_1:39;
k-polytopes(p) = {p} by A7,Def5;
then num-polytopes(p,k) = 1 by CARD_2:42;
hence thesis by A8,FINSEQ_1:def 3;
end;
end;
suppose
k > dim(p);
then k-polytope-seq(p) = <*>{} & k-polytopes(p) = {} by Def5,Def7;
hence thesis by FINSEQ_1:def 3;
end;
end;
theorem Th26:
len (k-polytope-seq(p)) = num-polytopes(p,k)
proof
dom (k-polytope-seq(p)) = Seg (num-polytopes(p,k)) by Th25;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th27:
rng (k-polytope-seq(p)) = k-polytopes(p)
proof
set F = the PolytopsF of p;
per cases;
suppose
A1: k < -1;
then k-polytopes(p) = {} by Def5;
hence thesis by A1,Def7,RELAT_1:38;
end;
suppose
A2: -1 <= k & k <= dim(p);
per cases by A2,XXREAL_0:1;
suppose
k = -1;
then k-polytopes(p) = {{}} & k-polytope-seq(p) = <*{}*> by Def5,Def7;
hence thesis by FINSEQ_1:38;
end;
suppose
A3: -1 < k & k < dim(p);
then k-polytopes(p) = rng (F.(k+1)) by Def5;
hence thesis by A3,Def7;
end;
suppose
k = dim(p);
then k-polytopes(p) = {p} & k-polytope-seq(p) = <*p*> by Def5,Def7;
hence thesis by FINSEQ_1:38;
end;
end;
suppose
A4: k > dim(p);
then k-polytopes(p) = {} by Def5;
hence thesis by A4,Def7,RELAT_1:38;
end;
end;
theorem Th28:
num-polytopes(p,-1) = 1
proof
reconsider minusone = -1 as Integer;
minusone-polytopes(p) = {{}} by Def5;
hence thesis by CARD_1:30;
end;
theorem Th29:
num-polytopes(p,dim(p)) = 1
proof
dim(p)-polytopes(p) = {p} by Def5;
hence thesis by CARD_1:30;
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);
func n-th-polytope(p,k) -> Element of k-polytopes(p) equals
:Def12:
(k-polytope-seq(p)).n;
coherence
proof
n in Seg num-polytopes(p,k) by A1;
then n in dom (k-polytope-seq(p)) by Th25;
then (k-polytope-seq(p)).n in rng (k-polytope-seq(p)) by FUNCT_1:3;
hence thesis by Th27;
end;
end;
theorem Th30:
-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;
reconsider n = 1 as Nat;
k-polytope-seq(p) = <*{}*> by A2,Def7;
then
A3: (k-polytope-seq(p)).n = {};
take n;
k-polytopes(p) = {{}} by A2,Def5;
then x = {} & n <= num-polytopes(p,k) by CARD_1:30,TARSKI:def 1;
hence thesis by A3,Def12;
end;
suppose
A4: k = dim(p);
reconsider n = 1 as Nat;
k-polytope-seq(p) = <*p*> by A4,Def7;
then
A5: (k-polytope-seq(p)).n = p;
take n;
k-polytopes(p) = {p} by A4,Def5;
then x = p & num-polytopes(p,k) = 1 by CARD_1:30,TARSKI:def 1;
hence thesis by A5,Def12;
end;
suppose
A6: -1 < k & k < dim(p);
set F = the PolytopsF of p;
A7: k-polytopes(p) = rng (F.(k+1)) by A6,Def5;
A8: -1 + 1 < k + 1 by A6,XREAL_1:6;
then
A9: 0 + 1 <= k + 1 by INT_1:7;
reconsider k9 = k + 1 as Element of NAT by A8,INT_1:3;
k + 1 <= dim(p) by A6,INT_1:7;
then F.k9 is non empty by A9,Def3;
then consider m being object such that
A10: m in dom (F.k9) and
A11: (F.k9).m = x by A7,FUNCT_1:def 3;
reconsider Fk9 = F.k9 as FinSequence;
reconsider m as Element of NAT by A10;
dom Fk9 = Seg (len Fk9) by FINSEQ_1:def 3;
then
A12: 1 <= m & m <= len Fk9 by A10,FINSEQ_1:1;
take m;
A13: k-polytope-seq(p) = F.(k+1) by A6,Def7;
then num-polytopes(p,k) = len (F.(k+1)) by Th26;
hence thesis by A13,A11,A12,Def12;
end;
end;
theorem Th31:
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 Def7;
end;
suppose
k = -1;
hence thesis by Def7;
end;
suppose
A1: -1 < k & k < dim(p);
then
A2: -1 + 1 < k + 1 by XREAL_1:6;
then reconsider m = k + 1 as Element of NAT by INT_1:3;
set F = the PolytopsF of p;
A3: 0 + 1 <= m by A2,INT_1:7;
s = F.(k+1) & m <= dim(p) by A1,Def7,INT_1:7;
hence thesis by A3,Def3;
end;
suppose
k = dim(p);
then s = <*p*> by Def7;
hence thesis;
end;
suppose
k > dim(p);
hence thesis by Def7;
end;
end;
theorem Th32:
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
let m,n be Nat such that
A1: 1 <= n & n <= num-polytopes(p,k) and
A2: 1 <= m & m <= num-polytopes(p,k) and
A3: n-th-polytope(p,k) = m-th-polytope(p,k);
set s = k-polytope-seq(p);
A4: s is one-to-one by Th31;
m in Seg (num-polytopes(p,k)) by A2;
then
A5: m in dom s by Th25;
n in Seg (num-polytopes(p,k)) by A1;
then
A6: n in dom s by Th25;
n-th-polytope(p,k) = s.n & m-th-polytope(p,k) = s.m by A1,A2,Def12;
hence thesis by A3,A6,A5,A4,FUNCT_1:def 4;
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 that
A1: 0 <= k and
A2: k <= dim(p);
func incidence-value(x,y) -> Element of Z_2 equals
:Def13:
eta(p,k).(x,y);
coherence
proof
set n = eta(p,k);
A3: (k-1)-polytopes(p) <> {}
proof
set m = k - 1;
0 - 1 = -1;
then
A4: -1 <= m by A1,XREAL_1:9;
m <= dim(p) - 0 by A2,XREAL_1:13;
hence thesis by A4,Th23;
end;
dom n = [:(k-1)-polytopes(p),k-polytopes(p):] & k-polytopes(p) <> {}
by A1,A2,Th23,FUNCT_2:92;
then [x,y] in dom n by A3,ZFMISC_1:87;
then n.[x,y] in rng n by FUNCT_1:3;
hence thesis by BSPACE:3,5,6;
end;
end;
begin :: The Chain Spaces and their Subspaces. Boundary of a k-chain.
:: 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 Th34:
num-polytopes(p,k) = dim (k-chain-space(p))
proof
set n = dim (k-chain-space(p));
singletons(k-polytopes(p)) is Basis of k-chain-space(p) by BSPACE:40;
then n = card (singletons(k-polytopes(p))) by VECTSP_9:def 1;
hence thesis by BSPACE:41;
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
:Def16:
((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 = <*>{};
rng s c= the carrier of Z_2;
then reconsider s as FinSequence of Z_2 by FINSEQ_1:def 4;
take s;
thus thesis by A1;
end;
suppose
A2: (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
A3: len s = num-polytopes(p,k) and
A4: for n being Nat st n in dom s holds s.n = F(n) from FINSEQ_2:sch
1;
take s;
A5: dom s = Seg num-polytopes(p,k) by A3,FINSEQ_1:def 3;
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;
assume 1 <= n & n <= num-polytopes(p,k);
then n in Seg num-polytopes(p,k);
hence thesis by A4,A5;
end;
hence thesis by A2,A3;
end;
end;
uniqueness
proof
let s,t be FinSequence of Z_2 such that
A6: (k-1)-polytopes(p) is empty implies s = <*>{} and
A7: (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
A8: (k-1)-polytopes(p) is empty implies t = <*>{} and
A9: (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 A6,A8;
end;
suppose
A10: (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
A11: 1 <= n & n <= len s;
reconsider n as Nat;
s.n = (v@(n-th-polytope(p,k)))*incidence-value(x,n-th-polytope(p,
k)) by A7,A10,A11;
hence thesis by A7,A9,A10,A11;
end;
hence thesis by A7,A9,A10;
end;
end;
end;
theorem Th35:
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 Th36:
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;
then isd is Tuple of 0, the carrier of Z_2 by Def16;
then reconsider isd as Element of 0-tuples_on the carrier of Z_2 by
FINSEQ_2:131;
isc = <*>(the carrier of Z_2) by A1,Def16;
then reconsider isc as Element of 0-tuples_on the carrier of Z_2 by
FINSEQ_2:131;
isc + isd is Element of 0-tuples_on the carrier of Z_2;
hence thesis by A1,Def16;
end;
suppose
A2: (k-1)-polytopes(p) is non empty;
A3: len(l) = n & len(r) = n
proof
len isd = n by A2,Def16;
then reconsider isd as Element of n-tuples_on the carrier of Z_2 by
FINSEQ_2:92;
len isc = n by A2,Def16;
then reconsider isc as Element of n-tuples_on the carrier of Z_2 by
FINSEQ_2:92;
reconsider s = isc + isd as Element of n-tuples_on the carrier of Z_2;
len s = n by CARD_1:def 7;
hence thesis by A2,Def16;
end;
for n being Nat st 1 <= n & n <= len l holds l.n = r.n
proof
A4: dom r = Seg n & len l = n by A3,FINSEQ_1:def 3;
let m be Nat such that
A5: 1 <= m & m <= len l;
set a = m-th-polytope(p,k);
set iva = incidence-value(x,a);
A6: len l = n by A2,Def16;
then
A7: l.m = ((c+d)@a)*iva by A2,A5,Def16;
A8: m in dom r by A4,A5;
isc.m = (c@a)*iva & isd.m = (d@a)*iva by A2,A5,A6,Def16;
then r.m = (c@a)*iva + (d@a)*iva by A8,FVSUM_1:17
.= (c@a + d@a)*iva by VECTSP_1:def 3
.= l.m by A7,Th35;
hence thesis;
end;
hence thesis by A3;
end;
end;
theorem Th37:
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;
then isd = <*>(the carrier of Z_2) by Def16;
then reconsider isd as Element of 0-tuples_on the carrier of Z_2 by
FINSEQ_2:131;
isc = <*>(the carrier of Z_2) by A1,Def16;
then reconsider isc as Element of 0-tuples_on the carrier of Z_2 by
FINSEQ_2:131;
reconsider s = isc + isd as Element of 0-tuples_on the carrier of Z_2;
Sum s = 0.Z_2 by FVSUM_1:74;
hence thesis by RLVECT_1:def 4;
end;
suppose
A2: (k-1)-polytopes(p) is non empty;
reconsider n = num-polytopes(p,k) as Element of NAT;
len isd = n by A2,Def16;
then reconsider
isd9 = isd as Element of n-tuples_on the carrier of Z_2 by FINSEQ_2:92;
len isc = n by A2,Def16;
then reconsider
isc9 = isc as Element of n-tuples_on the carrier of Z_2 by FINSEQ_2:92;
Sum (isc + isd) = Sum (isc9 + isd9) .= Sum (isc) + Sum (isd) by FVSUM_1:76;
hence thesis;
end;
end;
theorem Th38:
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 Th36
.= (Sum incidence-sequence(x,c)) + (Sum incidence-sequence(x,d)) by Th37;
hence thesis;
end;
theorem Th39:
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
a = 0.Z_2;
then a*(c@x) = 0.Z_2 & a*c = 0.(k-chain-space(p)) by VECTSP_1:14;
hence thesis by BSPACE:14;
end;
suppose
a = 1.Z_2;
hence thesis;
end;
end;
theorem Th40:
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;
then isc = <*>(the carrier of Z_2) by Def16;
then reconsider isc as Element of 0-tuples_on the carrier of Z_2 by
FINSEQ_2:131;
a*isc is Element of 0-tuples_on the carrier of Z_2;
then reconsider r as Element of 0-tuples_on the carrier of Z_2;
r = <*>(the carrier of Z_2);
hence thesis by A1,Def16;
end;
suppose
A2: (k-1)-polytopes(p) is non empty;
set n = num-polytopes(p,k);
A3: len l = n & len r = n
proof
len isc = n by A2,Def16;
then reconsider isc as Element of n-tuples_on the carrier of Z_2 by
FINSEQ_2:92;
set r = a*isc;
reconsider r as Element of n-tuples_on the carrier of Z_2;
len r = n by CARD_1:def 7;
hence thesis by A2,Def16;
end;
for m being Nat st 1 <= m & m <= len l holds l.m = r.m
proof
A4: dom r = Seg n by A3,FINSEQ_1:def 3;
let m be Nat such that
A5: 1 <= m & m <= len l;
set s = m-th-polytope(p,k);
set ivs = incidence-value(x,s);
A6: len l = n by A2,Def16;
then
A7: l.m = ((a*c)@s)*ivs by A2,A5,Def16;
len l = n & m in NAT by A2,Def16,ORDINAL1:def 12;
then
A8: m in Seg n by A5;
isc.m = (c@s)*ivs by A2,A5,A6,Def16;
then r.m = a*((c@s)*ivs) by A4,A8,FVSUM_1:50
.= (a*(c@s))*ivs by GROUP_1:def 3
.= l.m by A7,Th39;
hence thesis;
end;
hence thesis by A3;
end;
end;
theorem Th41:
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 object such that
A2: x in c;
reconsider x as Element of k-polytopes(p) by A2;
reconsider c as Subset of k-polytopes(p);
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 object such that
A3: x in d;
reconsider x as Element of k-polytopes(p) by A3;
reconsider d as Subset of k-polytopes(p);
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 Th42:
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 c <> d;
then consider x being Element of k-polytopes(p) such that
A2: c@x <> d@x by Th41;
not (x in c iff x in d) by A2,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 object;
assume x in c;
then ex y being Element of k()-polytopes(p()) st x = y &( P[y] )& y in k()
-polytopes(p());
hence thesis;
end;
then reconsider c as Subset of k()-polytopes(p());
take c;
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
ex y being Element of k()-polytopes(p()) st y = x &( P[y] )& y in k()
-polytopes(p());
hence thesis;
end;
thus thesis;
end;
hence thesis;
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
:Def17:
((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
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
A1: 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 A1;
end;
uniqueness
proof
let c,d be Element of (k-1)-chain-space(p) such that
A2: (k-1)-polytopes(p) is empty implies c = 0.((k-1)-chain-space(p)) and
A3: (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
(k-1)-polytopes(p) is empty implies d = 0.((k-1)-chain-space(p)) and
A4: (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 A2;
end;
suppose
A5: (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 A3;
hence thesis by A4,A5;
end;
thus x in d implies x in c
proof
assume x in d;
then Sum incidence-sequence(x,v) = 1.Z_2 by A4;
hence thesis by A3,A5;
end;
end;
hence thesis by Th42;
end;
end;
end;
theorem Th43:
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;
set iscx = incidence-sequence(x,c);
iscx = <*>(the carrier of Z_2) by A1,Def16;
then
A2: Sum iscx = 0.Z_2 by RLVECT_1:43;
Boundary(c) = 0.((k-1)-chain-space(p)) by A1;
hence thesis by A2,BSPACE:14;
end;
suppose
A3: (k-1)-polytopes(p) is non empty;
then
A4: x in b iff Sum incidence-sequence(x,c) = 1.Z_2 by Def17;
per cases;
suppose
x in b;
hence thesis by A4,BSPACE:def 3;
end;
suppose
A5: not x in b;
then Sum incidence-sequence(x,c) <> 1.Z_2 by A3,Def17;
then Sum incidence-sequence(x,c) = 0.Z_2 by BSPACE:8;
hence thesis by A5,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
:Def18:
for c being Element of k-chain-space(p) holds it.c = Boundary(c);
existence
proof
defpred Q[object,object] means
ex c being Element of k-chain-space(p) st $1 = c
& $2 = Boundary(c);
A1: for x being object st x in k-chains(p) ex y being object st y in (k-1)
-chains(p) & Q[x,y]
proof
let x be object;
assume x in k-chains(p);
then reconsider x as Element of k-chain-space(p);
set b = Boundary(x);
take b;
thus thesis;
end;
consider f being Function of k-chains(p), (k-1)-chains(p) such that
A2: for x being object 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);
take f;
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 A2;
hence thesis;
end;
hence thesis;
end;
uniqueness
proof
let f,g be Function of k-chain-space(p),(k-1)-chain-space(p) such that
A3: for c being Element of k-chain-space(p) holds f.c = Boundary(c) and
A4: for c being Element of k-chain-space(p) holds g.c = Boundary(c);
A5: for x being object st x in dom f holds f.x = g.x
proof
let x be object;
assume x in dom f;
then reconsider x as Element of k-chain-space(p);
f.x = Boundary(x) by A3;
hence thesis by A4;
end;
dom f = [#](k-chain-space(p)) by FUNCT_2:def 1;
then dom f = dom g by FUNCT_2:def 1;
hence thesis by A5,FUNCT_1:2;
end;
end;
theorem Th44:
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);
set a = bc@x;
set b = bd@x;
A1: a = Sum incidence-sequence(x,c) & b = Sum incidence-sequence(x,d) by Th43;
l@x = Sum incidence-sequence(x,s) & r@x = a+b by Th35,Th43;
hence thesis by A1,Th38;
end;
hence thesis by Th41;
end;
theorem Th45:
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);
set b = rb@x;
A1: l@x = Sum incidence-sequence(x,lsm) & rb@x = Sum incidence-sequence(x,
c) by Th43;
r@x = a*b & incidence-sequence(x,lsm) = a*incidence-sequence(x,c) by Th39
,Th40;
hence thesis by A1,FVSUM_1:73;
end;
hence thesis by Th41;
end;
:: As defined, the k-boundary operator gives rise to a linear
:: transformation.
theorem Th46:
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 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 Def18
.= a*(Boundary(x)) by Th45
.= a*(b.x) by Def18;
hence thesis;
end;
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 Def18
.= Boundary(x) + Boundary(y) by Th44
.= (b.x) + Boundary(y) by Def18
.= (b.x) + (b.y) by Def18;
hence thesis;
end;
then b is additive homogeneous by A1,MOD_2:def 2,VECTSP_1:def 20;
hence thesis;
end;
registration
let p be polyhedron, k be Integer;
cluster k-boundary(p) -> homogeneous additive;
coherence by Th46;
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;
begin :: Simply Connected and Eulerian Polyhedra
:: 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
for k being Integer holds k -circuits(p) = k-bounding-chains(p);
end;
theorem Th48:
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;
hence thesis by VECTSP_4:29;
end;
thus Q[p] implies p is simply-connected;
end;
definition
let p be polyhedron;
func alternating-f-vector(p) -> FinSequence of INT means
:Def26:
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) = In((-1)|^$1*num-polytopes(p,$1-2),INT);
consider s being FinSequence of INT such that
A1: len s = dim(p) + 2 and
A2: for j being Nat st j in dom s holds s.j = F(j) from FINSEQ_2:sch 1;
take s;
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;
assume 1 <= j & j <= dim(p) + 2;
then j in dom s by A1,FINSEQ_3:25;
then s.j = F(j) by A2;
hence thesis;
end;
hence thesis by A1;
end;
uniqueness
proof
let s,t be FinSequence of INT such that
A3: len(s) = dim(p) + 2 and
A4: for k being Nat st 1 <= k & k <= dim(p) + 2 holds s.k = ((-1)|^k)*
num-polytopes(p,k-2) and
A5: len(t) = dim(p) + 2 and
A6: 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
A7: 1 <= k & k <= len s;
reconsider k as Nat;
s.k = ((-1)|^k)*num-polytopes(p,k-2) by A3,A4,A7;
hence thesis by A3,A6,A7;
end;
hence thesis by A3,A5;
end;
end;
definition
let p be polyhedron;
func alternating-proper-f-vector(p) -> FinSequence of INT means
:Def27:
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) = In(((-1)|^($1+1))*num-polytopes(p,$1-1),INT);
consider s being FinSequence of INT such that
A1: len s = dim(p) and
A2: for j being Nat st j in dom s holds s.j = F(j) from FINSEQ_2:sch 1;
take s;
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;
assume 1 <= j & j <= dim(p);
then j in dom s by A1,FINSEQ_3:25;
then s.j = F(j) by A2;
hence thesis;
end;
hence thesis by A1;
end;
uniqueness
proof
let s,t be FinSequence of INT such that
A3: len(s) = dim(p) and
A4: for k being Nat st 1 <= k & k <= dim(p) holds s.k = ((-1)|^(k+1))*
num-polytopes(p,k-1) and
A5: len(t) = dim(p) and
A6: 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
A7: 1 <= k & k <= len s;
reconsider k as Nat;
s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) by A3,A4,A7;
hence thesis by A3,A6,A7;
end;
hence thesis by A3,A5;
end;
end;
definition
let p be polyhedron;
func alternating-semi-proper-f-vector(p) -> FinSequence of INT means
:Def28:
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) = In(((-1)|^($1+1))*num-polytopes(p,$1-1),INT);
consider s being FinSequence of INT such that
A1: len s = dim(p) + 1 and
A2: for j being Nat st j in dom s holds s.j = F(j) from FINSEQ_2:sch 1;
take s;
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;
assume 1 <= j & j <= dim(p) + 1;
then j in dom s by A1,FINSEQ_3:25;
then s.j = F(j) by A2;
hence thesis;
end;
hence thesis by A1;
end;
uniqueness
proof
let s,t be FinSequence of INT such that
A3: len(s) = dim(p) + 1 and
A4: for k being Nat st 1 <= k & k <= dim(p) + 1 holds s.k = ((-1)|^(k+
1))*num-polytopes(p,k-1) and
A5: len(t) = dim(p) + 1 and
A6: 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
A7: 1 <= k & k <= len s;
reconsider k as Nat;
s.k = ((-1)|^(k+1))*num-polytopes(p,k-1) by A3,A4,A7;
hence thesis by A3,A6,A7;
end;
hence thesis by A3,A5;
end;
end;
theorem Th49:
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;
set a = (-1)|^(n+1);
assume n <= len apcs;
then n <= dim(p) by Def27;
then apcs.n = a*num-polytopes(p,n-1) by A1,Def27
.= a*(dim ((n-1)-chain-space(p))) by Th34
.= 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
Sum (alternating-proper-f-vector(p)) = 1 + (-1)|^(dim(p)+1);
end;
theorem Th50:
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 Def28;
A2: for n being Nat st 1 <= n & n <= len aspcs holds aspcs.n = r.n
proof
let n be Nat such that
A3: 1 <= n and
A4: n <= len aspcs;
per cases by A1,A4,NAT_1:8;
suppose
A5: n <= d;
len apcs = d & dom apcs = Seg (len apcs) by Def27,FINSEQ_1:def 3;
then n in dom apcs by A3,A5;
then r.n = apcs.n by FINSEQ_1:def 7
.= ((-1)|^(n+1))*num-polytopes(p,n-1) by A3,A5,Def27;
hence thesis by A1,A3,A4,Def28;
end;
suppose
A6: n = d + 1;
then n = (len apcs) + 1 by Def27;
then
A7: r.n = (-1)|^d by FINSEQ_1:42
.= (-1)|^(d+2) by Th12;
aspcs.n = ((-1)|^(n+1))*num-polytopes(p,n-1) by A3,A6,Def28
.= ((-1)|^(n+1))*1 by A6,Th29
.= (-1)|^(n+1);
hence thesis by A6,A7;
end;
end;
len r = (len apcs) + (len <*(-1)|^(dim(p))*>) by FINSEQ_1:22
.= d + (len <*(-1)|^(dim(p))*>) by Def27
.= d + 1 by FINSEQ_1:40;
then len aspcs = len r by Def28;
hence thesis by A2;
end;
:: Another characterization of Eulerian polyhedra
definition
let p be polyhedron;
redefine attr p is eulerian means :: redefines eulerian (POLYFORM, definition)
Sum ( alternating-semi-proper-f-vector(p)) = 1;
compatibility
proof
set aspcs = alternating-semi-proper-f-vector(p);
set apcs = alternating-proper-f-vector(p);
aspcs = apcs ^ <*(-1)|^(dim(p))*> by Th50;
then
A1: Sum aspcs = (Sum apcs) + (-1)|^(dim(p)) by RVSUM_1:74;
A2: Sum aspcs = 1 implies p is eulerian
proof
assume Sum aspcs = 1;
then Sum apcs = 1 + (-1)*((-1)|^(dim(p))) by A1
.= 1 + (-1)|^(dim(p)+1) by NEWTON:6;
hence thesis;
end;
p is eulerian implies Sum aspcs = 1
proof
assume p is eulerian;
then Sum aspcs = 1 + (-1)|^(dim(p)+1) + (-1)|^(dim(p)) by A1
.= 1 + (-1)*((-1)|^(dim(p))) + (-1)|^(dim(p)) by NEWTON:6
.= 1;
hence thesis;
end;
hence thesis by A2;
end;
end;
theorem Th51:
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:22
.= (len <*-1*>) + (d + 1) by Def28
.= 1 + (d + 1) by FINSEQ_1:40
.= d + 2;
A2: 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,Def26;
per cases by A3,XXREAL_0:1;
suppose
A6: n = 1;
then acs.n = ((-1)|^1)*num-polytopes(p,1-2) by A5,Def26
.= (-1)*num-polytopes(p,-1)
.= (-1)*1 by Th28
.= -1;
hence thesis by A6,FINSEQ_1:41;
end;
suppose
A7: n > 1;
then
A8: 1 - 1 < n - 1 by XREAL_1:9;
then reconsider m = n - 1 as Element of NAT by INT_1:3;
n - 1 <= (d + 2) - 1 by A5,XREAL_1:9;
then
A9: m <= d + 1;
len <*-1*> = 1 by FINSEQ_1:39;
then
A10: r.n = aspcs.(n-1) by A1,A5,A7,FINSEQ_1:24;
0 < 0 + m by A8;
then 1 <= m by NAT_1:19;
then aspcs.m = ((-1)|^(m+1))*num-polytopes(p,m-1) by A9,Def28
.= ((-1)|^n)*(num-polytopes(p,n-2));
hence thesis by A3,A5,A10,Def26;
end;
end;
len acs = len r by A1,Def26;
hence thesis by A2;
end;
:: Yet another characterization of eulerian polyhedra
definition
let p be polyhedron;
redefine attr p is eulerian means :: redefines eulerian (POLYFORM, redefinition) → eulerian (POLYFORM, definition)
Sum (alternating-f-vector(p)) = 0;
compatibility
proof
set aspcs = alternating-semi-proper-f-vector(p);
set acs = alternating-f-vector(p);
acs = <*-1*> ^ aspcs by Th51;
then
A1: Sum acs = -1 + (Sum aspcs) by RVSUM_2:33;
thus thesis by A1;
end;
end;
begin :: The Extremal Chain Spaces
theorem Th52:
0-polytopes(p) is non empty
proof
set d = dim(p);
per cases;
suppose
d = 0;
then 0-polytopes(p) = {p} by Def5;
hence thesis;
end;
suppose
d > 0;
hence thesis by Th23;
end;
end;
theorem Th53:
card [#]((-1)-chain-space(p)) = 2
proof
(-1)-polytopes(p) = {{}} by Def5;
then card ((-1)-polytopes(p)) = 1 by CARD_1:30;
then card [#]((-1)-chain-space(p)) = exp(2,1) by BSPACE:42
.= 2 by CARD_2:27;
hence thesis;
end;
theorem Th54:
[#]((-1)-chain-space(p)) = { {}, {{}} }
proof
(-1)-polytopes(p) = {{}} by Def5;
hence thesis by ZFMISC_1:24;
end;
theorem Th55:
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: eta(p,k) = [:{{}},0-polytopes(p):] --> 1.Z_2 by A1,Def6;
A4: k <= dim(p) by A1;
then {} in {{}} & 0-polytopes(p) is non empty by Th23,TARSKI:def 1;
then
A5: [{},x] in [:{{}},0-polytopes(p):] by A1,ZFMISC_1:87;
incidence-value(e,x) = eta(p,k).(e,x) by A1,A4,Def13
.= 1.Z_2 by A2,A3,A5,FUNCOP_1:7;
hence thesis;
end;
theorem Th56:
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) & 1 <= n & n <= num-polytopes(p,k);
set iseq = incidence-sequence(e,v);
A5: x in v by A2,TARSKI:def 1;
(k-1)-polytopes(p) is non empty by A1,Def5;
then iseq.n = (v@x)*incidence-value(e,x) by A4,Def16
.= (1.Z_2)*incidence-value(e,x) by A5,BSPACE:def 3
.= (1.Z_2)*(1.Z_2) by A1,A3,Th55
.= 1.Z_2;
hence thesis;
end;
theorem Th57:
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 & m <= num-polytopes(p,k) and
A5: 1 <= n & n <= num-polytopes(p,k) & m <> n;
A6: m-th-polytope(p,k) <> x by A3,A4,A5,Th32;
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 A6,TARSKI:def 1;
end;
then
A7: v@(m-th-polytope(p,k)) = 0.Z_2 by BSPACE:11;
set iseq = incidence-sequence(e,v);
(k-1)-polytopes(p) is non empty by A1,Def5;
then iseq.m = (0.Z_2)*(incidence-value(e,m-th-polytope(p,k))) by A4,A7,Def16
.= 0.Z_2;
hence thesis;
end;
theorem Th58:
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);
k <= dim(p) by A1;
then consider n being Nat such that
A4: x = n-th-polytope(p,k) and
A5: 1 <= n & n <= num-polytopes(p,k) by A1,Th30;
(k-1)-polytopes(p) is non empty by A1,Def5;
then
A6: len iseq = num-polytopes(p,k) by Def16;
A7: for m being Nat st m in dom iseq & m <> n holds iseq.m = 0.Z_2
proof
let m be Nat such that
A8: m in dom iseq and
A9: m <> n;
m in Seg (len iseq) by A8,FINSEQ_1:def 3;
then 1 <= m & m <= len iseq by FINSEQ_1:1;
hence thesis by A1,A2,A4,A5,A6,A9,Th57;
end;
dom iseq = Seg (len iseq) by FINSEQ_1:def 3;
then
A10: n in dom iseq by A5,A6;
iseq.n = 1.Z_2 by A1,A2,A3,A4,A5,Th56;
hence thesis by A10,A7,MATRIX_3:12;
end;
theorem Th59:
for x being Element of 0-polytopes(p) holds (0-boundary(p)).({x} ) = {{}}
proof
reconsider minusone = 0-1 as Integer;
let x be Element of 0-polytopes(p);
set T = 0-boundary(p);
0-polytopes(p) is non empty by Th52;
then reconsider v = {x} as Subset of 0-polytopes(p) by ZFMISC_1:31;
(0-1)-polytopes(p) = {{}} by Def5;
then reconsider null = {} as Element of (0-1)-polytopes(p)
by TARSKI:def 1;
reconsider v as Element of 0-chain-space(p);
reconsider bv = Boundary(v) as Element of minusone-chain-space(p);
A1: bv c= {null}
proof
A2: [#](minusone-chain-space(p)) = { {}, {{}} } by Th54;
let y be object such that
A3: y in bv;
per cases by A2,TARSKI:def 2;
suppose
bv = {};
hence thesis by A3;
end;
suppose
bv = {{}};
hence thesis by A3;
end;
end;
minusone-polytopes(p) is non empty by Def5;
then null in bv iff Sum incidence-sequence(null,v) = 1.Z_2 by Def17;
then
A4: {null} c= bv by Th58,ZFMISC_1:31;
T.v = Boundary(v) by Def18;
hence thesis by A4,A1;
end;
theorem Th60:
k = -1 implies dim(k-bounding-chain-space(p)) = 1
proof
set T = 0-boundary(p);
set V = k-bounding-chain-space(p);
assume
A1: k = -1;
card [#]V = 2
proof
[#]V c= [#](k-chain-space(p)) by VECTSP_4:def 2;
then card [#]V c= card [#](k-chain-space(p)) by CARD_1:11;
then
A2: card [#]V c= 2 by A1,Th53;
0-polytopes(p) <> {} by Th52;
then consider x being object such that
A3: x in 0-polytopes(p) by XBOOLE_0:def 1;
reconsider x as Element of 0-polytopes(p) by A3;
set v = {x};
A4: T.v = {{}} by Th59;
reconsider v as Subset of 0-polytopes(p) by A3,ZFMISC_1:31;
reconsider v as Element of 0-chain-space(p);
A5: dom T = [#](0-chain-space(p)) by RANKNULL:7;
then v in dom T;
then
A6: {{}} in rng T by A4,FUNCT_1:3;
T.(0.(0-chain-space(p))) = 0.(k-chain-space(p)) by A1,RANKNULL:9
.= {};
then {} in rng T by A5,FUNCT_1:3;
then
A7: {{},{{}}} c= rng T by A6,ZFMISC_1:32;
card {{},{{}}} = 2 by CARD_2:57;
then
A8: 2 c= card rng T by A7,CARD_1:11;
card rng T = card (T .: [#](0-chain-space(p))) by RELSET_1:22
.= card [#]V by A1,RANKNULL:def 2;
hence thesis by A8,A2;
end;
hence thesis by RANKNULL:6;
end;
theorem Th61:
card [#](dim(p)-chain-space(p)) = 2
proof
dim(p)-polytopes(p) = {p} by Def5;
then card (dim(p)-polytopes(p)) = 1 by CARD_1:30;
then card [#]((dim(p))-chain-space(p)) = exp(2,1) by BSPACE:42
.= 2 by CARD_2:27;
hence thesis;
end;
theorem Th62:
{p} is Element of dim(p)-chain-space(p)
proof
dim(p)-polytopes(p) = {p} by Def5;
hence thesis;
end;
theorem Th63:
{p} in [#](dim(p)-chain-space(p))
proof
{p} is Element of dim(p)-chain-space(p) by Th62;
hence thesis;
end;
theorem Th64:
(dim(p) - 1)-polytopes(p) is non empty
proof
set n = dim(p) - 1;
0 - 1 = -1;
then
A1: -1 <= n by XREAL_1:9;
n <= dim(p) by XREAL_1:146;
hence thesis by A1,Th23;
end;
registration
let p be polyhedron;
cluster (dim(p)-1)-polytopes(p) -> non empty;
coherence by Th64;
end;
theorem Th65:
[#](dim(p)-chain-space(p)) = { 0.(dim(p)-chain-space(p)), {p} }
proof
set V = dim(p)-chain-space(p);
set C = [#]V;
A1: card C = 2 by Th61;
reconsider C as finite set;
A2: {p} in C by Th63;
ex a,b being object st a <> b & C = {a,b} by A1,CARD_2:60;
hence thesis by A2,Th1;
end;
theorem Th66:
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;
x in [#]V;
then x in { 0.V, {p} } by Th65;
hence thesis by TARSKI:def 2;
end;
theorem Th67:
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 x <> 0.V;
then
A2: x = {p} by Th66;
assume y <> 0.V;
hence contradiction by A1,A2,Th66;
end;
theorem
dim(p)-polytope-seq(p) = <*p*> by Def7;
theorem Th69:
1-th-polytope(p,dim(p)) = p
proof
reconsider egy = 1 as Nat;
set s = dim(p)-polytope-seq(p);
A1: s = <*p*> by Def7;
egy <= num-polytopes(p,dim(p)) by Th29;
then egy-th-polytope(p,dim(p)) = s.egy by Def12
.= p by A1;
hence thesis;
end;
theorem Th70:
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
A1: dim(p)-polytopes(p) = {p} by Def5;
let c be Element of dim(p)-chain-space(p), x be Element of dim(p)-polytopes(
p);
assume c = {p};
hence thesis by A1,BSPACE:def 3;
end;
theorem Th71:
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
set f = [:(dim(p)-1)-polytopes(p),{p}:] --> 1.Z_2;
let x be Element of (dim(p)-1)-polytopes(p), c be Element of dim(p)
-polytopes(p);
assume c = p;
then dom f = [:(dim(p)-1)-polytopes(p),{p}:] & c in {p} by TARSKI:def 1;
then [x,c] in dom f by ZFMISC_1:87;
then f.(x,c) in rng f by FUNCT_1:3;
then f.(x,c) in {1.Z_2} by FUNCOP_1:8;
then
A1: f.(x,c) = 1.Z_2 by TARSKI:def 1;
eta(p,dim(p)) = f by Def6;
hence thesis by A1,Def13;
end;
theorem Th72:
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: iseq.1 = 1.Z_2
proof
reconsider egy = 1 as Nat;
set z = egy-th-polytope(p,dim(p));
egy <= num-polytopes(p,dim(p)) by Th29;
then
A3: iseq.egy = (c@z)*(incidence-value(x,z)) by Def16;
c@z = 1.Z_2 & incidence-value(x,z) = 1.Z_2 by A1,Th69,Th70,Th71;
hence thesis by A3;
end;
num-polytopes(p,dim(p))= 1 by Th29;
then len iseq = 1 by Def16;
hence thesis by A2,FINSEQ_1:40;
end;
theorem Th73:
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);
assume c = {p};
then incidence-sequence(x,c) = <*1.Z_2*> by Th72;
hence thesis by FINSOP_1:11;
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 Th74:
(dim(p)-boundary(p)).{p} = (dim(p)-1)-polytopes(p)
proof
reconsider c = {p} as Element of dim(p)-chain-space(p) by Th62;
set T = dim(p)-boundary(p);
set X = (dim(p)-1)-polytopes(p);
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;
Sum incidence-sequence(x,c) = 1.Z_2 by Th73;
then x in Boundary(c) by Def17;
hence thesis by Def18;
end;
end;
hence thesis by SUBSET_1:3;
end;
theorem Th75:
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 B = {p};
assume not T is one-to-one;
then consider x1,x2 being object such that
A1: x1 in dom T and
A2: x2 in dom T and
A3: T.x1 = T.x2 and
A4: x1 <> x2 by FUNCT_1:def 4;
reconsider x2 as Element of V by A2;
reconsider x1 as Element of V by A1;
per cases by A4,Th67;
suppose
x1 = 0.V;
then x2 = B & T.x1 = 0.U by A4,Th66,RANKNULL:9;
hence thesis by A3,Th74;
end;
suppose
x2 = 0.V;
then x1 = B & T.x2 = 0.U by A4,Th66,RANKNULL:9;
hence thesis by A3,Th74;
end;
end;
theorem Th76:
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: card [#]V = card (T .: [#]U) by RANKNULL:def 2
.= card (rng T) by RELSET_1:22;
A2: card (dom T) = card [#]U by RANKNULL:7
.= 2 by Th61;
T is one-to-one by Th75;
then card [#]V = 2 by A1,A2,CARD_1:70;
hence thesis by RANKNULL:6;
end;
theorem Th77:
p is simply-connected implies dim ((dim(p)-1)-circuit-space(p)) = 1
proof
set d = dim(p);
set U = (d-1)-bounding-chain-space(p);
set V = (d-1)-circuit-space(p);
assume p is simply-connected;
then U = V by Th48;
hence thesis by Th76;
end;
theorem Th78:
1 < n & n < dim(p) + 2 implies (alternating-f-vector(p)).n = (
alternating-proper-f-vector(p)).(n-1)
proof
assume
A1: 1 < n;
1 - 1 = 0;
then reconsider m = n - 1 as Element of NAT by A1,INT_1:3,XREAL_1:13;
reconsider m as Nat;
set apcs = alternating-proper-f-vector(p);
set acs = alternating-f-vector(p);
A2: 2 - 1 = 1;
1 + 1 = 2;
then 2 <= n by A1,INT_1:7;
then
A3: 1 <= m by A2,XREAL_1:13;
assume
A4: n < dim(p) + 2;
then n < (dim(p) + 1) + 1;
then n <= dim(p) + 1 by NAT_1:13;
then n - 1 <= (dim(p) + 1) - 1 by XREAL_1:9;
then
A5: apcs.m = ((-1)|^(m+1))*num-polytopes(p,m-1) by A3,Def27;
acs.n = ((-1)|^n)*num-polytopes(p,n-2) by A1,A4,Def26;
hence thesis by A5;
end;
theorem Th79:
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 <*(-1)|^(dim(p))*> = 1 by FINSEQ_1:39;
A2: len apcs = n by Def27;
A3: len acs = n + 2 by Def26;
A4: for k being Nat st 1 <= k & k <= len acs holds acs.k = r.k
proof
let k be Nat such that
A5: 1 <= k & k <= len acs;
per cases by A3,A5,XXREAL_0:1;
suppose
A6: k = 1;
reconsider o = 1 as Nat;
1 <= n + 2 & o - 2 = -1 by Th10;
then
A7: acs.o = ((-1)|^o)*num-polytopes(p,-1) by Def26;
(-1)|^1 = -1 & num-polytopes(p,-1) = 1 by Th28;
hence thesis by A6,A7,Th15;
end;
suppose
A8: k = n + 2;
len <*-1*> = 1 by FINSEQ_1:39;
then k = (len <*-1*> + len (apcs) + 1) by A2,A8;
then
A9: r.k = (-1)|^(dim(p)) by Th16
.= (-1)|^k by A8,Th12;
1 <= k by A8,Th10;
then
A10: acs.k = ((-1)|^k)*num-polytopes(p,k-2) by A8,Def26;
num-polytopes(p,k-2) = 1 by A8,Th29;
hence thesis by A10,A9;
end;
suppose
A11: 1 < k & k < n + 2;
set m = k - 1;
A12: (k + 1) - 1 = k & (n + 2) - 1 = n + 1;
A13: k + 1 <= n + 2 by A11,INT_1:7;
len (<*-1*> ^ apcs) = (len <*-1*> + len apcs) by FINSEQ_1:22
.= n + 1 by A2,FINSEQ_1:39;
then len <*-1*> = 1 & k <= len (<*-1*> ^ apcs) by A13,A12,FINSEQ_1:39
,XREAL_1:9;
then r.k = apcs.m by A11,Th17;
hence thesis by A11,Th78;
end;
end;
len r = (len <*-1*>) + (len apcs) + (len <*(-1)|^(dim(p))*>) & len <*-1
*> = 1 by Th14,FINSEQ_1:39;
hence thesis by A3,A2,A1,A4;
end;
begin :: A Generalized Euler Relation and its 1-, 2-, and 3-dimensional Special Cases
theorem Th80:
dim(p) is odd implies
Sum (alternating-f-vector(p)) = Sum (alternating-proper-f-vector(p)) - 2
proof
reconsider minusone = -1 as Integer;
set acs = alternating-f-vector(p);
set apcs = alternating-proper-f-vector(p);
reconsider lastterm = (-1)|^(dim(p)) as Integer;
assume dim(p) is odd;
then
A1: (-1)|^(dim(p)) = -1 by Th8;
acs = <*-1*> ^ apcs ^ <*(-1)|^(dim(p))*> by Th79;
then Sum acs = (Sum <*minusone*>) + (Sum apcs) + (Sum <*lastterm*>) by Th19
.= (Sum <*minusone*>) + (Sum apcs) + (-1) by A1,RVSUM_1:73
.= (-1) + (Sum apcs) + (-1) by RVSUM_1:73
.= (Sum apcs) - 2;
hence thesis;
end;
theorem Th81:
dim(p) is even implies
Sum (alternating-f-vector(p)) = Sum (alternating-proper-f-vector(p))
proof
reconsider minusone = -1 as Integer;
set acs = alternating-f-vector(p);
set apcs = alternating-proper-f-vector(p);
reconsider lastterm = (-1)|^(dim(p)) as Integer;
assume dim(p) is even;
then
A1: (-1)|^(dim(p)) = 1 by Th7;
acs = <*-1*> ^ apcs ^ <*(-1)|^(dim(p))*> by Th79;
then Sum acs = (Sum <*minusone*>) + (Sum apcs) + (Sum <*lastterm*>) by Th19
.= (Sum <*minusone*>) + (Sum apcs) + 1 by A1,RVSUM_1:73
.= (-1) + (Sum apcs) + 1 by RVSUM_1:73
.= Sum apcs;
hence thesis;
end;
theorem Th82:
dim(p) = 1 implies Sum alternating-proper-f-vector(p) = num-polytopes(p,0)
proof
reconsider egy = 1 as Nat;
set apcs = alternating-proper-f-vector(p);
assume dim(p) = 1;
then
A1: len apcs = 1 & apcs.egy = (-1)|^(egy+1)*num-polytopes(p,egy-1) by Def27;
(-1)|^(egy+1) = 1 by Th4,Th7;
then apcs = <*num-polytopes(p,0)*> by A1,FINSEQ_1:40;
hence thesis by RVSUM_1:73;
end;
theorem Th83:
dim(p) = 2 implies Sum alternating-proper-f-vector(p) =
num-polytopes(p,0) - num-polytopes(p,1)
proof
reconsider t = 2 as Nat;
reconsider o = 1 as Nat;
set apcs = alternating-proper-f-vector(p);
reconsider apcso = apcs.o as Integer;
reconsider apcst = apcs.t as Integer;
assume
A1: dim(p) = 2;
then
A2: apcs.o = ((-1)|^(o+1))*num-polytopes(p,o-1) & apcs.t = ((-1)|^(t+1))*
num-polytopes(p,t-1) by Def27;
A3: (-1)|^(o+1) = 1 & (-1)|^(t+1) = -1 by Th4,Th7,Th8;
len apcs = 2 by A1,Def27;
then apcs = <*apcso,apcst*> by FINSEQ_1:44;
then Sum apcs = apcso + apcst by RVSUM_1:77
.= num-polytopes(p,0) - num-polytopes(p,1) by A2,A3;
hence thesis;
end;
theorem Th84:
dim(p) = 3 implies Sum alternating-proper-f-vector(p) =
num-polytopes(p,0) - num-polytopes(p,1) + num-polytopes(p,2)
proof
reconsider mo = -1 as Integer;
reconsider th = 3 as Nat;
reconsider tw = 2 as Nat;
reconsider o = 1 as Nat;
assume
A1: dim(p) = 3;
set apcs = alternating-proper-f-vector(p);
(-1)|^(tw+1) = -1 by Th5,Th8;
then
A2: apcs.tw = mo*num-polytopes(p,tw-1) by A1,Def27;
(-1)|^(th+1) = 1 by Th6,Th7;
then
A3: apcs.th = o*num-polytopes(p,th-1) by A1,Def27;
reconsider apcsth = apcs.th as Integer;
reconsider apcstw = apcs.tw as Integer;
reconsider apcson = apcs.o as Integer;
(-1)|^(o+1) = 1 by Th4,Th7;
then
A4: apcs.o = o*num-polytopes(p,o-1) by A1,Def27;
len apcs = 3 by A1,Def27;
then apcs = <*apcson,apcstw,apcsth*> by FINSEQ_1:45;
then Sum apcs = apcson + apcstw + apcsth by RVSUM_1:78
.= num-polytopes(p,0) - num-polytopes(p,1) + num-polytopes(p,2) by A4,A2,A3
;
hence thesis;
end;
:: A trivial special case
theorem Th85:
dim(p) = 0 implies p is eulerian
proof
set d = dim(p);
set apcs = alternating-proper-f-vector(p);
assume
A1: d = 0;
then (-1)|^(d+1) = -1;
then
A2: 1 + (-1)|^(d+1) = 0;
len apcs = 0 by A1,Def27;
then apcs = <*>INT;
hence thesis by A2,GR_CY_1:3;
end;
theorem Th86:
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 Th85;
end;
suppose
A2: dim(p) > 0;
deffunc B(Nat) = ((-1)|^($1+1))*(dim (($1-1)-circuit-space(p)));
deffunc A(Nat) = ((-1)|^($1+1))*(dim (($1-2)-bounding-chain-space(p)));
consider a being FinSequence such that
A3: len a = len apcs and
A4: for n being Nat st n in dom a holds a.n = A(n) from FINSEQ_1:sch 2;
A5: rng a c= INT
proof
let y be object;
assume y in rng a;
then consider x being object such that
A6: x in dom a and
A7: y = a.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A6;
a.x = ((-1)|^(x+1))*(dim ((x-2)-bounding-chain-space(p))) by A4,A6;
hence thesis by A7, INT_1:def 2;
end;
consider b being FinSequence such that
A8: len b = len apcs and
A9: for n being Nat st n in dom b holds b.n = B(n) from FINSEQ_1:sch 2;
rng b c= INT
proof
let y be object;
assume y in rng b;
then consider x being object such that
A10: x in dom b and
A11: y = b.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A10;
b.x = ((-1)|^(x+1))*(dim ((x-1)-circuit-space(p))) by A9,A10;
hence thesis by A11,INT_1:def 2;
end;
then reconsider a,b as FinSequence of INT by A5,FINSEQ_1:def 4;
A12: len apcs > 0 by A2,Def27;
A13: a.1 = 1
proof
reconsider egy = 1 as Element of NAT;
1 <= 0 + 1;
then egy <= len apcs by A12,NAT_1:13;
then egy in dom a by A3,FINSEQ_3:25;
then
a.egy = ((-1)|^(1+1))*(dim ((egy-2)-bounding-chain-space(p))) by A4
.= 1*(dim ((egy-2)-bounding-chain-space(p))) by Th4,Th7
.= 1 by Th60;
hence thesis;
end;
A14: for n being Nat st 1 <= n & n < len apcs holds b.n = -(a.(n+1))
proof
let n be Nat such that
A15: 1 <= n and
A16: n < len apcs;
A17: n in dom b by A8,A15,A16,FINSEQ_3:25;
reconsider n as Element of NAT by ORDINAL1:def 12;
A18: b.n = ((-1)|^(n+1))*(dim ((n-1)-circuit-space(p))) by A9,A17;
A19: 1 <= n + 1 by NAT_1:11;
n + 1 <= len apcs by A16,INT_1:7;
then n + 1 in dom a by A3,A19,FINSEQ_3:25;
then a.(n+1) = A(n+1) by A4
.= (((-1)|^(n+1))*((-1)|^1))*(dim ((n-1)-bounding-chain-space(p)))
by NEWTON:8
.= ((-1)|^(n+1))*(-1)*(dim ((n-1)-bounding-chain-space(p)))
.= -((-1)|^(n+1))*(dim ((n-1)-bounding-chain-space(p)))
.= -(b.n) by A1,A18,Th48;
hence thesis;
end;
A20: b.(len apcs) = (-1)|^(dim(p)+1)
proof
reconsider n = len apcs as Element of NAT;
A21: n = dim(p) by Def27;
0 + 1 = 1;
then 1 <= len apcs by A12,NAT_1:13;
then n in dom b by A8,FINSEQ_3:25;
then b.n = B(n) by A9
.= ((-1)|^(n+1))*1 by A1,A21,Th77
.= (-1)|^(n+1);
hence thesis by Def27;
end;
for n being Nat st 1 <= n & n <= len apcs holds apcs.n = a.n + b.n
proof
let n be Nat such that
A22: 1 <= n & n <= len apcs;
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
n9 in dom a by A3,A22,FINSEQ_3:25;
then
A23: a.n9 = ((-1)|^(n9+1))*(dim ((n9-2)-bounding-chain-space(p))) by A4;
apcs.n = ((-1)|^(n+1))*(dim ((n-2)-bounding-chain-space(p))) +
((-1)|^(n+1))* (dim ((n-1)-circuit-space(p))) & n9 in dom b
by A8,A22,Th49,FINSEQ_3:25;
hence thesis by A9,A23;
end;
then Sum apcs = (a.1) + (b.(len apcs)) by A12,A3,A8,A14,Th13;
hence thesis by A13,A20;
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
set acs = alternating-f-vector(p);
set apcs = alternating-proper-f-vector(p);
assume p is simply-connected;
then
A1: p is eulerian by Th86;
assume
A2: dim(p) = 1;
0 = Sum acs by A1
.= Sum apcs - 2 by A2,Th3,Th80
.= num-polytopes(p,0) - 2 by A2,Th82;
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
set s = num-polytopes(p,0) - num-polytopes(p,1);
set c = alternating-f-vector(p);
assume p is simply-connected;
then
A1: p is eulerian by Th86;
assume
A2: dim(p) = 2;
then
A3: s = Sum(alternating-proper-f-vector(p)) by Th83;
0 = Sum c by A1
.= s by A2,A3,Th4,Th81;
hence thesis;
end;
:: Euler's Polyhedron Formula in Three Dimensions: V - E + F = 2.
::$N Euler's Polyhedron Formula
::$L https://en.wikipedia.org/wiki/Polyhedron Euler's Polyhedron Formula
theorem
p is simply-connected & dim(p) = 3 implies
num-vertices(p) - num-edges(p) + num-faces(p) = 2
proof
set s = num-polytopes(p,0) - num-polytopes(p,1) + num-polytopes(p,2);
set c = alternating-f-vector(p);
assume p is simply-connected;
then
A1: p is eulerian by Th86;
assume
A2: dim(p) = 3;
then
A3: s = Sum(alternating-proper-f-vector(p)) by Th84;
0 = Sum c by A1
.= s - 2 by A2,A3,Th5,Th80;
hence thesis;
end;