:: Euler's Polyhedron Formula :: by Jesse Alama :: :: Received October 9, 2007 :: Copyright (c) 2007-2021 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; 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, 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; begin theorem :: POLYFORM:1 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}; begin :: Arithmetical Preliminaries reserve n for Nat, k for Integer; ::$CT theorem :: POLYFORM:3 1 <= k implies k is Nat; theorem :: POLYFORM:4 1 is odd; theorem :: POLYFORM:5 2 is even; theorem :: POLYFORM:6 3 is odd; theorem :: POLYFORM:7 4 is even; theorem :: POLYFORM:8 n is even implies (-1)|^n = 1; theorem :: POLYFORM:9 n is odd implies (-1)|^n = -1; ::$CT theorem :: POLYFORM:11 for p,q,r being FinSequence holds len (p ^ q) <= len (p ^ (q ^ r )); theorem :: POLYFORM:12 1 < n + 2; theorem :: POLYFORM:13 (-1)|^2 = 1; theorem :: POLYFORM:14 for n being Nat holds (-1)|^n = (-1)|^(n+2); begin :: Preliminaries on Finite Sequences :: A theorem on telescoping sequences of integers. theorem :: POLYFORM:15 for a,b,s being FinSequence of INT st len s > 0 & len a = len s & len b = len s & (for n being Nat st 1 <= n & n <= len s holds s.n = a.n + b.n ) & (for k being Nat st 1 <= k & k < len s holds b.k = -(a.(k+1))) holds Sum s = (a.1) + (b.(len s)); theorem :: POLYFORM:16 for p,q,r being FinSequence holds len (p ^ q ^ r) = (len p) + ( len q) + (len r); theorem :: POLYFORM:17 for x being set, p,q being FinSequence holds (<*x*> ^ p ^ q).1 = x; theorem :: POLYFORM:18 for x being set, p,q being FinSequence holds (p ^ q ^ <*x*>).(( len p) + (len q) + 1) = x; theorem :: POLYFORM:19 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)); definition let a be Integer; redefine func <*a*> -> FinSequence of INT; end; definition let a,b be Integer; redefine func <*a,b*> -> FinSequence of INT; end; definition let a,b,c be Integer; redefine func <*a,b,c*> -> FinSequence of INT; end; theorem :: POLYFORM:20 for k being Integer, p being FinSequence of INT holds Sum (<*k*> ^ p) = k + (Sum p); theorem :: POLYFORM:21 for p,q,r being FinSequence of INT holds Sum (p ^ q ^ r) = (Sum p) + (Sum q) + (Sum r); theorem :: POLYFORM:22 for a being Element of Z_2 holds Sum <*a*> = a; 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 :: POLYFORM:23 for X,Y being set holds [:X,Y:] --> 1.Z_2 is incidence-matrix of X,Y; :: 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 :: POLYFORM:def 1 len the IncidenceF of p = len(the PolytopsF of p) - 1; attr p is polyhedron_2 means :: POLYFORM:def 2 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 :: POLYFORM:def 3 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; 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 :: POLYFORM:def 4 len the PolytopsF of p; 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 :: POLYFORM:def 5 (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 = {}); end; theorem :: POLYFORM:24 -1 < k & k < dim(p) implies k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim(p); theorem :: POLYFORM:25 k-polytopes(p) is non empty iff -1 <= k & k <= dim(p); theorem :: POLYFORM:26 k < dim(p) implies k - 1 < dim(p); :: 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 :: POLYFORM:def 6 (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 = {}); end; definition let p be polyhedron, k be Integer; func k-polytope-seq(p) -> FinSequence means :: POLYFORM:def 7 (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 = <*>{}); end; definition let p be polyhedron, k be Integer; func num-polytopes(p,k) -> Element of NAT equals :: POLYFORM:def 8 card(k-polytopes(p)); 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 :: POLYFORM:def 9 num-polytopes(p,0); func num-edges(p) -> Element of NAT equals :: POLYFORM:def 10 num-polytopes(p,1); func num-faces(p) -> Element of NAT equals :: POLYFORM:def 11 num-polytopes(p,2); end; theorem :: POLYFORM:27 dom (k-polytope-seq(p)) = Seg (num-polytopes(p,k)); theorem :: POLYFORM:28 len (k-polytope-seq(p)) = num-polytopes(p,k); theorem :: POLYFORM:29 rng (k-polytope-seq(p)) = k-polytopes(p); theorem :: POLYFORM:30 num-polytopes(p,-1) = 1; theorem :: POLYFORM:31 num-polytopes(p,dim(p)) = 1; :: 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 1 <= n & n <= num-polytopes(p,k); func n-th-polytope(p,k) -> Element of k-polytopes(p) equals :: POLYFORM:def 12 (k-polytope-seq(p)).n; end; theorem :: POLYFORM:32 -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) ; theorem :: POLYFORM:33 k-polytope-seq(p) is one-to-one; theorem :: POLYFORM:34 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 ; 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 0 <= k and k <= dim(p); func incidence-value(x,y) -> Element of Z_2 equals :: POLYFORM:def 13 eta(p,k).(x,y); 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 :: POLYFORM:def 14 bspace(k-polytopes(p)); end; theorem :: POLYFORM:35 for x being Element of k-polytopes(p) holds (0.(k-chain-space(p)))@x = 0.Z_2; theorem :: POLYFORM:36 num-polytopes(p,k) = dim (k-chain-space(p)); :: 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 :: POLYFORM:def 15 bool (k-polytopes(p)); 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 :: POLYFORM:def 16 ((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))); end; theorem :: POLYFORM:37 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); theorem :: POLYFORM:38 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); theorem :: POLYFORM:39 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)); theorem :: POLYFORM:40 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)); theorem :: POLYFORM:41 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); theorem :: POLYFORM:42 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); theorem :: POLYFORM:43 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; theorem :: POLYFORM:44 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; scheme :: POLYFORM:sch 1 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()); :: 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 :: POLYFORM:def 17 ((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); end; theorem :: POLYFORM:45 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); :: 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 :: POLYFORM:def 18 for c being Element of k-chain-space(p) holds it.c = Boundary(c); end; theorem :: POLYFORM:46 for c,d being Element of k-chain-space(p) holds Boundary(c+d) = Boundary(c) + Boundary(d); theorem :: POLYFORM:47 for a being Element of Z_2, c being Element of k-chain-space(p) holds Boundary(a*c) = a*(Boundary(c)); :: As defined, the k-boundary operator gives rise to a linear :: transformation. theorem :: POLYFORM:48 k-boundary(p) is linear-transformation of k-chain-space(p),(k-1) -chain-space(p); registration let p be polyhedron, k be Integer; cluster k-boundary(p) -> homogeneous additive; 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 :: POLYFORM:def 19 ker (k-boundary(p)); end; definition let p be polyhedron, k be Integer; func k-circuits(p) -> non empty Subset of k-chains(p) equals :: POLYFORM:def 20 [#](k-circuit-space(p)); end; definition let p be polyhedron, k be Integer; func k-bounding-chain-space(p) -> Subspace of k-chain-space(p) equals :: POLYFORM:def 21 im ((k+1)-boundary(p)); end; definition let p be polyhedron, k be Integer; func k-bounding-chains(p) -> non empty Subset of k-chains(p) equals :: POLYFORM:def 22 [#](k-bounding-chain-space(p)); end; definition let p be polyhedron, k be Integer; func k-bounding-circuit-space(p) -> Subspace of k-chain-space(p) equals :: POLYFORM:def 23 (k-bounding-chain-space(p)) /\ (k-circuit-space(p)); end; definition let p be polyhedron, k be Integer; func k-bounding-circuits(p) -> non empty Subset of k-chains(p) equals :: POLYFORM:def 24 [#](k-bounding-circuit-space(p)); end; theorem :: POLYFORM:49 dim (k-chain-space(p)) = rank (k-boundary(p)) + nullity (k-boundary(p) ); 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 :: POLYFORM:def 25 for k being Integer holds k -circuits(p) = k-bounding-chains(p); end; theorem :: POLYFORM:50 p is simply-connected iff for n being Integer holds n -circuit-space(p) = n-bounding-chain-space(p); definition let p be polyhedron; func alternating-f-vector(p) -> FinSequence of INT means :: POLYFORM:def 26 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); end; definition let p be polyhedron; func alternating-proper-f-vector(p) -> FinSequence of INT means :: POLYFORM:def 27 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); end; definition let p be polyhedron; func alternating-semi-proper-f-vector(p) -> FinSequence of INT means :: POLYFORM:def 28 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); end; theorem :: POLYFORM:51 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))); :: The term "eulerian" comes from Lakatos. definition let p be polyhedron; attr p is eulerian means :: POLYFORM:def 29 Sum (alternating-proper-f-vector(p)) = 1 + (-1)|^(dim(p)+1); end; theorem :: POLYFORM:52 alternating-semi-proper-f-vector(p) = alternating-proper-f-vector(p) ^ <*(-1)|^(dim(p))*>; :: Another characterization of Eulerian polyhedra definition let p be polyhedron; redefine attr p is eulerian means :: POLYFORM:def 30 Sum ( alternating-semi-proper-f-vector(p)) = 1; end; theorem :: POLYFORM:53 alternating-f-vector(p) = <*-1*> ^ alternating-semi-proper-f-vector(p); :: Yet another characterization of eulerian polyhedra definition let p be polyhedron; redefine attr p is eulerian means :: POLYFORM:def 31 Sum (alternating-f-vector(p)) = 0; end; begin :: The Extremal Chain Spaces theorem :: POLYFORM:54 0-polytopes(p) is non empty; theorem :: POLYFORM:55 card [#]((-1)-chain-space(p)) = 2; theorem :: POLYFORM:56 [#]((-1)-chain-space(p)) = { {}, {{}} }; theorem :: POLYFORM:57 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; theorem :: POLYFORM:58 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; theorem :: POLYFORM:59 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; theorem :: POLYFORM:60 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; theorem :: POLYFORM:61 for x being Element of 0-polytopes(p) holds (0-boundary(p)).({x} ) = {{}}; theorem :: POLYFORM:62 k = -1 implies dim(k-bounding-chain-space(p)) = 1; theorem :: POLYFORM:63 card [#](dim(p)-chain-space(p)) = 2; theorem :: POLYFORM:64 {p} is Element of dim(p)-chain-space(p); theorem :: POLYFORM:65 {p} in [#](dim(p)-chain-space(p)); theorem :: POLYFORM:66 (dim(p) - 1)-polytopes(p) is non empty; registration let p be polyhedron; cluster (dim(p)-1)-polytopes(p) -> non empty; end; theorem :: POLYFORM:67 [#](dim(p)-chain-space(p)) = { 0.(dim(p)-chain-space(p)), {p} }; theorem :: POLYFORM:68 for x being Element of dim(p)-chain-space(p) holds x = 0.(dim(p) -chain-space(p)) or x = {p}; theorem :: POLYFORM:69 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)); theorem :: POLYFORM:70 dim(p)-polytope-seq(p) = <*p*>; theorem :: POLYFORM:71 1-th-polytope(p,dim(p)) = p; theorem :: POLYFORM:72 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; theorem :: POLYFORM:73 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; theorem :: POLYFORM:74 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*> ; theorem :: POLYFORM:75 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 ; :: 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 :: POLYFORM:76 (dim(p)-boundary(p)).{p} = (dim(p)-1)-polytopes(p); theorem :: POLYFORM:77 dim(p)-boundary(p) is one-to-one; theorem :: POLYFORM:78 dim ((dim(p)-1)-bounding-chain-space(p)) = 1; theorem :: POLYFORM:79 p is simply-connected implies dim ((dim(p)-1)-circuit-space(p)) = 1; theorem :: POLYFORM:80 1 < n & n < dim(p) + 2 implies (alternating-f-vector(p)).n = ( alternating-proper-f-vector(p)).(n-1); theorem :: POLYFORM:81 alternating-f-vector(p) = <*-1*> ^ alternating-proper-f-vector(p ) ^ <*(-1)|^(dim(p))*>; begin :: A Generalized Euler Relation and its 1-, 2-, and 3-dimensional Special Cases theorem :: POLYFORM:82 dim(p) is odd implies Sum (alternating-f-vector(p)) = Sum ( alternating-proper-f-vector(p)) - 2; theorem :: POLYFORM:83 dim(p) is even implies Sum (alternating-f-vector(p)) = Sum ( alternating-proper-f-vector(p)); theorem :: POLYFORM:84 dim(p) = 1 implies Sum alternating-proper-f-vector(p) = num-polytopes(p,0); theorem :: POLYFORM:85 dim(p) = 2 implies Sum alternating-proper-f-vector(p) = num-polytopes(p,0) - num-polytopes(p,1); theorem :: POLYFORM:86 dim(p) = 3 implies Sum alternating-proper-f-vector(p) = num-polytopes(p,0) - num-polytopes(p,1) + num-polytopes(p,2); :: A trivial special case theorem :: POLYFORM:87 dim(p) = 0 implies p is eulerian; theorem :: POLYFORM:88 p is simply-connected implies p is eulerian; :: Euler's Polyhedron Formula in One Dimension: simply-connected :: 1-dimensional polyhedra are just line segments. theorem :: POLYFORM:89 p is simply-connected & dim(p) = 1 implies num-vertices(p) = 2; :: Euler's Polyhedron Formula in Two Dimensions: polygons have exactly :: as many vertices as edges. theorem :: POLYFORM:90 p is simply-connected & dim(p) = 2 implies num-vertices(p) = num-edges (p); :: Euler's Polyhedron Formula in Three Dimensions: V - E + F = 2. ::$N Euler's Polyhedron Formula theorem :: POLYFORM:91 p is simply-connected & dim(p) = 3 implies num-vertices(p) - num-edges (p) + num-faces(p) = 2;