:: Euler's Polyhedron Formula
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007-2016 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;