:: Euler's Polyhedron Formula
:: by Jesse Alama
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
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}
theorem Th2: :: POLYFORM:2
theorem Th3: :: POLYFORM:3
theorem Th4: :: POLYFORM:4
theorem Th5: :: POLYFORM:5
theorem Th6: :: POLYFORM:6
theorem Th7: :: POLYFORM:7
theorem Th8: :: POLYFORM:8
theorem Th9: :: POLYFORM:9
theorem Th10: :: POLYFORM:10
Lm1:
for x being Element of NAT st 0 < x holds
0 + 1 <= x
by NAT_1:13;
theorem Th11: :: POLYFORM:11
theorem Th12: :: POLYFORM:12
for
n being
Nat holds 1
< n + 2
theorem Th13: :: POLYFORM:13
theorem Th14: :: POLYFORM:14
theorem Th15: :: POLYFORM:15
theorem Th16: :: POLYFORM:16
theorem Th17: :: POLYFORM:17
theorem Th18: :: POLYFORM:18
theorem Th19: :: POLYFORM:19
theorem Th20: :: POLYFORM:20
theorem Th21: :: POLYFORM:21
theorem Th22: :: POLYFORM:22
theorem :: POLYFORM:23
theorem Th24: :: POLYFORM:24
:: 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: :: POLYFORM:25
theorem Th26: :: POLYFORM:26
theorem Th27: :: POLYFORM:27
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 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: :: POLYFORM:28
theorem Th29: :: POLYFORM:29
theorem Th30: :: POLYFORM:30
theorem Th31: :: POLYFORM:31
theorem Th32: :: POLYFORM:32
:: deftheorem Def12 defines -th-polytope POLYFORM:def 12 :
theorem Th33: :: POLYFORM:33
theorem Th34: :: POLYFORM:34
theorem Th35: :: POLYFORM:35
:: deftheorem Def13 defines incidence-value POLYFORM:def 13 :
:: deftheorem defines -chain-space POLYFORM:def 14 :
theorem :: POLYFORM:36
theorem Th37: :: POLYFORM:37
:: 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
(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 b1 being FinSequence of Z_2 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 Z_2 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: :: POLYFORM:38
theorem Th39: :: POLYFORM:39
theorem Th40: :: POLYFORM:40
theorem Th41: :: POLYFORM:41
theorem Th42: :: POLYFORM:42
theorem Th43: :: POLYFORM:43
theorem Th44: :: POLYFORM:44
theorem Th45: :: POLYFORM:45
:: deftheorem Def17 defines Boundary POLYFORM:def 17 :
theorem Th46: :: POLYFORM:46
:: deftheorem Def18 defines -boundary POLYFORM:def 18 :
theorem Th47: :: POLYFORM:47
theorem Th48: :: POLYFORM:48
theorem Th49: :: POLYFORM:49
:: 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 :: POLYFORM:50
:: deftheorem Def25 defines simply-connected POLYFORM:def 25 :
theorem Th51: :: POLYFORM:51
:: 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: :: POLYFORM:52
:: deftheorem Def29 defines eulerian POLYFORM:def 29 :
theorem Th53: :: POLYFORM:53
:: deftheorem Def30 defines eulerian POLYFORM:def 30 :
theorem Th54: :: POLYFORM:54
:: deftheorem Def31 defines eulerian POLYFORM:def 31 :
theorem Th55: :: POLYFORM:55
theorem Th56: :: POLYFORM:56
theorem Th57: :: POLYFORM:57
theorem Th58: :: POLYFORM:58
theorem Th59: :: POLYFORM:59
theorem Th60: :: POLYFORM:60
theorem Th61: :: POLYFORM:61
theorem Th62: :: POLYFORM:62
theorem Th63: :: POLYFORM:63
theorem Th64: :: POLYFORM:64
theorem Th65: :: POLYFORM:65
theorem Th66: :: POLYFORM:66
theorem Th67: :: POLYFORM:67
theorem Th68: :: POLYFORM:68
theorem Th69: :: POLYFORM:69
theorem Th70: :: POLYFORM:70
theorem :: POLYFORM:71
theorem Th72: :: POLYFORM:72
theorem Th73: :: POLYFORM:73
theorem Th74: :: POLYFORM:74
theorem Th75: :: POLYFORM:75
theorem Th76: :: POLYFORM:76
theorem Th77: :: POLYFORM:77
theorem Th78: :: POLYFORM:78
theorem Th79: :: POLYFORM:79
theorem Th80: :: POLYFORM:80
theorem Th81: :: POLYFORM:81
theorem Th82: :: POLYFORM:82
theorem Th83: :: POLYFORM:83
theorem Th84: :: POLYFORM:84
theorem Th85: :: POLYFORM:85
theorem Th86: :: POLYFORM:86
theorem Th87: :: POLYFORM:87
theorem Th88: :: POLYFORM:88
theorem Th89: :: POLYFORM:89
theorem :: POLYFORM:90
theorem :: POLYFORM:91
theorem :: POLYFORM:92