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

begin

theorem Th1: :: POLYFORM:1

for X, c, d being set st ex a, b being set st
( a <> b & X = {a,b} ) & c in X & d in X & c <> d holds
X = {c,d}

proof end;

theorem Th2: :: POLYFORM:2

for f being Function st f is one-to-one holds
card (dom f) = card (rng f)

proof end;

begin

theorem Th3: :: POLYFORM:3

for k being Integer st 1 <= k holds
k is Nat

proof end;

definition

let a be Integer;
let b be Nat;
:: original: *
redefine func a * b -> Element of INT ;
coherence
a * b is Element of INT by INT_1:def 2;

end;

theorem Th4: :: POLYFORM:4

not 1 is even

proof end;

theorem Th5: :: POLYFORM:5

2 is even

proof end;

theorem Th6: :: POLYFORM:6

not 3 is even

proof end;

theorem Th7: :: POLYFORM:7

4 is even

proof end;

theorem Th8: :: POLYFORM:8

for n being Nat st n is even holds
(- 1) |^ n = 1

proof end;

theorem Th9: :: POLYFORM:9

for n being Nat st not n is even holds
(- 1) |^ n = - 1

proof end;

theorem Th10: :: POLYFORM:10

for n being Nat holds (- 1) |^ n is Integer

proof end;

definition

let a be Integer;
let n be Nat;
:: original: |^
redefine func a |^ n -> Element of INT ;
coherence
a |^ n is Element of INT

proof end;

end;

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

theorem Th11: :: POLYFORM:11

for p, q, r being FinSequence holds len (p ^ q) <= len (p ^ (q ^ r))

proof end;

theorem Th12: :: POLYFORM:12

for n being Nat holds 1 < n + 2

proof end;

theorem Th13: :: POLYFORM:13

(- 1) |^ 2 = 1

proof end;

theorem Th14: :: POLYFORM:14

for n being Nat holds (- 1) |^ n = (- 1) |^ (n + 2)

proof end;

begin

registration

let f be FinSequence of INT ;
let k be Nat;
cluster f . k -> integer ;
coherence
f . k is integer ;

end;

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

proof end;

theorem Th16: :: POLYFORM:16

for p, q, r being FinSequence holds len ((p ^ q) ^ r) = ((len p) + (len q)) + (len r)

proof end;

theorem Th17: :: POLYFORM:17

for x being set
for p, q being FinSequence holds ((<*x*> ^ p) ^ q) . 1 = x

proof end;

theorem Th18: :: POLYFORM:18

for x being set
for p, q being FinSequence holds ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x

proof end;

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

proof end;

definition

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

proof end;

end;

definition

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

proof end;

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

proof end;

end;

definition

let p, q be FinSequence of INT ;
:: original: ^
redefine func p ^ q -> FinSequence of INT ;
coherence
p ^ q is FinSequence of INT by FINSEQ_1:96;

end;

theorem :: POLYFORM:20

canceled;

theorem Th21: :: POLYFORM:21

for k being Integer
for p being FinSequence of INT holds Sum (<*k*> ^ p) = k + (Sum p)

proof end;

theorem Th22: :: POLYFORM:22

for p, q, r being FinSequence of INT holds Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r)

proof end;

theorem :: POLYFORM:23

for a being Element of Z_2 holds Sum <*a*> = a by FINSOP_1:12;

begin

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 Th24: :: POLYFORM:24

for X, Y being set holds [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y

proof end;

definition

attr c₁ is strict ;
struct PolyhedronStr -> ;
aggr PolyhedronStr(# PolytopsF, IncidenceF #) -> PolyhedronStr ;
sel PolytopsF c₁ -> FinSequence-yielding FinSequence;
sel IncidenceF c₁ -> Function-yielding FinSequence;

end;

definition

let p be PolyhedronStr ;
attr p is polyhedron_1 means :Def1: :: POLYFORM:def 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)));
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 );

end;

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

:: deftheorem Def2 defines polyhedron_2 POLYFORM:def 2 :
for p being PolyhedronStr holds
( p is polyhedron_2 iff for n being Nat st 1 <= n & 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 ) );

registration

cluster polyhedron_1 polyhedron_2 polyhedron_3 PolyhedronStr ;
existence
ex b₁ being PolyhedronStr st
( b₁ is polyhedron_1 & b₁ is polyhedron_2 & b₁ is polyhedron_3 )

proof end;

end;

definition

mode polyhedron is polyhedron_1 polyhedron_2 polyhedron_3 PolyhedronStr ;

end;

definition

let p be polyhedron;
func dim p -> Element of NAT equals :: POLYFORM:def 4
len the PolytopsF of p;
coherence
len the PolytopsF of p is Element of NAT ;

end;

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

definition

