begin
theorem Th1:
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}
theorem Th2:
begin
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
Lm1:
for x being Element of NAT st 0 < x holds
0 + 1 <= x
by NAT_1:13;
theorem Th11:
theorem Th12:
for
n being
Nat holds 1
< n + 2
theorem Th13:
theorem Th14:
begin
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem
canceled;
theorem Th21:
theorem Th22:
theorem
begin
theorem Th24:
:: deftheorem Def1 defines polyhedron_1 POLYFORM:def 1 :
:: deftheorem Def2 defines polyhedron_2 POLYFORM:def 2 :
:: deftheorem Def3 defines polyhedron_3 POLYFORM:def 3 :
:: deftheorem defines dim POLYFORM:def 4 :
:: deftheorem Def5 defines -polytopes POLYFORM:def 5 :
theorem Th25:
theorem Th26:
theorem
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:
( (
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 b1 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st
( ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{} },(0 -polytopes p):] --> (1. Z_2 ) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 ) ) & ( k > dim p implies b1 = {} ) )
uniqueness
for b1, b2 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) st ( k < 0 implies b1 = {} ) & ( k = 0 implies b1 = [:{{} },(0 -polytopes p):] --> (1. Z_2 ) ) & ( 0 < k & k < dim p implies b1 = the IncidenceF of p . k ) & ( k = dim p implies b1 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 ) ) & ( k > dim p implies b1 = {} ) & ( k < 0 implies b2 = {} ) & ( k = 0 implies b2 = [:{{} },(0 -polytopes p):] --> (1. Z_2 ) ) & ( 0 < k & k < dim p implies b2 = the IncidenceF of p . k ) & ( k = dim p implies b2 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 ) ) & ( k > dim p implies b2 = {} ) holds
b1 = b2
end;
:: deftheorem Def6 defines eta POLYFORM:def 6 :
:: deftheorem Def7 defines -polytope-seq POLYFORM:def 7 :
:: deftheorem defines num-polytopes POLYFORM:def 8 :
:: deftheorem defines num-vertices POLYFORM:def 9 :
:: deftheorem defines num-edges POLYFORM:def 10 :
:: deftheorem defines num-faces POLYFORM:def 11 :
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem Def12 defines -th-polytope POLYFORM:def 12 :
theorem Th33:
theorem Th34:
theorem Th35:
:: deftheorem Def13 defines incidence-value POLYFORM:def 13 :
begin
:: deftheorem defines -chain-space POLYFORM:def 14 :
theorem
theorem Th37:
:: deftheorem defines -chains POLYFORM:def 15 :
definition
let p be
polyhedron;
let k be
Integer;
let x be
Element of
(k - 1) -polytopes p;
let v be
Element of ;
func incidence-sequence x,
v -> FinSequence of
means :
Def16:
( (
(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 b1 being FinSequence of st
( ( (k - 1) -polytopes p is empty implies b1 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b1 = num-polytopes p,k & ( for n being Nat st 1 <= n & n <= num-polytopes p,k holds
b1 . n = (v @ (n -th-polytope p,k)) * (incidence-value x,(n -th-polytope p,k)) ) ) ) )
uniqueness
for b1, b2 being FinSequence of st ( (k - 1) -polytopes p is empty implies b1 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b1 = num-polytopes p,k & ( for n being Nat st 1 <= n & n <= num-polytopes p,k holds
b1 . n = (v @ (n -th-polytope p,k)) * (incidence-value x,(n -th-polytope p,k)) ) ) ) & ( (k - 1) -polytopes p is empty implies b2 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b2 = num-polytopes p,k & ( for n being Nat st 1 <= n & n <= num-polytopes p,k holds
b2 . n = (v @ (n -th-polytope p,k)) * (incidence-value x,(n -th-polytope p,k)) ) ) ) holds
b1 = b2
end;
:: deftheorem Def16 defines incidence-sequence POLYFORM:def 16 :
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
:: deftheorem Def17 defines Boundary POLYFORM:def 17 :
theorem Th46:
:: deftheorem Def18 defines -boundary POLYFORM:def 18 :
theorem Th47:
theorem Th48:
theorem Th49:
:: deftheorem defines -circuit-space POLYFORM:def 19 :
:: deftheorem defines -circuits POLYFORM:def 20 :
:: deftheorem defines -bounding-chain-space POLYFORM:def 21 :
:: deftheorem defines -bounding-chains POLYFORM:def 22 :
:: deftheorem defines -bounding-circuit-space POLYFORM:def 23 :
:: deftheorem defines -bounding-circuits POLYFORM:def 24 :
theorem
begin
:: deftheorem Def25 defines simply-connected POLYFORM:def 25 :
theorem Th51:
:: deftheorem Def26 defines alternating-f-vector POLYFORM:def 26 :
:: deftheorem Def27 defines alternating-proper-f-vector POLYFORM:def 27 :
:: deftheorem Def28 defines alternating-semi-proper-f-vector POLYFORM:def 28 :
theorem Th52:
:: deftheorem Def29 defines eulerian POLYFORM:def 29 :
theorem Th53:
:: deftheorem Def30 defines eulerian POLYFORM:def 30 :
theorem Th54:
:: deftheorem Def31 defines eulerian POLYFORM:def 31 :
begin
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem
theorem Th72:
theorem Th73:
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem Th78:
theorem Th79:
theorem Th80:
theorem Th81:
theorem Th82:
begin
theorem Th83:
theorem Th84:
theorem Th85:
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem
theorem
theorem