:: by Jesse Alama

::

:: Received October 9, 2007

:: Copyright (c) 2007-2021 Association of Mizar Users

theorem Th1: :: POLYFORM:1

for X being set

for 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}

for 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 end;

::$CT

Lm1: for x being Element of NAT st 0 < x holds

0 + 1 <= x

by NAT_1:13;

:: A theorem on telescoping sequences of integers.

theorem Th13: :: 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))

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 end;

theorem Th17: :: POLYFORM:19

for p, q, r being FinSequence

for k being Nat st len p < k & k <= len (p ^ q) holds

((p ^ q) ^ r) . k = q . (k - (len p))

for k being Nat st len p < k & k <= len (p ^ q) holds

((p ^ q) ^ r) . k = q . (k - (len p))

proof end;

definition

let a be Integer;

:: original: <*

redefine func <*a*> -> FinSequence of INT ;

coherence

<*a*> is FinSequence of INT

end;
:: original: <*

redefine func <*a*> -> FinSequence of INT ;

coherence

<*a*> is FinSequence of INT

proof end;

definition

let a, b be Integer;

:: original: <*

redefine func <*a,b*> -> FinSequence of INT ;

coherence

<*a,b*> is FinSequence of INT

end;
:: original: <*

redefine func <*a,b*> -> FinSequence of INT ;

coherence

<*a,b*> is FinSequence of INT

proof end;

definition

let a, b, c be Integer;

:: original: <*

redefine func <*a,b,c*> -> FinSequence of INT ;

coherence

<*a,b,c*> is FinSequence of INT

end;
:: original: <*

redefine func <*a,b,c*> -> FinSequence of INT ;

coherence

<*a,b,c*> is FinSequence of INT

proof end;

:: An incidence matrix is a function that says of any two objects

:: (contained in some set) whether they are incidence to each other.

:: (contained in some set) whether they are incidence to each other.

definition
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.

:: 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

attr c_{1} is strict ;

struct PolyhedronStr -> ;