let p be polyhedron;
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
ex b₁ being finite set st
( ( k < - 1 implies b₁ = {} ) & ( k = - 1 implies b₁ = {{}} ) & ( - 1 < k & k < dim p implies b₁ = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b₁ = {p} ) & ( k > dim p implies b₁ = {} ) )

proof end;

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

proof end;

end;

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

theorem Th25: :: POLYFORM:25

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 )

proof end;

theorem Th26: :: POLYFORM:26

for p being polyhedron
for k being Integer holds
( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )

proof end;

theorem :: POLYFORM:27

for p being polyhedron
for k being Integer st k < dim p holds
k - 1 < dim p by XREAL_1:148, XXREAL_0:2;

definition

let p be polyhedron;
let k be Integer;
func eta (p,k) -> incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) means :Def6: :: POLYFORM:def 6
( ( k < 0 implies it = {} ) & ( 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
ex b₁ being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b₁ = {} ) & ( k = 0 implies b₁ = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b₁ = the IncidenceF of p . k ) & ( k = dim p implies b₁ = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b₁ = {} ) )

proof end;

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

proof end;

end;

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

definition

let p be polyhedron;
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
ex b₁ being FinSequence st
( ( k < - 1 implies b₁ = <*> {} ) & ( k = - 1 implies b₁ = <*{}*> ) & ( - 1 < k & k < dim p implies b₁ = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b₁ = <*p*> ) & ( k > dim p implies b₁ = <*> {} ) )

proof end;

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

proof end;

end;

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

definition

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

end;

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

definition

let p be polyhedron;
func num-vertices p -> Element of NAT equals :: POLYFORM:def 9
num-polytopes (p,0);
correctness
coherence
num-polytopes (p,0) is Element of NAT ;
;
func num-edges p -> Element of NAT equals :: POLYFORM:def 10
num-polytopes (p,1);
correctness
coherence
num-polytopes (p,1) is Element of NAT ;
;
func num-faces p -> Element of NAT equals :: POLYFORM:def 11
num-polytopes (p,2);
correctness
coherence
num-polytopes (p,2) is Element of NAT ;
;

end;

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

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

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

theorem Th28: :: POLYFORM:28

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

proof end;

theorem Th29: :: POLYFORM:29

for p being polyhedron
for k being Integer holds len (k -polytope-seq p) = num-polytopes (p,k)

proof end;

theorem Th30: :: POLYFORM:30

for p being polyhedron
for k being Integer holds rng (k -polytope-seq p) = k -polytopes p

proof end;

theorem Th31: :: POLYFORM:31

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

proof end;

theorem Th32: :: POLYFORM:32

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

proof end;

definition

let p be polyhedron;
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 is Element of k -polytopes p

proof end;

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;

theorem Th33: :: POLYFORM:33

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

proof end;

theorem Th34: :: POLYFORM:34

for p being polyhedron
for k being Integer holds k -polytope-seq p is one-to-one

proof end;

theorem Th35: :: POLYFORM:35

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

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 ;
func incidence-value (x,y) -> Element of Z_2 equals :Def13: :: POLYFORM:def 13
(eta (p,k)) . (x,y);
coherence
(eta (p,k)) . (x,y) is Element of Z_2

proof end;

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

begin

definition

let p be polyhedron;
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) is finite-dimensional VectSp of Z_2 ;

end;

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

theorem :: POLYFORM:36

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

theorem Th37: :: POLYFORM:37

for p being polyhedron
for k being Integer holds num-polytopes (p,k) = dim (k -chain-space p)

proof end;

definition

let p be polyhedron;
let k be Integer;
func k -chains p -> non empty finite set equals :: POLYFORM:def 15
bool (k -polytopes p);
coherence
bool (k -polytopes p) is non empty finite set ;

end;

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

definition

