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