aggr PolyhedronStr(# PolytopsF, IncidenceF #) -> PolyhedronStr ;

sel PolytopsF c_{1} -> FinSequence-yielding FinSequence;

sel IncidenceF c_{1} -> Function-yielding FinSequence;

end;
struct PolyhedronStr -> ;

aggr PolyhedronStr(# PolytopsF, IncidenceF #) -> PolyhedronStr ;

sel PolytopsF c

sel IncidenceF c

:: 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.

:: `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 ;

end;
attr p is polyhedron_1 means :: POLYFORM:def 1

len the IncidenceF of p = (len the PolytopsF of p) - 1;

len the IncidenceF of p = (len the PolytopsF of p) - 1;

attr p is polyhedron_2 means :Def2: :: 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)));

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: :: POLYFORM:def 3

for n being Nat st 1 <= n & n <= len the PolytopsF of p holds

( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one );

for n being Nat st 1 <= n & n <= len the PolytopsF of p holds

( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one );

:: deftheorem defines polyhedron_1 POLYFORM:def 1 :

for p being PolyhedronStr holds

( p is polyhedron_1 iff len the IncidenceF of p = (len the PolytopsF of p) - 1 );

for p being PolyhedronStr holds

( p is polyhedron_1 iff len the IncidenceF of p = (len the PolytopsF of p) - 1 );

:: deftheorem Def2 defines polyhedron_2 POLYFORM:def 2 :

for p being PolyhedronStr holds

( p is polyhedron_2 iff for n being Nat st 1 <= n & 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))) );

for p being PolyhedronStr holds

( p is polyhedron_2 iff 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))) );

:: deftheorem Def3 defines polyhedron_3 POLYFORM:def 3 :

for p being PolyhedronStr holds

( p is polyhedron_3 iff for n being Nat st 1 <= n & n <= len the PolytopsF of p holds

( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) );

for p being PolyhedronStr holds

( p is polyhedron_3 iff for n being Nat st 1 <= n & n <= len the PolytopsF of p holds

( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) );

registration

existence

ex b_{1} being PolyhedronStr st

( b_{1} is polyhedron_1 & b_{1} is polyhedron_2 & b_{1} is polyhedron_3 )

end;
ex b

( b

proof end;

:: The dimension dim(p) of a polyhedron p is just the number of

:: polytope sets that it has.

:: polytope sets that it has.

:: deftheorem defines dim POLYFORM:def 4 :

for p being polyhedron holds dim p = len the PolytopsF of p;

for p being polyhedron holds dim p = len the PolytopsF of p;

:: For integers k such that 0 <= k <= dim(p), the set of k-polytopes

:: is data already given by the polyhedron. For k = dim(p), the set

:: is the singleton {p}, which seems clear enough. For k = -1, it is

:: convenient to define the set of k-polytopes to be {{}}. Doing this

:: ensures that, if p is simply connected, then any two vertices are

:: connected by a system of edges.

::

:: For k < -1 and k > dim(p), the set of k-polytopes of p is empty.

:: is data already given by the polyhedron. For k = dim(p), the set

:: is the singleton {p}, which seems clear enough. For k = -1, it is

:: convenient to define the set of k-polytopes to be {{}}. Doing this

:: ensures that, if p is simply connected, then any two vertices are

:: connected by a system of edges.

::

:: For k < -1 and k > dim(p), the set of k-polytopes of p is empty.

definition

let p be polyhedron;

let k be Integer;

ex b_{1} being finite set st

( ( k < - 1 implies b_{1} = {} ) & ( k = - 1 implies b_{1} = {{}} ) & ( - 1 < k & k < dim p implies b_{1} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b_{1} = {p} ) & ( k > dim p implies b_{1} = {} ) )

for b_{1}, b_{2} being finite set st ( k < - 1 implies b_{1} = {} ) & ( k = - 1 implies b_{1} = {{}} ) & ( - 1 < k & k < dim p implies b_{1} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b_{1} = {p} ) & ( k > dim p implies b_{1} = {} ) & ( k < - 1 implies b_{2} = {} ) & ( k = - 1 implies b_{2} = {{}} ) & ( - 1 < k & k < dim p implies b_{2} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b_{2} = {p} ) & ( k > dim p implies b_{2} = {} ) holds

b_{1} = b_{2}

end;
let k be Integer;

func k -polytopes p -> finite set means :Def5: :: 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 = {} ) );

existence ( ( 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 = {} ) );

ex b

( ( k < - 1 implies b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines -polytopes POLYFORM:def 5 :

for p being polyhedron

for k being Integer

for b_{3} being finite set holds

( b_{3} = k -polytopes p iff ( ( k < - 1 implies b_{3} = {} ) & ( k = - 1 implies b_{3} = {{}} ) & ( - 1 < k & k < dim p implies b_{3} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b_{3} = {p} ) & ( k > dim p implies b_{3} = {} ) ) );

for p being polyhedron

for k being Integer

for b

( b

theorem Th22: :: POLYFORM:24

for p being polyhedron

for k being Integer st - 1 < k & k < dim p holds

( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )

for k being Integer st - 1 < k & k < dim p holds

( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )

proof end;

theorem Th23: :: POLYFORM:25

for p being polyhedron

for k being Integer holds

( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )

for k being Integer holds

( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )

proof end;

theorem :: POLYFORM:26

for p being polyhedron

for k being Integer st k < dim p holds

k - 1 < dim p by XREAL_1:146, XXREAL_0:2;

for k being Integer st k < dim p holds

k - 1 < dim p by XREAL_1:146, XXREAL_0:2;

:: As we defined the set of k-polytopes for all integers k, we define

:: the an incidence matrix, eta(p,k), for any integer k. Naturally,

:: for almost all k, this is the empty matrix (empty function). The

:: two cases in which we extend the data already given by the

:: polyhedron itself is for k = 0 and k = dim(p). For the latter, we

:: declare that the empty set (the unique -1-dimensional polytope) is

:: incident to all 0-polytopes. For the latter, we declare that every

:: (dim(p)-1)-polytope is incidence to p, the unique dim(p)-polytope

:: of p.

:: the an incidence matrix, eta(p,k), for any integer k. Naturally,

:: for almost all k, this is the empty matrix (empty function). The

:: two cases in which we extend the data already given by the

:: polyhedron itself is for k = 0 and k = dim(p). For the latter, we

:: declare that the empty set (the unique -1-dimensional polytope) is

:: incident to all 0-polytopes. For the latter, we declare that every

:: (dim(p)-1)-polytope is incidence to p, the unique dim(p)-polytope

:: of p.

definition

let p be polyhedron;

let k be Integer;

ex b_{1} being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st

( ( k < 0 implies b_{1} = {} ) & ( k = 0 implies b_{1} = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b_{1} = the IncidenceF of p . k ) & ( k = dim p implies b_{1} = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b_{1} = {} ) )

for b_{1}, b_{2} being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st ( k < 0 implies b_{1} = {} ) & ( k = 0 implies b_{1} = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b_{1} = the IncidenceF of p . k ) & ( k = dim p implies b_{1} = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b_{1} = {} ) & ( k < 0 implies b_{2} = {} ) & ( k = 0 implies b_{2} = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b_{2} = the IncidenceF of p . k ) & ( k = dim p implies b_{2} = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b_{2} = {} ) holds

b_{1} = b_{2}

end;
let k be Integer;

func eta (p,k) -> incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) means :Def6: :: POLYFORM:def 6

( ( k < 0 implies it = {} ) & ( 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 ( ( 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 = {} ) );

ex b

( ( k < 0 implies b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines eta POLYFORM:def 6 :

for p being polyhedron

for k being Integer

for b_{3} being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) holds

( b_{3} = eta (p,k) iff ( ( k < 0 implies b_{3} = {} ) & ( k = 0 implies b_{3} = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b_{3} = the IncidenceF of p . k ) & ( k = dim p implies b_{3} = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b_{3} = {} ) ) );

for p being polyhedron

for k being Integer

for b

( b

definition

let p be polyhedron;

let k be Integer;

ex b_{1} being FinSequence st

( ( k < - 1 implies b_{1} = <*> {} ) & ( k = - 1 implies b_{1} = <*{}*> ) & ( - 1 < k & k < dim p implies b_{1} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b_{1} = <*p*> ) & ( k > dim p implies b_{1} = <*> {} ) )

for b_{1}, b_{2} being FinSequence st ( k < - 1 implies b_{1} = <*> {} ) & ( k = - 1 implies b_{1} = <*{}*> ) & ( - 1 < k & k < dim p implies b_{1} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b_{1} = <*p*> ) & ( k > dim p implies b_{1} = <*> {} ) & ( k < - 1 implies b_{2} = <*> {} ) & ( k = - 1 implies b_{2} = <*{}*> ) & ( - 1 < k & k < dim p implies b_{2} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b_{2} = <*p*> ) & ( k > dim p implies b_{2} = <*> {} ) holds

b_{1} = b_{2}

end;
let k be Integer;

func k -polytope-seq p -> FinSequence means :Def7: :: 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 = <*> {} ) );

existence ( ( 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 = <*> {} ) );

ex b

( ( k < - 1 implies b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines -polytope-seq POLYFORM:def 7 :

for p being polyhedron

for k being Integer

for b_{3} being FinSequence holds

( b_{3} = k -polytope-seq p iff ( ( k < - 1 implies b_{3} = <*> {} ) & ( k = - 1 implies b_{3} = <*{}*> ) & ( - 1 < k & k < dim p implies b_{3} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b_{3} = <*p*> ) & ( k > dim p implies b_{3} = <*> {} ) ) );

for p being polyhedron

for k being Integer

for b

( b

definition
end;

:: deftheorem defines num-polytopes POLYFORM:def 8 :

for p being polyhedron

for k being Integer holds num-polytopes (p,k) = card (k -polytopes p);

for p being polyhedron

for k being Integer holds num-polytopes (p,k) = card (k -polytopes p);

:: It will be convenient to use these in the cases of Euler's

:: polyhedron formula that interest us.

:: polyhedron formula that interest us.

definition

let p be polyhedron;

correctness

coherence

num-polytopes (p,0) is Element of NAT ;

;

correctness

coherence

num-polytopes (p,1) is Element of NAT ;

;

correctness

coherence

num-polytopes (p,2) is Element of NAT ;

;

end;
correctness

coherence

num-polytopes (p,0) is Element of NAT ;

;

correctness

coherence

num-polytopes (p,1) is Element of NAT ;

;

correctness

coherence

num-polytopes (p,2) is Element of NAT ;

;

:: deftheorem defines num-vertices POLYFORM:def 9 :

for p being polyhedron holds num-vertices p = num-polytopes (p,0);

for p being polyhedron holds num-vertices p = num-polytopes (p,0);

:: deftheorem defines num-edges POLYFORM:def 10 :

for p being polyhedron holds num-edges p = num-polytopes (p,1);

for p being polyhedron holds num-edges p = num-polytopes (p,1);

:: deftheorem defines num-faces POLYFORM:def 11 :

for p being polyhedron holds num-faces p = num-polytopes (p,2);

for p being polyhedron holds num-faces p = num-polytopes (p,2);

theorem Th25: :: POLYFORM:27

for p being polyhedron

for k being Integer holds dom (k -polytope-seq p) = Seg (num-polytopes (p,k))

for k being Integer holds dom (k -polytope-seq p) = Seg (num-polytopes (p,k))

proof 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.

:: (finite sequences).

::

:: Since the k-polytope sets are empty for k < -1 and k > dim(p), we

:: have to put a condition on n and k for the definition to make

:: sense.

definition

let p be polyhedron;

let k be Integer;

let n be Nat;

assume A1: ( 1 <= n & n <= num-polytopes (p,k) ) ;

(k -polytope-seq p) . n is Element of k -polytopes p

end;
let k be Integer;

let 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: :: POLYFORM:def 12

(k -polytope-seq p) . n;

coherence (k -polytope-seq p) . n;

(k -polytope-seq p) . n is Element of k -polytopes p

proof end;

:: deftheorem Def12 defines -th-polytope POLYFORM:def 12 :

for p being polyhedron

for k being Integer

for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds

n -th-polytope (p,k) = (k -polytope-seq p) . n;

for p being polyhedron

for k being Integer

for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds

n -th-polytope (p,k) = (k -polytope-seq p) . n;

theorem Th30: :: POLYFORM:32

for p being polyhedron

for k being Integer st - 1 <= k & k <= dim p holds

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) )

for k being Integer st - 1 <= k & k <= dim p holds

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 end;

theorem Th32: :: POLYFORM:34

for p being polyhedron

for k being Integer

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

for k being Integer

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 end;

definition

let p be polyhedron;

let k be Integer;

let x be Element of (k - 1) -polytopes p;

let y be Element of k -polytopes p;

assume that

A1: 0 <= k and

A2: k <= dim p ;

coherence

(eta (p,k)) . (x,y) is Element of Z_2

end;
let k be Integer;

let x be Element of (k - 1) -polytopes p;

let y be Element of k -polytopes p;

assume that

A1: 0 <= k and

A2: k <= dim p ;

coherence

(eta (p,k)) . (x,y) is Element of Z_2

proof end;

:: deftheorem Def13 defines incidence-value POLYFORM:def 13 :

for p being polyhedron

for k being Integer

for x being Element of (k - 1) -polytopes p

for y being Element of k -polytopes p st 0 <= k & k <= dim p holds

incidence-value (x,y) = (eta (p,k)) . (x,y);

for p being polyhedron

for k being Integer

for x being Element of (k - 1) -polytopes p

for y being Element of k -polytopes p st 0 <= k & k <= dim p holds

incidence-value (x,y) = (eta (p,k)) . (x,y);

:: 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.

:: space over the field Z_2. Addition is disjoint union, and scalar

:: multiplication is defined by the equations 1*x = x, 0*x = 0.

definition

let p be polyhedron;

let k be Integer;

bspace (k -polytopes p) is finite-dimensional VectSp of Z_2 ;

end;
let k be Integer;

func k -chain-space p -> finite-dimensional VectSp of Z_2 equals :: POLYFORM:def 14

bspace (k -polytopes p);

coherence bspace (k -polytopes p);

bspace (k -polytopes p) is finite-dimensional VectSp of Z_2 ;

:: deftheorem defines -chain-space POLYFORM:def 14 :

for p being polyhedron

for k being Integer holds k -chain-space p = bspace (k -polytopes p);

for p being polyhedron

for k being Integer holds k -chain-space p = bspace (k -polytopes p);

theorem :: POLYFORM:35

for p being polyhedron

for k being Integer

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

for k being Integer

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

:: A k-chain is a set of k-polytopes.

definition
end;

:: deftheorem defines -chains POLYFORM:def 15 :

for p being polyhedron

for k being Integer holds k -chains p = bool (k -polytopes p);

for p being polyhedron

for k being Integer holds k -chains p = bool (k -polytopes p);

definition

let p be polyhedron;

let k be Integer;

let x be Element of (k - 1) -polytopes p;

let v be Element of (k -chain-space p);

ex b_{1} being FinSequence of Z_2 st

( ( (k - 1) -polytopes p is empty implies b_{1} = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b_{1} = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds

b_{1} . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )

for b_{1}, b_{2} being FinSequence of Z_2 st ( (k - 1) -polytopes p is empty implies b_{1} = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b_{1} = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds

b_{1} . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) & ( (k - 1) -polytopes p is empty implies b_{2} = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b_{2} = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds

b_{2} . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) holds

b_{1} = b_{2}

end;
let k be Integer;

let x be Element of (k - 1) -polytopes p;

let v be Element of (k -chain-space p);

func incidence-sequence (x,v) -> FinSequence of Z_2 means :Def16: :: POLYFORM:def 16

( ( (k - 1) -polytopes p is empty implies it = <*> {} ) & ( not (k - 1) -polytopes p is 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 ( ( (k - 1) -polytopes p is empty implies it = <*> {} ) & ( not (k - 1) -polytopes p is 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)))) ) ) ) );

ex b

( ( (k - 1) -polytopes p is empty implies b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def16 defines incidence-sequence POLYFORM:def 16 :

for p being polyhedron

for k being Integer

for x being Element of (k - 1) -polytopes p

for v being Element of (k -chain-space p)

for b_{5} being FinSequence of Z_2 holds

( b_{5} = incidence-sequence (x,v) iff ( ( (k - 1) -polytopes p is empty implies b_{5} = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b_{5} = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds

b_{5} . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ) );

for p being polyhedron

for k being Integer

for x being Element of (k - 1) -polytopes p

for v being Element of (k -chain-space p)

for b

( b

b

theorem Th35: :: POLYFORM:37

for p being polyhedron

for k being Integer

for c, d being Element of (k -chain-space p)

for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)

for k being Integer

for c, d being Element of (k -chain-space p)

for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)

proof end;

theorem Th36: :: POLYFORM:38

for p being polyhedron

for k being Integer

for c, d being Element of (k -chain-space p)

for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))

for k being Integer

for c, d being Element of (k -chain-space p)

for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))

proof end;

theorem Th37: :: POLYFORM:39

for p being polyhedron

for k being Integer

for c, d being Element of (k -chain-space p)

for x being Element of (k - 1) -polytopes p holds Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))

for k being Integer

for c, d being Element of (k -chain-space p)

for x being Element of (k - 1) -polytopes p holds Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))

proof end;

theorem Th38: :: POLYFORM:40

for p being polyhedron

for k being Integer

for c, d being Element of (k -chain-space p)

for x being Element of (k - 1) -polytopes p holds Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))

for k being Integer

for c, d being Element of (k -chain-space p)

for x being Element of (k - 1) -polytopes p holds Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))

proof end;

theorem Th39: :: POLYFORM:41

for p being polyhedron

for k being Integer

for c being Element of (k -chain-space p)

for a being Element of Z_2

for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)

for k being Integer

for c being Element of (k -chain-space p)

for a being Element of Z_2

for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)

proof end;

theorem Th40: :: POLYFORM:42

for p being polyhedron

for k being Integer

for c being Element of (k -chain-space p)

for a being Element of Z_2

for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))

for k being Integer

for c being Element of (k -chain-space p)

for a being Element of Z_2

for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))

proof end;

theorem Th41: :: POLYFORM:43

for p being polyhedron

for k being Integer

for c, d being Element of (k -chain-space p) holds

( c = d iff for x being Element of k -polytopes p holds c @ x = d @ x )

for k being Integer

for c, d being Element of (k -chain-space p) holds

( c = d iff for x being Element of k -polytopes p holds c @ x = d @ x )

proof end;

theorem Th42: :: POLYFORM:44

for p being polyhedron

for k being Integer

for c, d being Element of (k -chain-space p) holds

( c = d iff for x being Element of k -polytopes p holds

( x in c iff x in d ) )

for k being Integer

for c, d being Element of (k -chain-space p) holds

( c = d iff for x being Element of k -polytopes p holds

( x in c iff x in d ) )

proof end;

scheme :: POLYFORM:sch 1

ChainEx{ F_{1}() -> polyhedron, F_{2}() -> Integer, P_{1}[ Element of F_{2}() -polytopes F_{1}()] } :

ChainEx{ F

ex c being Subset of (F_{2}() -polytopes F_{1}()) st

for x being Element of F_{2}() -polytopes F_{1}() holds

( x in c iff ( P_{1}[x] & x in F_{2}() -polytopes F_{1}() ) )

for x being Element of F

( x in c iff ( P

proof 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.

:: (k-1)-polytopes that are on the "perimeter" of v. Being on the

:: perimeter amounts the sum of the incidence sequence being non-zero,

:: i.e., being equal to 1.

definition

let p be polyhedron;

let k be Integer;

let v be Element of (k -chain-space p);

ex b_{1} being Element of ((k - 1) -chain-space p) st

( ( (k - 1) -polytopes p is empty implies b_{1} = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds

( x in b_{1} iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) )

for b_{1}, b_{2} being Element of ((k - 1) -chain-space p) st ( (k - 1) -polytopes p is empty implies b_{1} = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds

( x in b_{1} iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) & ( (k - 1) -polytopes p is empty implies b_{2} = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds

( x in b_{2} iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) holds

b_{1} = b_{2}

end;
let k be Integer;

let v be Element of (k -chain-space p);

func Boundary v -> Element of ((k - 1) -chain-space p) means :Def17: :: POLYFORM:def 17

( ( (k - 1) -polytopes p is empty implies it = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds

( x in it iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) );

existence ( ( (k - 1) -polytopes p is empty implies it = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds

( x in it iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) );

ex b

( ( (k - 1) -polytopes p is empty implies b

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def17 defines Boundary POLYFORM:def 17 :

for p being polyhedron

for k being Integer

for v being Element of (k -chain-space p)

for b_{4} being Element of ((k - 1) -chain-space p) holds

( b_{4} = Boundary v iff ( ( (k - 1) -polytopes p is empty implies b_{4} = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds

( x in b_{4} iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) ) );

for p being polyhedron

for k being Integer

for v being Element of (k -chain-space p)

for b

( b

( x in b

theorem Th43: :: POLYFORM:45

for p being polyhedron

for k being Integer

for c being Element of (k -chain-space p)

for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))

for k being Integer

for c being Element of (k -chain-space p)

for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))

proof end;

:: Every dimension k has its own boundary operation.

definition

let p be polyhedron;

let k be Integer;

ex b_{1} being Function of (k -chain-space p),((k - 1) -chain-space p) st

for c being Element of (k -chain-space p) holds b_{1} . c = Boundary c

for b_{1}, b_{2} being Function of (k -chain-space p),((k - 1) -chain-space p) st ( for c being Element of (k -chain-space p) holds b_{1} . c = Boundary c ) & ( for c being Element of (k -chain-space p) holds b_{2} . c = Boundary c ) holds

b_{1} = b_{2}

end;
let k be Integer;

func k -boundary p -> Function of (k -chain-space p),((k - 1) -chain-space p) means :Def18: :: POLYFORM:def 18

for c being Element of (k -chain-space p) holds it . c = Boundary c;

existence for c being Element of (k -chain-space p) holds it . c = Boundary c;

ex b

for c being Element of (k -chain-space p) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def18 defines -boundary POLYFORM:def 18 :

for p being polyhedron

for k being Integer

for b_{3} being Function of (k -chain-space p),((k - 1) -chain-space p) holds

( b_{3} = k -boundary p iff for c being Element of (k -chain-space p) holds b_{3} . c = Boundary c );

for p being polyhedron

for k being Integer

for b

( b

theorem Th44: :: POLYFORM:46

for p being polyhedron

for k being Integer

for c, d being Element of (k -chain-space p) holds Boundary (c + d) = (Boundary c) + (Boundary d)

for k being Integer

for c, d being Element of (k -chain-space p) holds Boundary (c + d) = (Boundary c) + (Boundary d)

proof end;

theorem Th45: :: POLYFORM:47

for p being polyhedron

for k being Integer

for a being Element of Z_2

for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)

for k being Integer

for a being Element of Z_2

for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)

proof end;

:: As defined, the k-boundary operator gives rise to a linear

:: transformation.

:: transformation.

theorem Th46: :: POLYFORM:48

for p being polyhedron

for k being Integer holds k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)

for k being Integer holds k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)

proof end;

registration

let p be polyhedron;

let k be Integer;

coherence

( k -boundary p is homogeneous & k -boundary p is additive ) by Th46;

end;
let k be Integer;

coherence

( k -boundary p is homogeneous & k -boundary p is additive ) by Th46;

:: The term "circuit" is used in Lakatos. (A more customary term is

:: "cycle".)

:: "cycle".)

definition

let p be polyhedron;

let k be Integer;

ker (k -boundary p) is Subspace of k -chain-space p ;

end;
let k be Integer;

func k -circuit-space p -> Subspace of k -chain-space p equals :: POLYFORM:def 19

ker (k -boundary p);

coherence ker (k -boundary p);

ker (k -boundary p) is Subspace of k -chain-space p ;

:: deftheorem defines -circuit-space POLYFORM:def 19 :

for p being polyhedron

for k being Integer holds k -circuit-space p = ker (k -boundary p);

for p being polyhedron

for k being Integer holds k -circuit-space p = ker (k -boundary p);

definition

let p be polyhedron;

let k be Integer;

[#] (k -circuit-space p) is non empty Subset of (k -chains p) by VECTSP_4:def 2;

end;
let k be Integer;

func k -circuits p -> non empty Subset of (k -chains p) equals :: POLYFORM:def 20

[#] (k -circuit-space p);

coherence [#] (k -circuit-space p);

[#] (k -circuit-space p) is non empty Subset of (k -chains p) by VECTSP_4:def 2;

:: deftheorem defines -circuits POLYFORM:def 20 :

for p being polyhedron

for k being Integer holds k -circuits p = [#] (k -circuit-space p);

for p being polyhedron

for k being Integer holds k -circuits p = [#] (k -circuit-space p);

definition

let p be polyhedron;

let k be Integer;

im ((k + 1) -boundary p) is Subspace of k -chain-space p ;

end;
let k be Integer;

func k -bounding-chain-space p -> Subspace of k -chain-space p equals :: POLYFORM:def 21

im ((k + 1) -boundary p);

coherence im ((k + 1) -boundary p);

im ((k + 1) -boundary p) is Subspace of k -chain-space p ;

:: deftheorem defines -bounding-chain-space POLYFORM:def 21 :

for p being polyhedron

for k being Integer holds k -bounding-chain-space p = im ((k + 1) -boundary p);

for p being polyhedron

for k being Integer holds k -bounding-chain-space p = im ((k + 1) -boundary p);

definition

let p be polyhedron;

let k be Integer;

[#] (k -bounding-chain-space p) is non empty Subset of (k -chains p) by VECTSP_4:def 2;

end;
let k be Integer;

func k -bounding-chains p -> non empty Subset of (k -chains p) equals :: POLYFORM:def 22

[#] (k -bounding-chain-space p);

coherence [#] (k -bounding-chain-space p);

[#] (k -bounding-chain-space p) is non empty Subset of (k -chains p) by VECTSP_4:def 2;

:: deftheorem defines -bounding-chains POLYFORM:def 22 :

for p being polyhedron

for k being Integer holds k -bounding-chains p = [#] (k -bounding-chain-space p);

for p being polyhedron

for k being Integer holds k -bounding-chains p = [#] (k -bounding-chain-space p);

definition

let p be polyhedron;

let k be Integer;

(k -bounding-chain-space p) /\ (k -circuit-space p) is Subspace of k -chain-space p ;

end;
let 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);

coherence (k -bounding-chain-space p) /\ (k -circuit-space p);

(k -bounding-chain-space p) /\ (k -circuit-space p) is Subspace of k -chain-space p ;

:: deftheorem defines -bounding-circuit-space POLYFORM:def 23 :

for p being polyhedron

for k being Integer holds k -bounding-circuit-space p = (k -bounding-chain-space p) /\ (k -circuit-space p);

for p being polyhedron

for k being Integer holds k -bounding-circuit-space p = (k -bounding-chain-space p) /\ (k -circuit-space p);

definition

let p be polyhedron;

let k be Integer;

[#] (k -bounding-circuit-space p) is non empty Subset of (k -chains p) by VECTSP_4:def 2;

end;
let k be Integer;

func k -bounding-circuits p -> non empty Subset of (k -chains p) equals :: POLYFORM:def 24

[#] (k -bounding-circuit-space p);

coherence [#] (k -bounding-circuit-space p);

[#] (k -bounding-circuit-space p) is non empty Subset of (k -chains p) by VECTSP_4:def 2;

:: deftheorem defines -bounding-circuits POLYFORM:def 24 :

for p being polyhedron

for k being Integer holds k -bounding-circuits p = [#] (k -bounding-circuit-space p);

for p being polyhedron

for k being Integer holds k -bounding-circuits p = [#] (k -bounding-circuit-space p);

theorem :: POLYFORM:49

for p being polyhedron

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

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

:: The property of being simply connected is that circuits are

:: bounding, and vice versa (any bounding chain is a circuit).

:: bounding, and vice versa (any bounding chain is a circuit).

definition

let p be polyhedron;

end;
attr p is simply-connected means :: POLYFORM:def 25

for k being Integer holds k -circuits p = k -bounding-chains p;

for k being Integer holds k -circuits p = k -bounding-chains p;

:: deftheorem defines simply-connected POLYFORM:def 25 :

for p being polyhedron holds

( p is simply-connected iff for k being Integer holds k -circuits p = k -bounding-chains p );

for p being polyhedron holds

( p is simply-connected iff for k being Integer holds k -circuits p = k -bounding-chains p );

theorem Th48: :: POLYFORM:50

for p being polyhedron holds

( p is simply-connected iff for n being Integer holds n -circuit-space p = n -bounding-chain-space p )

( p is simply-connected iff for n being Integer holds n -circuit-space p = n -bounding-chain-space p )

proof end;

definition

let p be polyhedron;

ex b_{1} being FinSequence of INT st

( len b_{1} = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds

b_{1} . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) )

for b_{1}, b_{2} being FinSequence of INT st len b_{1} = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds

b_{1} . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) & len b_{2} = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds

b_{2} . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) holds

b_{1} = b_{2}

end;
func alternating-f-vector p -> FinSequence of INT means :Def26: :: 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))) ) );

existence ( 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))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def26 defines alternating-f-vector POLYFORM:def 26 :

for p being polyhedron

for b_{2} being FinSequence of INT holds

( b_{2} = alternating-f-vector p iff ( len b_{2} = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds

b_{2} . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) ) );

for p being polyhedron

for b

( b

b

definition

let p be polyhedron;

ex b_{1} being FinSequence of INT st

( len b_{1} = dim p & ( for k being Nat st 1 <= k & k <= dim p holds

b_{1} . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )

for b_{1}, b_{2} being FinSequence of INT st len b_{1} = dim p & ( for k being Nat st 1 <= k & k <= dim p holds

b_{1} . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len b_{2} = dim p & ( for k being Nat st 1 <= k & k <= dim p holds

b_{2} . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) holds

b_{1} = b_{2}

end;
func alternating-proper-f-vector p -> FinSequence of INT means :Def27: :: 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))) ) );

existence ( 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))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def27 defines alternating-proper-f-vector POLYFORM:def 27 :

for p being polyhedron

for b_{2} being FinSequence of INT holds

( b_{2} = alternating-proper-f-vector p iff ( len b_{2} = dim p & ( for k being Nat st 1 <= k & k <= dim p holds

b_{2} . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) );

for p being polyhedron

for b

( b

b

definition

let p be polyhedron;

ex b_{1} being FinSequence of INT st

( len b_{1} = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds

b_{1} . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )

for b_{1}, b_{2} being FinSequence of INT st len b_{1} = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds

b_{1} . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len b_{2} = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds

b_{2} . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) holds

b_{1} = b_{2}

end;
func alternating-semi-proper-f-vector p -> FinSequence of INT means :Def28: :: 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))) ) );

existence ( 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))) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def28 defines alternating-semi-proper-f-vector POLYFORM:def 28 :

for p being polyhedron

for b_{2} being FinSequence of INT holds

( b_{2} = alternating-semi-proper-f-vector p iff ( len b_{2} = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds

b_{2} . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) );

for p being polyhedron

for b

( b

b

theorem Th49: :: POLYFORM:51

for p being polyhedron

for n being Nat st 1 <= n & n <= len (alternating-proper-f-vector p) holds

(alternating-proper-f-vector p) . n = (((- 1) |^ (n + 1)) * (dim ((n - 2) -bounding-chain-space p))) + (((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p)))

for n being Nat st 1 <= n & n <= len (alternating-proper-f-vector p) holds

(alternating-proper-f-vector p) . n = (((- 1) |^ (n + 1)) * (dim ((n - 2) -bounding-chain-space p))) + (((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p)))

proof end;

:: The term "eulerian" comes from Lakatos.

:: deftheorem defines eulerian POLYFORM:def 29 :

for p being polyhedron holds

( p is eulerian iff Sum (alternating-proper-f-vector p) = 1 + ((- 1) |^ ((dim p) + 1)) );

for p being polyhedron holds

( p is eulerian iff Sum (alternating-proper-f-vector p) = 1 + ((- 1) |^ ((dim p) + 1)) );

theorem Th50: :: POLYFORM:52

for p being polyhedron holds alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>

proof end;

:: Another characterization of Eulerian polyhedra

definition

let p be polyhedron;

compatibility

( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 )

end;
compatibility

( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 )

proof end;

:: deftheorem defines eulerian POLYFORM:def 30 :

for p being polyhedron holds

( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 );

for p being polyhedron holds

( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 );

theorem Th51: :: POLYFORM:53

for p being polyhedron holds alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p)

proof end;

:: Yet another characterization of eulerian polyhedra

definition

let p be polyhedron;

compatibility

( p is eulerian iff Sum (alternating-f-vector p) = 0 )

end;
compatibility

( p is eulerian iff Sum (alternating-f-vector p) = 0 )

proof end;

:: deftheorem defines eulerian POLYFORM:def 31 :

for p being polyhedron holds

( p is eulerian iff Sum (alternating-f-vector p) = 0 );

for p being polyhedron holds

( p is eulerian iff Sum (alternating-f-vector p) = 0 );

theorem Th55: :: POLYFORM:57

for p being polyhedron

for k being Integer

for x being Element of k -polytopes p

for e being Element of (k - 1) -polytopes p st k = 0 & e = {} holds

incidence-value (e,x) = 1. Z_2

for k being Integer

for x being Element of k -polytopes p

for e being Element of (k - 1) -polytopes p st k = 0 & e = {} holds

incidence-value (e,x) = 1. Z_2

proof end;

theorem Th56: :: POLYFORM:58

for p being polyhedron

for k being Integer

for x being Element of k -polytopes p

for v being Element of (k -chain-space p)

for e being Element of (k - 1) -polytopes p

for n being Nat st k = 0 & 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

for k being Integer

for x being Element of k -polytopes p

for v being Element of (k -chain-space p)

for e being Element of (k - 1) -polytopes p

for n being Nat st k = 0 & 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 end;

theorem Th57: :: POLYFORM:59

for p being polyhedron

for k being Integer

for x being Element of k -polytopes p

for e being Element of (k - 1) -polytopes p

for v being Element of (k -chain-space p)

for m, n being Nat st k = 0 & 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

for k being Integer

for x being Element of k -polytopes p

for e being Element of (k - 1) -polytopes p

for v being Element of (k -chain-space p)

for m, n being Nat st k = 0 & 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 end;

theorem Th58: :: POLYFORM:60

for p being polyhedron

for k being Integer

for x being Element of k -polytopes p

for v being Element of (k -chain-space p)

for e being Element of (k - 1) -polytopes p st k = 0 & v = {x} & e = {} holds

Sum (incidence-sequence (e,v)) = 1. Z_2

for k being Integer

for x being Element of k -polytopes p

for v being Element of (k -chain-space p)

for e being Element of (k - 1) -polytopes p st k = 0 & v = {x} & e = {} holds

Sum (incidence-sequence (e,v)) = 1. Z_2

proof end;

theorem Th66: :: POLYFORM:68

for p being polyhedron

for x being Element of ((dim p) -chain-space p) holds

( x = 0. ((dim p) -chain-space p) or x = {p} )

for x being Element of ((dim p) -chain-space p) holds

( x = 0. ((dim p) -chain-space p) or x = {p} )

proof end;

theorem Th67: :: POLYFORM:69

for p being polyhedron

for x, y being Element of ((dim p) -chain-space p) holds

( not x <> y or x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )

for x, y being Element of ((dim p) -chain-space p) holds

( not x <> y or x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )

proof end;

theorem Th70: :: POLYFORM:72

for p being polyhedron

for c being Element of ((dim p) -chain-space p)

for x being Element of (dim p) -polytopes p st c = {p} holds

c @ x = 1. Z_2

for c being Element of ((dim p) -chain-space p)

for x being Element of (dim p) -polytopes p st c = {p} holds

c @ x = 1. Z_2

proof end;

theorem Th71: :: POLYFORM:73

for p being polyhedron

for x being Element of ((dim p) - 1) -polytopes p

for c being Element of (dim p) -polytopes p st c = p holds

incidence-value (x,c) = 1. Z_2

for x being Element of ((dim p) - 1) -polytopes p

for c being Element of (dim p) -polytopes p st c = p holds

incidence-value (x,c) = 1. Z_2

proof end;

theorem Th72: :: POLYFORM:74

for p being polyhedron

for x being Element of ((dim p) - 1) -polytopes p

for c being Element of ((dim p) -chain-space p) st c = {p} holds

incidence-sequence (x,c) = <*(1. Z_2)*>

for x being Element of ((dim p) - 1) -polytopes p

for c being Element of ((dim p) -chain-space p) st c = {p} holds

incidence-sequence (x,c) = <*(1. Z_2)*>

proof end;

theorem Th73: :: POLYFORM:75

for p being polyhedron

for x being Element of ((dim p) - 1) -polytopes p

for c being Element of ((dim p) -chain-space p) st c = {p} holds

Sum (incidence-sequence (x,c)) = 1. Z_2

for x being Element of ((dim p) - 1) -polytopes p

for c being Element of ((dim p) -chain-space p) st c = {p} holds

Sum (incidence-sequence (x,c)) = 1. Z_2

proof 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.

:: 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 Th78: :: POLYFORM:80

for p being polyhedron

for n being Nat st 1 < n & n < (dim p) + 2 holds

(alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)

for n being Nat st 1 < n & n < (dim p) + 2 holds

(alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)

proof end;

theorem Th79: :: POLYFORM:81

for p being polyhedron holds alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>

proof end;

theorem Th80: :: POLYFORM:82

for p being polyhedron st dim p is odd holds

Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2

Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2

proof end;

theorem Th81: :: POLYFORM:83

for p being polyhedron st dim p is even holds

Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p)

Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p)

proof end;

theorem Th83: :: POLYFORM:85

for p being polyhedron st dim p = 2 holds

Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1))

Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1))

proof end;

theorem Th84: :: POLYFORM:86

for p being polyhedron st dim p = 3 holds

Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2))

Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2))

proof end;

:: A trivial special case

:: Euler's Polyhedron Formula in One Dimension: simply-connected

:: 1-dimensional polyhedra are just line segments.

:: 1-dimensional polyhedra are just line segments.

:: Euler's Polyhedron Formula in Two Dimensions: polygons have exactly

:: as many vertices as edges.

:: as many vertices as edges.

theorem :: POLYFORM:91

for p being polyhedron st p is simply-connected & dim p = 3 holds

((num-vertices p) - (num-edges p)) + (num-faces p) = 2

((num-vertices p) - (num-edges p)) + (num-faces p) = 2

proof end;