let p be polyhedron;
let k be Integer;
let x be Element of (k - 1) -polytopes p;
let v be Element of (k -chain-space p);
func incidence-sequence (x,v) -> FinSequence of Z_2 means :Def16: :: POLYFORM:def 16
( ( (k - 1) -polytopes p is empty implies it = <*> {} ) & ( 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
ex b₁ being FinSequence of Z_2 st
( ( (k - 1) -polytopes p is empty implies b₁ = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b₁ = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b₁ . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of Z_2 st ( (k - 1) -polytopes p is empty implies b₁ = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b₁ = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b₁ . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) & ( (k - 1) -polytopes p is empty implies b₂ = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b₂ = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b₂ . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) holds
b₁ = b₂

proof end;

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₅ being FinSequence of Z_2 holds
( b₅ = incidence-sequence (x,v) iff ( ( (k - 1) -polytopes p is empty implies b₅ = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b₅ = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b₅ . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ) );

theorem Th38: :: POLYFORM:38

for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p)
for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)

proof end;

theorem Th39: :: POLYFORM:39

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

proof end;

theorem Th40: :: POLYFORM:40

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

proof end;

theorem Th41: :: POLYFORM:41

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

proof end;

theorem Th42: :: POLYFORM:42

for p being polyhedron
for k being Integer
for c being Element of (k -chain-space p)
for a being Element of Z_2
for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)

proof end;

theorem Th43: :: POLYFORM:43

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

proof end;

theorem Th44: :: POLYFORM:44

for p being polyhedron
for k being Integer
for c, d being Element of (k -chain-space p) holds
( c = d iff for x being Element of k -polytopes p holds c @ x = d @ x )

proof end;

theorem Th45: :: POLYFORM:45

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

proof end;

scheme :: POLYFORM:sch 1
ChainEx{ F₁() -> polyhedron, F₂() -> Integer, P₁[ Element of F₂() -polytopes F₁()] } :

ex c being Subset of (F₂() -polytopes F₁()) st
for x being Element of F₂() -polytopes F₁() holds
( x in c iff ( P₁[x] & x in F₂() -polytopes F₁() ) )

proof end;

definition

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

proof end;

uniqueness
for b₁, b₂ being Element of ((k - 1) -chain-space p) st ( (k - 1) -polytopes p is empty implies b₁ = 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₁ iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) & ( (k - 1) -polytopes p is empty implies b₂ = 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₂ iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) holds
b₁ = b₂

proof end;

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₄ being Element of ((k - 1) -chain-space p) holds
( b₄ = Boundary v iff ( ( (k - 1) -polytopes p is empty implies b₄ = 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₄ iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) ) );

theorem Th46: :: POLYFORM:46

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

proof end;

definition

let p be polyhedron;
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
ex b₁ being Function of (k -chain-space p),((k - 1) -chain-space p) st
for c being Element of (k -chain-space p) holds b₁ . c = Boundary c

proof end;

uniqueness
for b₁, b₂ being Function of (k -chain-space p),((k - 1) -chain-space p) st ( for c being Element of (k -chain-space p) holds b₁ . c = Boundary c ) & ( for c being Element of (k -chain-space p) holds b₂ . c = Boundary c ) holds
b₁ = b₂

proof end;

end;

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

theorem Th47: :: POLYFORM:47

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)

proof end;

theorem Th48: :: POLYFORM:48

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)

proof end;

theorem Th49: :: POLYFORM:49

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)

proof end;

registration

let p be polyhedron;
let k be Integer;
cluster k -boundary p -> homogeneous additive ;
coherence
( k -boundary p is homogeneous & k -boundary p is additive ) by Th49;

end;

definition

let p be polyhedron;
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) is Subspace of k -chain-space p ;

end;

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

definition

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

end;

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

definition

let p be polyhedron;
let k be Integer;
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) is Subspace of k -chain-space p ;

end;

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

definition

let p be polyhedron;
let k be Integer;
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) is non empty Subset of (k -chains p) by VECTSP_4:def 2;

end;

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

definition

let p be polyhedron;
let k be Integer;
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) is Subspace of k -chain-space p ;

end;

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

definition

let p be polyhedron;
let k be Integer;
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) is non empty Subset of (k -chains p) by VECTSP_4:def 2;

end;

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

theorem :: POLYFORM:50

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

begin

definition

let p be polyhedron;
attr p is simply-connected means :Def25: :: POLYFORM:def 25
for k being Integer holds k -circuits p = k -bounding-chains p;

end;

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

theorem Th51: :: POLYFORM:51

for p being polyhedron holds
( 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;
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
ex b₁ being FinSequence of INT st
( len b₁ = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b₁ . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of INT st len b₁ = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b₁ . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) & len b₂ = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b₂ . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) holds
b₁ = b₂

proof end;

end;

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

definition

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

proof end;

uniqueness
for b₁, b₂ being FinSequence of INT st len b₁ = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
b₁ . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len b₂ = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
b₂ . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) holds
b₁ = b₂

proof end;

end;

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

definition

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

proof end;

uniqueness
for b₁, b₂ being FinSequence of INT st len b₁ = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
b₁ . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len b₂ = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
b₂ . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) holds
b₁ = b₂

proof end;

end;

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

theorem Th52: :: POLYFORM:52

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

proof end;

definition

let p be polyhedron;
attr p is eulerian means :Def29: :: POLYFORM:def 29
Sum (alternating-proper-f-vector p) = 1 + ((- 1) |^ ((dim p) + 1));

end;

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

theorem Th53: :: POLYFORM:53

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

proof end;

definition

let p be polyhedron;
redefine attr p is eulerian means :Def30: :: POLYFORM:def 30
Sum (alternating-semi-proper-f-vector p) = 1;
compatibility
( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 )

proof end;

end;

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

theorem Th54: :: POLYFORM:54

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

proof end;

definition

let p be polyhedron;
redefine attr p is eulerian means :Def31: :: POLYFORM:def 31
Sum (alternating-f-vector p) = 0 ;
compatibility
( p is eulerian iff Sum (alternating-f-vector p) = 0 )

proof end;

end;

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

begin

theorem Th55: :: POLYFORM:55

for p being polyhedron holds not 0 -polytopes p is empty

proof end;

theorem Th56: :: POLYFORM:56

for p being polyhedron holds card ([#] ((- 1) -chain-space p)) = 2

proof end;

theorem Th57: :: POLYFORM:57

for p being polyhedron holds [#] ((- 1) -chain-space p) = {{},{{}}}

proof end;

theorem Th58: :: POLYFORM:58

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

proof end;

theorem Th59: :: POLYFORM:59

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

proof end;

theorem Th60: :: POLYFORM:60

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

proof end;

theorem Th61: :: POLYFORM:61

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

proof end;

theorem Th62: :: POLYFORM:62

for p being polyhedron
for x being Element of 0 -polytopes p holds (0 -boundary p) . {x} = {{}}

proof end;

theorem Th63: :: POLYFORM:63

for p being polyhedron
for k being Integer st k = - 1 holds
dim (k -bounding-chain-space p) = 1

proof end;

theorem Th64: :: POLYFORM:64

for p being polyhedron holds card ([#] ((dim p) -chain-space p)) = 2

proof end;

theorem Th65: :: POLYFORM:65

for p being polyhedron holds {p} is Element of ((dim p) -chain-space p)

proof end;

theorem Th66: :: POLYFORM:66

for p being polyhedron holds {p} in [#] ((dim p) -chain-space p)

proof end;

theorem Th67: :: POLYFORM:67

for p being polyhedron holds not ((dim p) - 1) -polytopes p is empty

proof end;

registration

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

end;

theorem Th68: :: POLYFORM:68

for p being polyhedron holds [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}}

proof end;

theorem Th69: :: POLYFORM:69

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

proof end;

theorem Th70: :: POLYFORM:70

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

proof end;

theorem :: POLYFORM:71

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

theorem Th72: :: POLYFORM:72

for p being polyhedron holds 1 -th-polytope (p,(dim p)) = p

proof end;

theorem Th73: :: POLYFORM:73

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

proof end;

theorem Th74: :: POLYFORM:74

for p being polyhedron
for x being Element of ((dim p) - 1) -polytopes p
for c being Element of (dim p) -polytopes p st c = p holds
incidence-value (x,c) = 1. Z_2

proof end;

theorem Th75: :: POLYFORM:75

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

proof end;

theorem Th76: :: POLYFORM:76

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

proof end;

theorem Th77: :: POLYFORM:77

for p being polyhedron holds ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p

proof end;

theorem Th78: :: POLYFORM:78

for p being polyhedron holds (dim p) -boundary p is one-to-one

proof end;

theorem Th79: :: POLYFORM:79

for p being polyhedron holds dim (((dim p) - 1) -bounding-chain-space p) = 1

proof end;

theorem Th80: :: POLYFORM:80

for p being polyhedron st p is simply-connected holds
dim (((dim p) - 1) -circuit-space p) = 1

proof end;

theorem Th81: :: POLYFORM:81

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)

proof end;

theorem Th82: :: POLYFORM:82

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

proof end;

begin

theorem Th83: :: POLYFORM:83

for p being polyhedron st not dim p is even holds
Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2

proof end;

theorem Th84: :: POLYFORM:84

for p being polyhedron st dim p is even holds
Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p)

proof end;

theorem Th85: :: POLYFORM:85

for p being polyhedron st dim p = 1 holds
Sum (alternating-proper-f-vector p) = num-polytopes (p,0)

proof end;

theorem Th86: :: POLYFORM:86

for p being polyhedron st dim p = 2 holds
Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1))

proof end;

theorem Th87: :: POLYFORM:87

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

proof end;

theorem Th88: :: POLYFORM:88

for p being polyhedron st dim p = 0 holds
p is eulerian

proof end;

theorem Th89: :: POLYFORM:89

for p being polyhedron st p is simply-connected holds
p is eulerian

proof end;

theorem :: POLYFORM:90

for p being polyhedron st p is simply-connected & dim p = 1 holds
num-vertices p = 2

proof end;

theorem :: POLYFORM:91

for p being polyhedron st p is simply-connected & dim p = 2 holds
num-vertices p = num-edges p

proof end;

theorem :: POLYFORM:92

for p being polyhedron st p is simply-connected & dim p = 3 holds
((num-vertices p) - (num-edges p)) + (num-faces p) = 2

proof end;