:: POLYFORM semantic presentation
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
let X, c, d be set ; ::_thesis: ( ex a, b being set st
( a <> b & X = {a,b} ) & c in X & d in X & c <> d implies X = {c,d} )
assume that
A1: ex a, b being set st
( a <> b & X = {a,b} ) and
A2: c in X and
A3: d in X and
A4: c <> d ; ::_thesis: X = {c,d}
consider a, b being set such that
a <> b and
A5: X = {a,b} by A1;
A6: X c= {c,d}
proof
A7: ( d = a or d = b ) by A3, A5, TARSKI:def_2;
A8: ( c = a or c = b ) by A2, A5, TARSKI:def_2;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in {c,d} )
assume A9: x in X ; ::_thesis: x in {c,d}
percases ( x = a or x = b ) by A5, A9, TARSKI:def_2;
suppose x = a ; ::_thesis: x in {c,d}
hence x in {c,d} by A4, A8, A7, TARSKI:def_2; ::_thesis: verum
end;
suppose x = b ; ::_thesis: x in {c,d}
hence x in {c,d} by A4, A8, A7, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
{c,d} c= X by A2, A3, ZFMISC_1:32;
hence X = {c,d} by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
begin
theorem :: POLYFORM:2
canceled;
theorem Th3: :: POLYFORM:3
for k being Integer st 1 <= k holds
k is Nat
proof
let k be Integer; ::_thesis: ( 1 <= k implies k is Nat )
assume 1 <= k ; ::_thesis: k is Nat
then reconsider k = k as Element of NAT by INT_1:3;
k is Nat ;
hence k is Nat ; ::_thesis: verum
end;
definition
let a be Integer;
let b be Nat;
:: original: *
redefine funca * b -> Element of INT ;
coherence
a * b is Element of INT by INT_1:def_2;
end;
theorem Th4: :: POLYFORM:4
1 is odd
proof
1 = (2 * 0) + 1 ;
hence 1 is odd ; ::_thesis: verum
end;
theorem Th5: :: POLYFORM:5
2 is even
proof
2 = 2 * 1 ;
hence 2 is even ; ::_thesis: verum
end;
theorem Th6: :: POLYFORM:6
3 is odd
proof
3 = (2 * 1) + 1 ;
hence 3 is odd ; ::_thesis: verum
end;
theorem Th7: :: POLYFORM:7
4 is even
proof
4 = 2 * 2 ;
hence 4 is even ; ::_thesis: verum
end;
theorem Th8: :: POLYFORM:8
for n being Nat st n is even holds
(- 1) |^ n = 1
proof
let n be Nat; ::_thesis: ( n is even implies (- 1) |^ n = 1 )
assume A1: n is even ; ::_thesis: (- 1) |^ n = 1
reconsider n = n as Element of NAT by ORDINAL1:def_12;
(- 1) |^ n = (- 1) to_power n by POWER:41;
hence (- 1) |^ n = 1 by A1, FIB_NUM2:3; ::_thesis: verum
end;
theorem Th9: :: POLYFORM:9
for n being Nat st n is odd holds
(- 1) |^ n = - 1
proof
let n be Nat; ::_thesis: ( n is odd implies (- 1) |^ n = - 1 )
assume A1: n is odd ; ::_thesis: (- 1) |^ n = - 1
reconsider n = n as Element of NAT by ORDINAL1:def_12;
(- 1) |^ n = (- 1) to_power n by POWER:41;
hence (- 1) |^ n = - 1 by A1, FIB_NUM2:2; ::_thesis: verum
end;
theorem Th10: :: POLYFORM:10
for n being Nat holds (- 1) |^ n is Integer
proof
let n be Nat; ::_thesis: (- 1) |^ n is Integer
percases ( n is even or n is odd ) ;
suppose n is even ; ::_thesis: (- 1) |^ n is Integer
hence (- 1) |^ n is Integer by Th8; ::_thesis: verum
end;
suppose n is odd ; ::_thesis: (- 1) |^ n is Integer
hence (- 1) |^ n is Integer by Th9; ::_thesis: verum
end;
end;
end;
definition
let a be Integer;
let n be Nat;
:: original: |^
redefine funca |^ n -> Element of INT ;
coherence
a |^ n is Element of INT
proof
consider b being Element of NAT such that
A1: ( a = b or a = - b ) by INT_1:2;
percases ( a = b or a = - b ) by A1;
suppose a = b ; ::_thesis: a |^ n is Element of INT
then reconsider a = a as Element of NAT ;
reconsider s = a |^ n as Element of NAT by ORDINAL1:def_12;
s in NAT ;
hence a |^ n is Element of INT by NUMBERS:17; ::_thesis: verum
end;
supposeA2: a = - b ; ::_thesis: a |^ n is Element of INT
reconsider bn = b |^ n as Element of NAT by ORDINAL1:def_12;
(- 1) |^ n is Integer by Th10;
then reconsider l = (- 1) |^ n as Element of INT by INT_1:def_2;
- b = (- 1) * b ;
then a |^ n = l * bn by A2, NEWTON:7;
hence a |^ n is Element of INT ; ::_thesis: verum
end;
end;
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
let p, q, r be FinSequence; ::_thesis: len (p ^ q) <= len (p ^ (q ^ r))
len ((p ^ q) ^ r) = len (p ^ (q ^ r)) by FINSEQ_1:32;
hence len (p ^ q) <= len (p ^ (q ^ r)) by CALCUL_1:6; ::_thesis: verum
end;
theorem Th12: :: POLYFORM:12
for n being Nat holds 1 < n + 2
proof
let n be Nat; ::_thesis: 1 < n + 2
( 0 < n + 1 implies 1 < n + 2 )
proof
assume 0 < n + 1 ; ::_thesis: 1 < n + 2
0 + 1 = 1 ;
hence 1 < n + 2 by XREAL_1:8; ::_thesis: verum
end;
hence 1 < n + 2 ; ::_thesis: verum
end;
theorem Th13: :: POLYFORM:13
(- 1) |^ 2 = 1
proof
(- 1) |^ 2 = (- 1) |^ (1 + 1)
.= ((- 1) |^ 1) * ((- 1) |^ 1) by NEWTON:8
.= ((- 1) |^ 1) * (- 1) by NEWTON:5
.= (- 1) * (- 1) by NEWTON:5 ;
hence (- 1) |^ 2 = 1 ; ::_thesis: verum
end;
theorem Th14: :: POLYFORM:14
for n being Nat holds (- 1) |^ n = (- 1) |^ (n + 2)
proof
let n be Nat; ::_thesis: (- 1) |^ n = (- 1) |^ (n + 2)
(- 1) |^ (n + 2) = ((- 1) |^ n) * ((- 1) |^ 2) by NEWTON:8
.= (- 1) |^ n by Th13 ;
hence (- 1) |^ n = (- 1) |^ (n + 2) ; ::_thesis: verum
end;
begin
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
defpred S1[ FinSequence of INT ] means ( len $1 > 0 implies for a, b being FinSequence of INT st len a = len $1 & len b = len $1 & ( for n being Nat st 1 <= n & n <= len $1 holds
$1 . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len $1 holds
b . k = - (a . (k + 1)) ) holds
Sum $1 = (a . 1) + (b . (len $1)) );
A1: for p being FinSequence of INT
for x being Element of INT st S1[p] holds
S1[p ^ <*x*>]
proof
let p be FinSequence of INT ; ::_thesis: for x being Element of INT st S1[p] holds
S1[p ^ <*x*>]
let x be Element of INT ; ::_thesis: ( S1[p] implies S1[p ^ <*x*>] )
assume A2: S1[p] ; ::_thesis: S1[p ^ <*x*>]
set t = p ^ <*x*>;
assume len (p ^ <*x*>) > 0 ; ::_thesis: for a, b being FinSequence of INT st len a = len (p ^ <*x*>) & len b = len (p ^ <*x*>) & ( for n being Nat st 1 <= n & n <= len (p ^ <*x*>) holds
(p ^ <*x*>) . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len (p ^ <*x*>) holds
b . k = - (a . (k + 1)) ) holds
Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))
let a, b be FinSequence of INT ; ::_thesis: ( len a = len (p ^ <*x*>) & len b = len (p ^ <*x*>) & ( for n being Nat st 1 <= n & n <= len (p ^ <*x*>) holds
(p ^ <*x*>) . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len (p ^ <*x*>) holds
b . k = - (a . (k + 1)) ) implies Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) )
assume that
A3: len a = len (p ^ <*x*>) and
A4: len b = len (p ^ <*x*>) and
A5: for n being Nat st 1 <= n & n <= len (p ^ <*x*>) holds
(p ^ <*x*>) . n = (a . n) + (b . n) and
A6: for k being Nat st 1 <= k & k < len (p ^ <*x*>) holds
b . k = - (a . (k + 1)) ; ::_thesis: Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))
A7: Sum (p ^ <*x*>) = (Sum p) + x by RVSUM_1:74;
percases ( len p = 0 or len p > 0 ) ;
supposeA8: len p = 0 ; ::_thesis: Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))
reconsider egy = 1 as Nat ;
p = {} by A8;
then A9: p ^ <*x*> = <*x*> by FINSEQ_1:34;
then egy <= len (p ^ <*x*>) by FINSEQ_1:39;
then A10: (p ^ <*x*>) . egy = (a . egy) + (b . egy) by A5;
A11: p = {} by A8;
len (p ^ <*x*>) = 1 by A9, FINSEQ_1:39;
hence Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) by A7, A11, A9, A10, FINSEQ_1:40, GR_CY_1:3; ::_thesis: verum
end;
supposeA12: len p > 0 ; ::_thesis: Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>)))
set m = len p;
set a9 = a | (len p);
A13: (a | (len p)) . 1 = a . 1
proof
reconsider egy = 1 as Element of NAT ;
0 + 1 = 1 ;
then egy <= len p by A12, INT_1:7;
hence (a | (len p)) . 1 = a . 1 by FINSEQ_3:112; ::_thesis: verum
end;
set b9 = b | (len p);
A14: b . (len p) = (b | (len p)) . (len p) by FINSEQ_3:112;
A15: for n being Nat st 1 <= n & n < len p holds
(b | (len p)) . n = - ((a | (len p)) . (n + 1))
proof
let n be Nat; ::_thesis: ( 1 <= n & n < len p implies (b | (len p)) . n = - ((a | (len p)) . (n + 1)) )
assume that
A16: 1 <= n and
A17: n < len p ; ::_thesis: (b | (len p)) . n = - ((a | (len p)) . (n + 1))
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A18: (b | (len p)) . n = b . n by A17, FINSEQ_3:112;
n + 1 <= len p by A17, INT_1:7;
then A19: (a | (len p)) . (n + 1) = a . (n + 1) by FINSEQ_3:112;
len p <= len (p ^ <*x*>) by CALCUL_1:6;
then n < len (p ^ <*x*>) by A17, XXREAL_0:2;
hence (b | (len p)) . n = - ((a | (len p)) . (n + 1)) by A6, A16, A18, A19; ::_thesis: verum
end;
A20: for n being Nat st 1 <= n & n <= len p holds
p . n = ((a | (len p)) . n) + ((b | (len p)) . n)
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len p implies p . n = ((a | (len p)) . n) + ((b | (len p)) . n) )
assume that
A21: 1 <= n and
A22: n <= len p ; ::_thesis: p . n = ((a | (len p)) . n) + ((b | (len p)) . n)
dom p = Seg (len p) by FINSEQ_1:def_3;
then A23: n in dom p by A21, A22, FINSEQ_1:1;
len p <= len (p ^ <*x*>) by CALCUL_1:6;
then A24: n <= len (p ^ <*x*>) by A22, XXREAL_0:2;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
p . n = (p ^ <*x*>) . n by A23, FINSEQ_1:def_7
.= (a . n) + (b . n) by A5, A21, A24
.= ((a | (len p)) . n) + (b . n) by A22, FINSEQ_3:112
.= ((a | (len p)) . n) + ((b | (len p)) . n) by A22, FINSEQ_3:112 ;
hence p . n = ((a | (len p)) . n) + ((b | (len p)) . n) ; ::_thesis: verum
end;
A25: 1 <= len p by A12, Lm1;
len <*x*> = 1 by FINSEQ_1:39;
then A26: len (p ^ <*x*>) = (len p) + 1 by FINSEQ_1:22;
0 + (len p) = len p ;
then len p < len (p ^ <*x*>) by A26, XREAL_1:6;
then A27: b . (len p) = - (a . ((len p) + 1)) by A6, A25;
0 + 1 = 1 ;
then A28: 1 <= len (p ^ <*x*>) by A26, XREAL_1:6;
A29: x = (p ^ <*x*>) . ((len p) + 1) by FINSEQ_1:42
.= (- ((b | (len p)) . (len p))) + (b . (len (p ^ <*x*>))) by A5, A26, A28, A27, A14 ;
len p <= len b by A4, CALCUL_1:6;
then A30: len (b | (len p)) = len p by FINSEQ_1:59;
len p <= len a by A3, CALCUL_1:6;
then len (a | (len p)) = len p by FINSEQ_1:59;
then Sum p = ((a | (len p)) . 1) + ((b | (len p)) . (len p)) by A2, A12, A30, A20, A15;
hence Sum (p ^ <*x*>) = (a . 1) + (b . (len (p ^ <*x*>))) by A7, A13, A29; ::_thesis: verum
end;
end;
end;
A31: S1[ <*> INT] ;
A32: for p being FinSequence of INT holds S1[p] from FINSEQ_2:sch_2(A31, A1);
let a, b, s be FinSequence of INT ; ::_thesis: ( 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)) ) implies Sum s = (a . 1) + (b . (len s)) )
assume ( 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)) ) ) ; ::_thesis: Sum s = (a . 1) + (b . (len s))
hence Sum s = (a . 1) + (b . (len s)) by A32; ::_thesis: verum
end;
theorem Th16: :: POLYFORM:16
for p, q, r being FinSequence holds len ((p ^ q) ^ r) = ((len p) + (len q)) + (len r)
proof
let p, q, r be FinSequence; ::_thesis: len ((p ^ q) ^ r) = ((len p) + (len q)) + (len r)
len ((p ^ q) ^ r) = (len (p ^ q)) + (len r) by FINSEQ_1:22
.= ((len p) + (len q)) + (len r) by FINSEQ_1:22 ;
hence len ((p ^ q) ^ r) = ((len p) + (len q)) + (len r) ; ::_thesis: verum
end;
theorem Th17: :: POLYFORM:17
for x being set
for p, q being FinSequence holds ((<*x*> ^ p) ^ q) . 1 = x
proof
let x be set ; ::_thesis: for p, q being FinSequence holds ((<*x*> ^ p) ^ q) . 1 = x
let p, q be FinSequence; ::_thesis: ((<*x*> ^ p) ^ q) . 1 = x
(<*x*> ^ p) ^ q = <*x*> ^ (p ^ q) by FINSEQ_1:32;
hence ((<*x*> ^ p) ^ q) . 1 = x by FINSEQ_1:41; ::_thesis: verum
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
let x be set ; ::_thesis: for p, q being FinSequence holds ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x
let p, q be FinSequence; ::_thesis: ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x
set s = p ^ q;
((p ^ q) ^ <*x*>) . ((len (p ^ q)) + 1) = x by FINSEQ_1:42;
hence ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x by FINSEQ_1:22; ::_thesis: verum
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
let p, q, r be FinSequence; ::_thesis: for k being Nat st len p < k & k <= len (p ^ q) holds
((p ^ q) ^ r) . k = q . (k - (len p))
let k be Nat; ::_thesis: ( len p < k & k <= len (p ^ q) implies ((p ^ q) ^ r) . k = q . (k - (len p)) )
assume that
A1: len p < k and
A2: k <= len (p ^ q) ; ::_thesis: ((p ^ q) ^ r) . k = q . (k - (len p))
set n = k - (len p);
(len p) - (len p) = 0 ;
then A3: 0 < k - (len p) by A1, XREAL_1:9;
0 + 1 = 1 ;
then A4: 1 <= k - (len p) by A3, INT_1:7;
then reconsider n = k - (len p) as Nat by Th3;
A5: ((len p) + (len q)) - (len p) = len q ;
k <= (len p) + (len q) by A2, FINSEQ_1:22;
then n <= len q by A5, XREAL_1:9;
then n in Seg (len q) by A4, FINSEQ_1:1;
then A6: n in dom q by FINSEQ_1:def_3;
len (p ^ q) <= len (p ^ (q ^ r)) by Th11;
then k <= len (p ^ (q ^ r)) by A2, XXREAL_0:2;
then A7: (p ^ (q ^ r)) . k = (q ^ r) . (k - (len p)) by A1, FINSEQ_1:24;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
(q ^ r) . n = q . n by A6, FINSEQ_1:def_7;
hence ((p ^ q) ^ r) . k = q . (k - (len p)) by A7, FINSEQ_1:32; ::_thesis: verum
end;
definition
let a be Integer;
:: original: <*
redefine func<*a*> -> FinSequence of INT ;
coherence
<*a*> is FinSequence of INT
proof
set s = <*a*>;
a in INT by INT_1:def_2;
then ( rng <*a*> = {a} & {a} c= INT ) by FINSEQ_1:38, ZFMISC_1:31;
hence <*a*> is FinSequence of INT by FINSEQ_1:def_4; ::_thesis: verum
end;
end;
definition
let a, b be Integer;
:: original: <*
redefine func<*a,b*> -> FinSequence of INT ;
coherence
<*a,b*> is FinSequence of INT
proof
set s = <*a,b*>;
( a in INT & b in INT ) by INT_1:def_2;
then ( rng <*a,b*> = {a,b} & {a,b} c= INT ) by FINSEQ_2:127, ZFMISC_1:32;
hence <*a,b*> is FinSequence of INT by FINSEQ_1:def_4; ::_thesis: verum
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
set s = <*a,b,c*>;
A1: c in INT by INT_1:def_2;
( a in INT & b in INT ) by INT_1:def_2;
then ( rng <*a,b,c*> = {a,b,c} & {a,b,c} c= INT ) by A1, FINSEQ_2:128, ZFMISC_1:133;
hence <*a,b,c*> is FinSequence of INT by FINSEQ_1:def_4; ::_thesis: verum
end;
end;
definition
let p, q be FinSequence of INT ;
:: original: ^
redefine funcp ^ q -> FinSequence of INT ;
coherence
p ^ q is FinSequence of INT by FINSEQ_1:75;
end;
theorem Th20: :: POLYFORM:20
for k being Integer
for p being FinSequence of INT holds Sum (<*k*> ^ p) = k + (Sum p)
proof
let k be Integer; ::_thesis: for p being FinSequence of INT holds Sum (<*k*> ^ p) = k + (Sum p)
let p be FinSequence of INT ; ::_thesis: Sum (<*k*> ^ p) = k + (Sum p)
reconsider k = k as Element of INT by INT_1:def_2;
Sum (<*k*> ^ p) = (Sum p) + (Sum <*k*>) by RVSUM_1:75
.= Sum (p ^ <*k*>) by RVSUM_1:75
.= k + (Sum p) by RVSUM_1:74 ;
hence Sum (<*k*> ^ p) = k + (Sum p) ; ::_thesis: verum
end;
theorem Th21: :: POLYFORM:21
for p, q, r being FinSequence of INT holds Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r)
proof
let p, q, r be FinSequence of INT ; ::_thesis: Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r)
Sum ((p ^ q) ^ r) = (Sum (p ^ q)) + (Sum r) by RVSUM_1:75
.= ((Sum p) + (Sum q)) + (Sum r) by RVSUM_1:75 ;
hence Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r) ; ::_thesis: verum
end;
theorem :: POLYFORM:22
for a being Element of Z_2 holds Sum <*a*> = a by FINSOP_1:11;
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 Th23: :: POLYFORM:23
for X, Y being set holds [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y
proof
let X, Y be set ; ::_thesis: [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y
set f = [:X,Y:] --> (1. Z_2);
( rng ([:X,Y:] --> (1. Z_2)) c= {(1. Z_2)} & {(1. Z_2)} c= {(0. Z_2),(1. Z_2)} ) by FUNCOP_1:13, ZFMISC_1:7;
then ( dom ([:X,Y:] --> (1. Z_2)) = [:X,Y:] & rng ([:X,Y:] --> (1. Z_2)) c= {(0. Z_2),(1. Z_2)} ) by FUNCOP_1:13, XBOOLE_1:1;
hence [:X,Y:] --> (1. Z_2) is incidence-matrix of X,Y by FUNCT_2:def_2; ::_thesis: verum
end;
definition
attrc1 is strict ;
struct PolyhedronStr -> ;
aggrPolyhedronStr(# PolytopsF, IncidenceF #) -> PolyhedronStr ;
sel PolytopsF c1 -> FinSequence-yielding FinSequence;
sel IncidenceF c1 -> Function-yielding FinSequence;
end;
definition
let p be PolyhedronStr ;
attrp is polyhedron_1 means :Def1: :: POLYFORM:def 1
len the IncidenceF of p = (len the PolytopsF of p) - 1;
attrp 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)));
attrp 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 for PolyhedronStr ;
existence
ex b1 being PolyhedronStr st
( b1 is polyhedron_1 & b1 is polyhedron_2 & b1 is polyhedron_3 )
proof
reconsider I = <*> {} as Function-yielding FinSequence ;
reconsider F = <*<*{}*>*> as FinSequence-yielding FinSequence ;
take p = PolyhedronStr(# F,I #); ::_thesis: ( p is polyhedron_1 & p is polyhedron_2 & p is polyhedron_3 )
A1: len F = 1 by FINSEQ_1:39;
len I = 1 - 1 ;
hence p is polyhedron_1 by A1, Def1; ::_thesis: ( p is polyhedron_2 & p is polyhedron_3 )
for n being Nat st 1 <= n & n < 1 holds
I . n is incidence-matrix of (rng (F . n)),(rng (F . (n + 1))) ;
hence p is polyhedron_2 by A1, Def2; ::_thesis: p is polyhedron_3
let n be Nat; :: according to POLYFORM:def_3 ::_thesis: ( 1 <= n & n <= len the PolytopsF of p implies ( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) )
assume ( 1 <= n & n <= len the PolytopsF of p ) ; ::_thesis: ( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one )
then n = 1 by A1, XXREAL_0:1;
hence ( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) by FINSEQ_1:def_8; ::_thesis: verum
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;
funck -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 b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
proof
set F = the PolytopsF of p;
percases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
supposeA1: k < - 1 ; ::_thesis: ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
take {} ; ::_thesis: ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) )
thus ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) ) by A1; ::_thesis: verum
end;
supposeA2: k = - 1 ; ::_thesis: ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
take {{}} ; ::_thesis: ( ( k < - 1 implies {{}} = {} ) & ( k = - 1 implies {{}} = {{}} ) & ( - 1 < k & k < dim p implies {{}} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {{}} = {p} ) & ( k > dim p implies {{}} = {} ) )
thus ( ( k < - 1 implies {{}} = {} ) & ( k = - 1 implies {{}} = {{}} ) & ( - 1 < k & k < dim p implies {{}} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {{}} = {p} ) & ( k > dim p implies {{}} = {} ) ) by A2; ::_thesis: verum
end;
supposeA3: ( - 1 < k & k < dim p ) ; ::_thesis: ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
(- 1) + 1 = 0 ;
then 0 <= k by A3, INT_1:7;
then reconsider k = k as Element of NAT by INT_1:3;
set n = k + 1;
reconsider Fn = the PolytopsF of p . (k + 1) as FinSequence ;
take rng Fn ; ::_thesis: ( ( k < - 1 implies rng Fn = {} ) & ( k = - 1 implies rng Fn = {{}} ) & ( - 1 < k & k < dim p implies rng Fn = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies rng Fn = {p} ) & ( k > dim p implies rng Fn = {} ) )
thus ( ( k < - 1 implies rng Fn = {} ) & ( k = - 1 implies rng Fn = {{}} ) & ( - 1 < k & k < dim p implies rng Fn = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies rng Fn = {p} ) & ( k > dim p implies rng Fn = {} ) ) by A3; ::_thesis: verum
end;
supposeA4: k = dim p ; ::_thesis: ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
take {p} ; ::_thesis: ( ( k < - 1 implies {p} = {} ) & ( k = - 1 implies {p} = {{}} ) & ( - 1 < k & k < dim p implies {p} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {p} = {p} ) & ( k > dim p implies {p} = {} ) )
thus ( ( k < - 1 implies {p} = {} ) & ( k = - 1 implies {p} = {{}} ) & ( - 1 < k & k < dim p implies {p} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {p} = {p} ) & ( k > dim p implies {p} = {} ) ) by A4; ::_thesis: verum
end;
supposeA5: k > dim p ; ::_thesis: ex b1 being finite set st
( ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) )
take {} ; ::_thesis: ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) )
thus ( ( k < - 1 implies {} = {} ) & ( k = - 1 implies {} = {{}} ) & ( - 1 < k & k < dim p implies {} = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies {} = {p} ) & ( k > dim p implies {} = {} ) ) by A5; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being finite set st ( k < - 1 implies b1 = {} ) & ( k = - 1 implies b1 = {{}} ) & ( - 1 < k & k < dim p implies b1 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b1 = {p} ) & ( k > dim p implies b1 = {} ) & ( k < - 1 implies b2 = {} ) & ( k = - 1 implies b2 = {{}} ) & ( - 1 < k & k < dim p implies b2 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b2 = {p} ) & ( k > dim p implies b2 = {} ) holds
b1 = b2
proof
set F = the PolytopsF of p;
let X, Y be finite set ; ::_thesis: ( ( k < - 1 implies X = {} ) & ( k = - 1 implies X = {{}} ) & ( - 1 < k & k < dim p implies X = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies X = {p} ) & ( k > dim p implies X = {} ) & ( k < - 1 implies Y = {} ) & ( k = - 1 implies Y = {{}} ) & ( - 1 < k & k < dim p implies Y = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies Y = {p} ) & ( k > dim p implies Y = {} ) implies X = Y )
assume that
A6: ( k < - 1 implies X = {} ) and
A7: ( k = - 1 implies X = {{}} ) and
A8: ( - 1 < k & k < dim p implies X = rng ( the PolytopsF of p . (k + 1)) ) and
A9: ( k = dim p implies X = {p} ) and
A10: ( k > dim p implies X = {} ) and
A11: ( k < - 1 implies Y = {} ) and
A12: ( k = - 1 implies Y = {{}} ) and
A13: ( - 1 < k & k < dim p implies Y = rng ( the PolytopsF of p . (k + 1)) ) and
A14: ( k = dim p implies Y = {p} ) and
A15: ( k > dim p implies Y = {} ) ; ::_thesis: X = Y
percases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
suppose k < - 1 ; ::_thesis: X = Y
hence X = Y by A6, A11; ::_thesis: verum
end;
suppose k = - 1 ; ::_thesis: X = Y
hence X = Y by A7, A12; ::_thesis: verum
end;
suppose ( - 1 < k & k < dim p ) ; ::_thesis: X = Y
hence X = Y by A8, A13; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: X = Y
hence X = Y by A9, A14; ::_thesis: verum
end;
suppose k > dim p ; ::_thesis: X = Y
hence X = Y by A10, A15; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def5 defines -polytopes POLYFORM:def_5_:_
for p being polyhedron
for k being Integer
for b3 being finite set holds
( b3 = k -polytopes p iff ( ( k < - 1 implies b3 = {} ) & ( k = - 1 implies b3 = {{}} ) & ( - 1 < k & k < dim p implies b3 = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b3 = {p} ) & ( k > dim p implies b3 = {} ) ) );
theorem Th24: :: 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 )
proof
let p be polyhedron; ::_thesis: for k being Integer st - 1 < k & k < dim p holds
( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )
let k be Integer; ::_thesis: ( - 1 < k & k < dim p implies ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) )
A1: (- 1) + 1 = 0 ;
assume - 1 < k ; ::_thesis: ( not k < dim p or ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) )
then A2: 0 < k + 1 by A1, XREAL_1:6;
then reconsider n = k + 1 as Element of NAT by INT_1:3;
A3: ( n is Nat & 0 + 1 = 1 ) ;
assume k < dim p ; ::_thesis: ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )
hence ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) by A2, A3, INT_1:7; ::_thesis: verum
end;
theorem Th25: :: POLYFORM:25
for p being polyhedron
for k being Integer holds
( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )
proof
let p be polyhedron; ::_thesis: for k being Integer holds
( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )
let k be Integer; ::_thesis: ( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )
set X = k -polytopes p;
thus ( not k -polytopes p is empty implies ( - 1 <= k & k <= dim p ) ) by Def5; ::_thesis: ( - 1 <= k & k <= dim p implies not k -polytopes p is empty )
thus ( - 1 <= k & k <= dim p implies not k -polytopes p is empty ) ::_thesis: verum
proof
assume A1: - 1 <= k ; ::_thesis: ( not k <= dim p or not k -polytopes p is empty )
assume A2: k <= dim p ; ::_thesis: not k -polytopes p is empty
percases ( k = - 1 or ( - 1 < k & k < dim p ) or k = dim p ) by A1, A2, XXREAL_0:1;
suppose k = - 1 ; ::_thesis: not k -polytopes p is empty
hence not k -polytopes p is empty by Def5; ::_thesis: verum
end;
supposeA3: ( - 1 < k & k < dim p ) ; ::_thesis: not k -polytopes p is empty
set F = the PolytopsF of p;
A4: k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by A3, Def5;
set n = k + 1;
A5: 1 <= k + 1 by A3, Th24;
A6: k + 1 <= dim p by A3, Th24;
reconsider n = k + 1 as Element of NAT by A5, INT_1:3;
reconsider n = n as Nat ;
not the PolytopsF of p . n is empty by A5, A6, Def3;
hence not k -polytopes p is empty by A4; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: not k -polytopes p is empty
then k -polytopes p = {p} by Def5;
hence not k -polytopes p is empty ; ::_thesis: verum
end;
end;
end;
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;
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 = {} ) )
proof
percases ( k < 0 or k > dim p or ( 0 < k & k < dim p ) or k = 0 or k = dim p ) by XXREAL_0:1;
supposeA1: k < 0 ; ::_thesis: 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 = {} ) )
set f = {} ;
reconsider f = {} as Function ;
k - 1 < 0 - 1 by A1, XREAL_1:9;
then (k - 1) -polytopes p = {} by Def5;
then [:((k - 1) -polytopes p),(k -polytopes p):] = {} by ZFMISC_1:90;
then reconsider f = f as Function of [:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)} by RELSET_1:12;
reconsider f = f as Element of Funcs ([:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)}) by FUNCT_2:8;
take f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A1; ::_thesis: verum
end;
supposeA2: k > dim p ; ::_thesis: 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 = {} ) )
set f = {} ;
reconsider f = {} as Function ;
k -polytopes p = {} by A2, Th25;
then [:((k - 1) -polytopes p),(k -polytopes p):] = {} by ZFMISC_1:90;
then reconsider f = f as Function of [:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)} by RELSET_1:12;
reconsider f = f as Element of Funcs ([:((k - 1) -polytopes p),(k -polytopes p):],{(0. Z_2),(1. Z_2)}) by FUNCT_2:8;
take f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A2; ::_thesis: verum
end;
supposeA3: ( 0 < k & k < dim p ) ; ::_thesis: 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 = {} ) )
set F = the PolytopsF of p;
set I = the IncidenceF of p;
A4: k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by A3, Def5;
A5: k - 1 < dim p by A3, XREAL_1:146, XXREAL_0:2;
0 + 1 = 1 ;
then A6: 1 <= k by A3, INT_1:7;
then reconsider k9 = k as Nat by Th3;
1 - 1 = 0 ;
then - 1 < k - 1 by A6, XREAL_1:9;
then (k - 1) -polytopes p = rng ( the PolytopsF of p . ((k - 1) + 1)) by A5, Def5;
then reconsider Ik = the IncidenceF of p . k9 as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A3, A6, A4, Def2;
take Ik ; ::_thesis: ( ( k < 0 implies Ik = {} ) & ( k = 0 implies Ik = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies Ik = the IncidenceF of p . k ) & ( k = dim p implies Ik = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies Ik = {} ) )
thus ( ( k < 0 implies Ik = {} ) & ( k = 0 implies Ik = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies Ik = the IncidenceF of p . k ) & ( k = dim p implies Ik = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies Ik = {} ) ) by A3; ::_thesis: verum
end;
supposeA7: k = 0 ; ::_thesis: 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 = {} ) )
percases ( k = dim p or k <> dim p ) ;
supposeA8: k = dim p ; ::_thesis: 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 = {} ) )
set f = [:{{}},{p}:] --> (1. Z_2);
reconsider f = [:{{}},{p}:] --> (1. Z_2) as incidence-matrix of {{}},{p} by Th23;
(k - 1) -polytopes p = {{}} by A7, Def5;
then reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A8, Def5;
take f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A7, A8, Def5; ::_thesis: verum
end;
supposeA9: k <> dim p ; ::_thesis: 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 = {} ) )
set f = [:{{}},(0 -polytopes p):] --> (1. Z_2);
reconsider f = [:{{}},(0 -polytopes p):] --> (1. Z_2) as incidence-matrix of {{}},(0 -polytopes p) by Th23;
reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A7, Def5;
take f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A7, A9; ::_thesis: verum
end;
end;
end;
supposeA10: k = dim p ; ::_thesis: 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 = {} ) )
percases ( k = 0 or k <> 0 ) ;
supposeA11: k = 0 ; ::_thesis: 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 = {} ) )
set f = [:{{}},{p}:] --> (1. Z_2);
reconsider f = [:{{}},{p}:] --> (1. Z_2) as incidence-matrix of {{}},{p} by Th23;
(k - 1) -polytopes p = {{}} by A11, Def5;
then reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A10, Def5;
take f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A10, A11, Def5; ::_thesis: verum
end;
supposeA12: k <> 0 ; ::_thesis: 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 = {} ) )
set f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2);
reconsider f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) as incidence-matrix of (((dim p) - 1) -polytopes p),{p} by Th23;
reconsider f = f as incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) by A10, Def5;
take f ; ::_thesis: ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) )
thus ( ( k < 0 implies f = {} ) & ( k = 0 implies f = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies f = the IncidenceF of p . k ) & ( k = dim p implies f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies f = {} ) ) by A10, A12; ::_thesis: verum
end;
end;
end;
end;
end;
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
proof
set I = the IncidenceF of p;
let s, t be incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p); ::_thesis: ( ( k < 0 implies s = {} ) & ( k = 0 implies s = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies s = the IncidenceF of p . k ) & ( k = dim p implies s = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies s = {} ) & ( k < 0 implies t = {} ) & ( k = 0 implies t = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies t = the IncidenceF of p . k ) & ( k = dim p implies t = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies t = {} ) implies s = t )
assume that
A13: ( k < 0 implies s = {} ) and
A14: ( k = 0 implies s = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) and
A15: ( 0 < k & k < dim p implies s = the IncidenceF of p . k ) and
A16: ( k = dim p implies s = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) and
A17: ( k > dim p implies s = {} ) and
A18: ( k < 0 implies t = {} ) and
A19: ( k = 0 implies t = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) and
A20: ( 0 < k & k < dim p implies t = the IncidenceF of p . k ) and
A21: ( k = dim p implies t = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) and
A22: ( k > dim p implies t = {} ) ; ::_thesis: s = t
percases ( k < 0 or k = 0 or ( 0 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
suppose k < 0 ; ::_thesis: s = t
hence s = t by A13, A18; ::_thesis: verum
end;
suppose k = 0 ; ::_thesis: s = t
hence s = t by A14, A19; ::_thesis: verum
end;
suppose ( 0 < k & k < dim p ) ; ::_thesis: s = t
hence s = t by A15, A20; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: s = t
hence s = t by A16, A21; ::_thesis: verum
end;
suppose k > dim p ; ::_thesis: s = t
hence s = t by A17, A22; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def6 defines eta POLYFORM:def_6_:_
for p being polyhedron
for k being Integer
for b3 being incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) holds
( b3 = eta (p,k) iff ( ( k < 0 implies b3 = {} ) & ( k = 0 implies b3 = [:{{}},(0 -polytopes p):] --> (1. Z_2) ) & ( 0 < k & k < dim p implies b3 = the IncidenceF of p . k ) & ( k = dim p implies b3 = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) ) & ( k > dim p implies b3 = {} ) ) );
definition
let p be polyhedron;
let k be Integer;
funck -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 b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
proof
percases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
supposeA1: k < - 1 ; ::_thesis: ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
take <*> {} ; ::_thesis: ( ( k < - 1 implies <*> {} = <*> {} ) & ( k = - 1 implies <*> {} = <*{}*> ) & ( - 1 < k & k < dim p implies <*> {} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*> {} = <*p*> ) & ( k > dim p implies <*> {} = <*> {} ) )
thus ( ( k < - 1 implies <*> {} = <*> {} ) & ( k = - 1 implies <*> {} = <*{}*> ) & ( - 1 < k & k < dim p implies <*> {} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*> {} = <*p*> ) & ( k > dim p implies <*> {} = <*> {} ) ) by A1; ::_thesis: verum
end;
supposeA2: k = - 1 ; ::_thesis: ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
take <*{}*> ; ::_thesis: ( ( k < - 1 implies <*{}*> = <*> {} ) & ( k = - 1 implies <*{}*> = <*{}*> ) & ( - 1 < k & k < dim p implies <*{}*> = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*{}*> = <*p*> ) & ( k > dim p implies <*{}*> = <*> {} ) )
thus ( ( k < - 1 implies <*{}*> = <*> {} ) & ( k = - 1 implies <*{}*> = <*{}*> ) & ( - 1 < k & k < dim p implies <*{}*> = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*{}*> = <*p*> ) & ( k > dim p implies <*{}*> = <*> {} ) ) by A2; ::_thesis: verum
end;
supposeA3: ( - 1 < k & k < dim p ) ; ::_thesis: ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
set F = the PolytopsF of p;
take the PolytopsF of p . (k + 1) ; ::_thesis: ( ( k < - 1 implies the PolytopsF of p . (k + 1) = <*> {} ) & ( k = - 1 implies the PolytopsF of p . (k + 1) = <*{}*> ) & ( - 1 < k & k < dim p implies the PolytopsF of p . (k + 1) = the PolytopsF of p . (k + 1) ) & ( k = dim p implies the PolytopsF of p . (k + 1) = <*p*> ) & ( k > dim p implies the PolytopsF of p . (k + 1) = <*> {} ) )
thus ( ( k < - 1 implies the PolytopsF of p . (k + 1) = <*> {} ) & ( k = - 1 implies the PolytopsF of p . (k + 1) = <*{}*> ) & ( - 1 < k & k < dim p implies the PolytopsF of p . (k + 1) = the PolytopsF of p . (k + 1) ) & ( k = dim p implies the PolytopsF of p . (k + 1) = <*p*> ) & ( k > dim p implies the PolytopsF of p . (k + 1) = <*> {} ) ) by A3; ::_thesis: verum
end;
supposeA4: k = dim p ; ::_thesis: ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
take <*p*> ; ::_thesis: ( ( k < - 1 implies <*p*> = <*> {} ) & ( k = - 1 implies <*p*> = <*{}*> ) & ( - 1 < k & k < dim p implies <*p*> = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*p*> = <*p*> ) & ( k > dim p implies <*p*> = <*> {} ) )
thus ( ( k < - 1 implies <*p*> = <*> {} ) & ( k = - 1 implies <*p*> = <*{}*> ) & ( - 1 < k & k < dim p implies <*p*> = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*p*> = <*p*> ) & ( k > dim p implies <*p*> = <*> {} ) ) by A4; ::_thesis: verum
end;
supposeA5: k > dim p ; ::_thesis: ex b1 being FinSequence st
( ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) )
take <*> {} ; ::_thesis: ( ( k < - 1 implies <*> {} = <*> {} ) & ( k = - 1 implies <*> {} = <*{}*> ) & ( - 1 < k & k < dim p implies <*> {} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*> {} = <*p*> ) & ( k > dim p implies <*> {} = <*> {} ) )
thus ( ( k < - 1 implies <*> {} = <*> {} ) & ( k = - 1 implies <*> {} = <*{}*> ) & ( - 1 < k & k < dim p implies <*> {} = the PolytopsF of p . (k + 1) ) & ( k = dim p implies <*> {} = <*p*> ) & ( k > dim p implies <*> {} = <*> {} ) ) by A5; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being FinSequence st ( k < - 1 implies b1 = <*> {} ) & ( k = - 1 implies b1 = <*{}*> ) & ( - 1 < k & k < dim p implies b1 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b1 = <*p*> ) & ( k > dim p implies b1 = <*> {} ) & ( k < - 1 implies b2 = <*> {} ) & ( k = - 1 implies b2 = <*{}*> ) & ( - 1 < k & k < dim p implies b2 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b2 = <*p*> ) & ( k > dim p implies b2 = <*> {} ) holds
b1 = b2
proof
set F = the PolytopsF of p;
let s, t be FinSequence; ::_thesis: ( ( k < - 1 implies s = <*> {} ) & ( k = - 1 implies s = <*{}*> ) & ( - 1 < k & k < dim p implies s = the PolytopsF of p . (k + 1) ) & ( k = dim p implies s = <*p*> ) & ( k > dim p implies s = <*> {} ) & ( k < - 1 implies t = <*> {} ) & ( k = - 1 implies t = <*{}*> ) & ( - 1 < k & k < dim p implies t = the PolytopsF of p . (k + 1) ) & ( k = dim p implies t = <*p*> ) & ( k > dim p implies t = <*> {} ) implies s = t )
assume that
A6: ( k < - 1 implies s = <*> {} ) and
A7: ( k = - 1 implies s = <*{}*> ) and
A8: ( - 1 < k & k < dim p implies s = the PolytopsF of p . (k + 1) ) and
A9: ( k = dim p implies s = <*p*> ) and
A10: ( k > dim p implies s = <*> {} ) and
A11: ( k < - 1 implies t = <*> {} ) and
A12: ( k = - 1 implies t = <*{}*> ) and
A13: ( - 1 < k & k < dim p implies t = the PolytopsF of p . (k + 1) ) and
A14: ( k = dim p implies t = <*p*> ) and
A15: ( k > dim p implies t = <*> {} ) ; ::_thesis: s = t
percases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
suppose k < - 1 ; ::_thesis: s = t
hence s = t by A6, A11; ::_thesis: verum
end;
suppose k = - 1 ; ::_thesis: s = t
hence s = t by A7, A12; ::_thesis: verum
end;
suppose ( - 1 < k & k < dim p ) ; ::_thesis: s = t
hence s = t by A8, A13; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: s = t
hence s = t by A9, A14; ::_thesis: verum
end;
suppose k > dim p ; ::_thesis: s = t
hence s = t by A10, A15; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def7 defines -polytope-seq POLYFORM:def_7_:_
for p being polyhedron
for k being Integer
for b3 being FinSequence holds
( b3 = k -polytope-seq p iff ( ( k < - 1 implies b3 = <*> {} ) & ( k = - 1 implies b3 = <*{}*> ) & ( - 1 < k & k < dim p implies b3 = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b3 = <*p*> ) & ( k > dim p implies b3 = <*> {} ) ) );
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 Th27: :: POLYFORM:27
for p being polyhedron
for k being Integer holds dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
proof
let p be polyhedron; ::_thesis: for k being Integer holds dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
let k be Integer; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
set F = the PolytopsF of p;
percases ( k < - 1 or ( - 1 <= k & k <= dim p ) or k > dim p ) ;
suppose k < - 1 ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
then ( k -polytope-seq p = <*> {} & k -polytopes p = {} ) by Def5, Def7;
hence dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by FINSEQ_1:def_3; ::_thesis: verum
end;
supposeA1: ( - 1 <= k & k <= dim p ) ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
percases ( k = - 1 or ( - 1 < k & k < dim p ) or k = dim p ) by A1, XXREAL_0:1;
supposeA2: k = - 1 ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
then k -polytope-seq p = <*{}*> by Def7;
then A3: len (k -polytope-seq p) = 1 by FINSEQ_1:39;
k -polytopes p = {{}} by A2, Def5;
then num-polytopes (p,k) = 1 by CARD_2:42;
hence dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by A3, FINSEQ_1:def_3; ::_thesis: verum
end;
supposeA4: ( - 1 < k & k < dim p ) ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
set n = k + 1;
reconsider n = k + 1 as Nat by A4, Th24;
reconsider Fn = the PolytopsF of p . n as FinSequence ;
( 1 <= n & n <= dim p ) by A4, Th24;
then A5: Fn is one-to-one by Def3;
k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by A4, Def5;
then num-polytopes (p,k) = card (dom Fn) by A5, CARD_1:70;
then A6: len Fn = num-polytopes (p,k) by CARD_1:62;
k -polytope-seq p = the PolytopsF of p . (k + 1) by A4, Def7;
hence dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by A6, FINSEQ_1:def_3; ::_thesis: verum
end;
supposeA7: k = dim p ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
then k -polytope-seq p = <*p*> by Def7;
then A8: len (k -polytope-seq p) = 1 by FINSEQ_1:39;
k -polytopes p = {p} by A7, Def5;
then num-polytopes (p,k) = 1 by CARD_2:42;
hence dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by A8, FINSEQ_1:def_3; ::_thesis: verum
end;
end;
end;
suppose k > dim p ; ::_thesis: dom (k -polytope-seq p) = Seg (num-polytopes (p,k))
then ( k -polytope-seq p = <*> {} & k -polytopes p = {} ) by Def5, Def7;
hence dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by FINSEQ_1:def_3; ::_thesis: verum
end;
end;
end;
theorem Th28: :: POLYFORM:28
for p being polyhedron
for k being Integer holds len (k -polytope-seq p) = num-polytopes (p,k)
proof
let p be polyhedron; ::_thesis: for k being Integer holds len (k -polytope-seq p) = num-polytopes (p,k)
let k be Integer; ::_thesis: len (k -polytope-seq p) = num-polytopes (p,k)
dom (k -polytope-seq p) = Seg (num-polytopes (p,k)) by Th27;
hence len (k -polytope-seq p) = num-polytopes (p,k) by FINSEQ_1:def_3; ::_thesis: verum
end;
theorem Th29: :: POLYFORM:29
for p being polyhedron
for k being Integer holds rng (k -polytope-seq p) = k -polytopes p
proof
let p be polyhedron; ::_thesis: for k being Integer holds rng (k -polytope-seq p) = k -polytopes p
let k be Integer; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
set F = the PolytopsF of p;
percases ( k < - 1 or ( - 1 <= k & k <= dim p ) or k > dim p ) ;
supposeA1: k < - 1 ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
then k -polytopes p = {} by Def5;
hence rng (k -polytope-seq p) = k -polytopes p by A1, Def7, RELAT_1:38; ::_thesis: verum
end;
supposeA2: ( - 1 <= k & k <= dim p ) ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
percases ( k = - 1 or ( - 1 < k & k < dim p ) or k = dim p ) by A2, XXREAL_0:1;
suppose k = - 1 ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
then ( k -polytopes p = {{}} & k -polytope-seq p = <*{}*> ) by Def5, Def7;
hence rng (k -polytope-seq p) = k -polytopes p by FINSEQ_1:38; ::_thesis: verum
end;
supposeA3: ( - 1 < k & k < dim p ) ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
then k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by Def5;
hence rng (k -polytope-seq p) = k -polytopes p by A3, Def7; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
then ( k -polytopes p = {p} & k -polytope-seq p = <*p*> ) by Def5, Def7;
hence rng (k -polytope-seq p) = k -polytopes p by FINSEQ_1:38; ::_thesis: verum
end;
end;
end;
supposeA4: k > dim p ; ::_thesis: rng (k -polytope-seq p) = k -polytopes p
then k -polytopes p = {} by Def5;
hence rng (k -polytope-seq p) = k -polytopes p by A4, Def7, RELAT_1:38; ::_thesis: verum
end;
end;
end;
theorem Th30: :: POLYFORM:30
for p being polyhedron holds num-polytopes (p,(- 1)) = 1
proof
let p be polyhedron; ::_thesis: num-polytopes (p,(- 1)) = 1
reconsider minusone = - 1 as Integer ;
minusone -polytopes p = {{}} by Def5;
hence num-polytopes (p,(- 1)) = 1 by CARD_1:30; ::_thesis: verum
end;
theorem Th31: :: POLYFORM:31
for p being polyhedron holds num-polytopes (p,(dim p)) = 1
proof
let p be polyhedron; ::_thesis: num-polytopes (p,(dim p)) = 1
(dim p) -polytopes p = {p} by Def5;
hence num-polytopes (p,(dim p)) = 1 by CARD_1:30; ::_thesis: verum
end;
definition
let p be polyhedron;
let k be Integer;
let n be Nat;
assume A1: ( 1 <= n & n <= num-polytopes (p,k) ) ;
funcn -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
n in Seg (num-polytopes (p,k)) by A1, FINSEQ_1:1;
then n in dom (k -polytope-seq p) by Th27;
then (k -polytope-seq p) . n in rng (k -polytope-seq p) by FUNCT_1:3;
hence (k -polytope-seq p) . n is Element of k -polytopes p by Th29; ::_thesis: verum
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 Th32: :: 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) )
proof
let p be polyhedron; ::_thesis: 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) )
let k be Integer; ::_thesis: ( - 1 <= k & k <= dim p implies 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) ) )
assume A1: ( - 1 <= k & k <= dim p ) ; ::_thesis: 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) )
let x be Element of k -polytopes p; ::_thesis: ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
percases ( k = - 1 or k = dim p or ( - 1 < k & k < dim p ) ) by A1, XXREAL_0:1;
supposeA2: k = - 1 ; ::_thesis: ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
reconsider n = 1 as Nat ;
k -polytope-seq p = <*{}*> by A2, Def7;
then A3: (k -polytope-seq p) . n = {} by FINSEQ_1:def_8;
take n ; ::_thesis: ( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
k -polytopes p = {{}} by A2, Def5;
then ( x = {} & n <= num-polytopes (p,k) ) by CARD_1:30, TARSKI:def_1;
hence ( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) ) by A3, Def12; ::_thesis: verum
end;
supposeA4: k = dim p ; ::_thesis: ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
reconsider n = 1 as Nat ;
k -polytope-seq p = <*p*> by A4, Def7;
then A5: (k -polytope-seq p) . n = p by FINSEQ_1:def_8;
take n ; ::_thesis: ( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
k -polytopes p = {p} by A4, Def5;
then ( x = p & num-polytopes (p,k) = 1 ) by CARD_1:30, TARSKI:def_1;
hence ( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) ) by A5, Def12; ::_thesis: verum
end;
supposeA6: ( - 1 < k & k < dim p ) ; ::_thesis: ex n being Nat st
( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) )
set F = the PolytopsF of p;
A7: k -polytopes p = rng ( the PolytopsF of p . (k + 1)) by A6, Def5;
A8: (- 1) + 1 < k + 1 by A6, XREAL_1:6;
then A9: 0 + 1 <= k + 1 by INT_1:7;
reconsider k9 = k + 1 as Element of NAT by A8, INT_1:3;
k + 1 <= dim p by A6, INT_1:7;
then not the PolytopsF of p . k9 is empty by A9, Def3;
then consider m being set such that
A10: m in dom ( the PolytopsF of p . k9) and
A11: ( the PolytopsF of p . k9) . m = x by A7, FUNCT_1:def_3;
reconsider Fk9 = the PolytopsF of p . k9 as FinSequence ;
reconsider m = m as Element of NAT by A10;
dom Fk9 = Seg (len Fk9) by FINSEQ_1:def_3;
then A12: ( 1 <= m & m <= len Fk9 ) by A10, FINSEQ_1:1;
take m ; ::_thesis: ( x = m -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) )
A13: k -polytope-seq p = the PolytopsF of p . (k + 1) by A6, Def7;
then num-polytopes (p,k) = len ( the PolytopsF of p . (k + 1)) by Th28;
hence ( x = m -th-polytope (p,k) & 1 <= m & m <= num-polytopes (p,k) ) by A13, A11, A12, Def12; ::_thesis: verum
end;
end;
end;
theorem Th33: :: POLYFORM:33
for p being polyhedron
for k being Integer holds k -polytope-seq p is one-to-one
proof
let p be polyhedron; ::_thesis: for k being Integer holds k -polytope-seq p is one-to-one
let k be Integer; ::_thesis: k -polytope-seq p is one-to-one
set s = k -polytope-seq p;
percases ( k < - 1 or k = - 1 or ( - 1 < k & k < dim p ) or k = dim p or k > dim p ) by XXREAL_0:1;
suppose k < - 1 ; ::_thesis: k -polytope-seq p is one-to-one
hence k -polytope-seq p is one-to-one by Def7; ::_thesis: verum
end;
suppose k = - 1 ; ::_thesis: k -polytope-seq p is one-to-one
hence k -polytope-seq p is one-to-one by Def7; ::_thesis: verum
end;
supposeA1: ( - 1 < k & k < dim p ) ; ::_thesis: k -polytope-seq p is one-to-one
then A2: (- 1) + 1 < k + 1 by XREAL_1:6;
then reconsider m = k + 1 as Element of NAT by INT_1:3;
set F = the PolytopsF of p;
A3: 0 + 1 <= m by A2, INT_1:7;
( k -polytope-seq p = the PolytopsF of p . (k + 1) & m <= dim p ) by A1, Def7, INT_1:7;
hence k -polytope-seq p is one-to-one by A3, Def3; ::_thesis: verum
end;
suppose k = dim p ; ::_thesis: k -polytope-seq p is one-to-one
then k -polytope-seq p = <*p*> by Def7;
hence k -polytope-seq p is one-to-one ; ::_thesis: verum
end;
suppose k > dim p ; ::_thesis: k -polytope-seq p is one-to-one
hence k -polytope-seq p is one-to-one by Def7; ::_thesis: verum
end;
end;
end;
theorem Th34: :: 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
proof
let p be polyhedron; ::_thesis: 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
let k be Integer; ::_thesis: 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
let m, n be Nat; ::_thesis: ( 1 <= n & n <= num-polytopes (p,k) & 1 <= m & m <= num-polytopes (p,k) & n -th-polytope (p,k) = m -th-polytope (p,k) implies m = n )
assume that
A1: ( 1 <= n & n <= num-polytopes (p,k) ) and
A2: ( 1 <= m & m <= num-polytopes (p,k) ) and
A3: n -th-polytope (p,k) = m -th-polytope (p,k) ; ::_thesis: m = n
set s = k -polytope-seq p;
A4: k -polytope-seq p is one-to-one by Th33;
m in Seg (num-polytopes (p,k)) by A2, FINSEQ_1:1;
then A5: m in dom (k -polytope-seq p) by Th27;
n in Seg (num-polytopes (p,k)) by A1, FINSEQ_1:1;
then A6: n in dom (k -polytope-seq p) by Th27;
( n -th-polytope (p,k) = (k -polytope-seq p) . n & m -th-polytope (p,k) = (k -polytope-seq p) . m ) by A1, A2, Def12;
hence m = n by A3, A6, A5, A4, FUNCT_1:def_4; ::_thesis: verum
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
set n = eta (p,k);
A3: (k - 1) -polytopes p <> {}
proof
set m = k - 1;
0 - 1 = - 1 ;
then A4: - 1 <= k - 1 by A1, XREAL_1:9;
k - 1 <= (dim p) - 0 by A2, XREAL_1:13;
hence (k - 1) -polytopes p <> {} by A4, Th25; ::_thesis: verum
end;
( dom (eta (p,k)) = [:((k - 1) -polytopes p),(k -polytopes p):] & k -polytopes p <> {} ) by A1, A2, Th25, FUNCT_2:92;
then [x,y] in dom (eta (p,k)) by A3, ZFMISC_1:87;
then (eta (p,k)) . [x,y] in rng (eta (p,k)) by FUNCT_1:3;
hence (eta (p,k)) . (x,y) is Element of Z_2 by BSPACE:3, BSPACE:5, BSPACE:6; ::_thesis: verum
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;
funck -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: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;
theorem Th36: :: POLYFORM:36
for p being polyhedron
for k being Integer holds num-polytopes (p,k) = dim (k -chain-space p)
proof
let p be polyhedron; ::_thesis: for k being Integer holds num-polytopes (p,k) = dim (k -chain-space p)
let k be Integer; ::_thesis: num-polytopes (p,k) = dim (k -chain-space p)
set n = dim (k -chain-space p);
singletons (k -polytopes p) is Basis of k -chain-space p by BSPACE:40;
then dim (k -chain-space p) = card (singletons (k -polytopes p)) by VECTSP_9:def_1;
hence num-polytopes (p,k) = dim (k -chain-space p) by BSPACE:41; ::_thesis: verum
end;
definition
let p be polyhedron;
let k be Integer;
funck -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 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)))) ) ) ) )
proof
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
supposeA1: (k - 1) -polytopes p is empty ; ::_thesis: 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)))) ) ) ) )
set s = <*> {};
rng (<*> {}) c= the carrier of Z_2 by XBOOLE_1:2;
then reconsider s = <*> {} as FinSequence of Z_2 by FINSEQ_1:def_4;
take s ; ::_thesis: ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )
thus ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ) by A1; ::_thesis: verum
end;
supposeA2: not (k - 1) -polytopes p is empty ; ::_thesis: 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)))) ) ) ) )
deffunc H1( Nat) -> Element of the carrier of Z_2 = (v @ ($1 -th-polytope (p,k))) * (incidence-value (x,($1 -th-polytope (p,k))));
consider s being FinSequence of Z_2 such that
A3: len s = num-polytopes (p,k) and
A4: for n being Nat st n in dom s holds
s . n = H1(n) from FINSEQ_2:sch_1();
take s ; ::_thesis: ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) )
A5: dom s = Seg (num-polytopes (p,k)) by A3, FINSEQ_1:def_3;
for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k))))
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= num-polytopes (p,k) implies s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) )
assume ( 1 <= n & n <= num-polytopes (p,k) ) ; ::_thesis: s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k))))
then n in Seg (num-polytopes (p,k)) by FINSEQ_1:1;
hence s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) by A4, A5; ::_thesis: verum
end;
hence ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ) by A2, A3; ::_thesis: verum
end;
end;
end;
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
proof
let s, t be FinSequence of Z_2; ::_thesis: ( ( (k - 1) -polytopes p is empty implies s = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) & ( (k - 1) -polytopes p is empty implies t = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len t = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
t . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) implies s = t )
assume that
A6: ( (k - 1) -polytopes p is empty implies s = <*> {} ) and
A7: ( not (k - 1) -polytopes p is empty implies ( len s = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) and
A8: ( (k - 1) -polytopes p is empty implies t = <*> {} ) and
A9: ( not (k - 1) -polytopes p is empty implies ( len t = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
t . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ; ::_thesis: s = t
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
suppose (k - 1) -polytopes p is empty ; ::_thesis: s = t
hence s = t by A6, A8; ::_thesis: verum
end;
supposeA10: not (k - 1) -polytopes p is empty ; ::_thesis: s = t
for n being Nat st 1 <= n & n <= len s holds
s . n = t . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len s implies s . n = t . n )
assume A11: ( 1 <= n & n <= len s ) ; ::_thesis: s . n = t . n
reconsider n = n as Nat ;
s . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) by A7, A10, A11;
hence s . n = t . n by A7, A9, A10, A11; ::_thesis: verum
end;
hence s = t by A7, A9, A10, FINSEQ_1:14; ::_thesis: verum
end;
end;
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 b5 being FinSequence of Z_2 holds
( b5 = incidence-sequence (x,v) iff ( ( (k - 1) -polytopes p is empty implies b5 = <*> {} ) & ( not (k - 1) -polytopes p is empty implies ( len b5 = num-polytopes (p,k) & ( for n being Nat st 1 <= n & n <= num-polytopes (p,k) holds
b5 . n = (v @ (n -th-polytope (p,k))) * (incidence-value (x,(n -th-polytope (p,k)))) ) ) ) ) );
theorem Th37: :: 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)
proof
let p be polyhedron; ::_thesis: 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)
let k be Integer; ::_thesis: 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)
let c, d be Element of (k -chain-space p); ::_thesis: for x being Element of k -polytopes p holds (c + d) @ x = (c @ x) + (d @ x)
let x be Element of k -polytopes p; ::_thesis: (c + d) @ x = (c @ x) + (d @ x)
c + d = c \+\ d by BSPACE:def_5;
hence (c + d) @ x = (c @ x) + (d @ x) by BSPACE:15; ::_thesis: verum
end;
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 - 1) -polytopes p holds incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
proof
let p be polyhedron; ::_thesis: 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))
let k be Integer; ::_thesis: 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))
let c, d be Element of (k -chain-space p); ::_thesis: for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
let x be Element of (k - 1) -polytopes p; ::_thesis: incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
set n = num-polytopes (p,k);
set l = incidence-sequence (x,(c + d));
set isc = incidence-sequence (x,c);
set isd = incidence-sequence (x,d);
set r = (incidence-sequence (x,c)) + (incidence-sequence (x,d));
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
supposeA1: (k - 1) -polytopes p is empty ; ::_thesis: incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
then incidence-sequence (x,d) is Tuple of 0 , the carrier of Z_2 by Def16;
then reconsider isd = incidence-sequence (x,d) as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:131;
incidence-sequence (x,c) = <*> the carrier of Z_2 by A1, Def16;
then reconsider isc = incidence-sequence (x,c) as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:131;
isc + isd is Element of 0 -tuples_on the carrier of Z_2 ;
hence incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d)) by A1, Def16; ::_thesis: verum
end;
supposeA2: not (k - 1) -polytopes p is empty ; ::_thesis: incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d))
A3: ( len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) & len ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = num-polytopes (p,k) )
proof
len (incidence-sequence (x,d)) = num-polytopes (p,k) by A2, Def16;
then reconsider isd = incidence-sequence (x,d) as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 by FINSEQ_2:92;
len (incidence-sequence (x,c)) = num-polytopes (p,k) by A2, Def16;
then reconsider isc = incidence-sequence (x,c) as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 by FINSEQ_2:92;
reconsider s = isc + isd as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 ;
len s = num-polytopes (p,k) by CARD_1:def_7;
hence ( len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) & len ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = num-polytopes (p,k) ) by A2, Def16; ::_thesis: verum
end;
for n being Nat st 1 <= n & n <= len (incidence-sequence (x,(c + d))) holds
(incidence-sequence (x,(c + d))) . n = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . n
proof
A4: ( dom ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = Seg (num-polytopes (p,k)) & len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) ) by A3, FINSEQ_1:def_3;
let m be Nat; ::_thesis: ( 1 <= m & m <= len (incidence-sequence (x,(c + d))) implies (incidence-sequence (x,(c + d))) . m = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m )
assume A5: ( 1 <= m & m <= len (incidence-sequence (x,(c + d))) ) ; ::_thesis: (incidence-sequence (x,(c + d))) . m = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m
set a = m -th-polytope (p,k);
set iva = incidence-value (x,(m -th-polytope (p,k)));
A6: len (incidence-sequence (x,(c + d))) = num-polytopes (p,k) by A2, Def16;
then A7: (incidence-sequence (x,(c + d))) . m = ((c + d) @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) by A2, A5, Def16;
m in NAT by ORDINAL1:def_12;
then A8: m in dom ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) by A4, A5;
( (incidence-sequence (x,c)) . m = (c @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) & (incidence-sequence (x,d)) . m = (d @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) ) by A2, A5, A6, Def16;
then ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m = ((c @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k))))) + ((d @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k))))) by A8, FVSUM_1:17
.= ((c @ (m -th-polytope (p,k))) + (d @ (m -th-polytope (p,k)))) * (incidence-value (x,(m -th-polytope (p,k)))) by VECTSP_1:def_3
.= (incidence-sequence (x,(c + d))) . m by A7, Th37 ;
hence (incidence-sequence (x,(c + d))) . m = ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) . m ; ::_thesis: verum
end;
hence incidence-sequence (x,(c + d)) = (incidence-sequence (x,c)) + (incidence-sequence (x,d)) by A3, FINSEQ_1:14; ::_thesis: verum
end;
end;
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 Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
proof
let p be polyhedron; ::_thesis: 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)))
let k be Integer; ::_thesis: 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)))
let c, d be Element of (k -chain-space p); ::_thesis: 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)))
let x be Element of (k - 1) -polytopes p; ::_thesis: Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
set isc = incidence-sequence (x,c);
set isd = incidence-sequence (x,d);
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
supposeA1: (k - 1) -polytopes p is empty ; ::_thesis: Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
then incidence-sequence (x,d) = <*> the carrier of Z_2 by Def16;
then reconsider isd = incidence-sequence (x,d) as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:131;
incidence-sequence (x,c) = <*> the carrier of Z_2 by A1, Def16;
then reconsider isc = incidence-sequence (x,c) as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:131;
reconsider s = isc + isd as Element of 0 -tuples_on the carrier of Z_2 ;
Sum s = 0. Z_2 by FVSUM_1:74;
hence Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) by RLVECT_1:def_4; ::_thesis: verum
end;
supposeA2: not (k - 1) -polytopes p is empty ; ::_thesis: Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
reconsider n = num-polytopes (p,k) as Element of NAT ;
len (incidence-sequence (x,d)) = n by A2, Def16;
then reconsider isd9 = incidence-sequence (x,d) as Element of n -tuples_on the carrier of Z_2 by FINSEQ_2:92;
len (incidence-sequence (x,c)) = n by A2, Def16;
then reconsider isc9 = incidence-sequence (x,c) as Element of n -tuples_on the carrier of Z_2 by FINSEQ_2:92;
Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = Sum (isc9 + isd9)
.= (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) by FVSUM_1:76 ;
hence Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) ; ::_thesis: verum
end;
end;
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 + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
proof
let p be polyhedron; ::_thesis: 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)))
let k be Integer; ::_thesis: 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)))
let c, d be Element of (k -chain-space p); ::_thesis: 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)))
let x be Element of (k - 1) -polytopes p; ::_thesis: Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d)))
Sum (incidence-sequence (x,(c + d))) = Sum ((incidence-sequence (x,c)) + (incidence-sequence (x,d))) by Th38
.= (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) by Th39 ;
hence Sum (incidence-sequence (x,(c + d))) = (Sum (incidence-sequence (x,c))) + (Sum (incidence-sequence (x,d))) ; ::_thesis: verum
end;
theorem Th41: :: 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)
proof
let p be polyhedron; ::_thesis: 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)
let k be Integer; ::_thesis: 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)
let c be Element of (k -chain-space p); ::_thesis: for a being Element of Z_2
for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
let a be Element of Z_2; ::_thesis: for x being Element of k -polytopes p holds (a * c) @ x = a * (c @ x)
let x be Element of k -polytopes p; ::_thesis: (a * c) @ x = a * (c @ x)
percases ( a = 0. Z_2 or a = 1. Z_2 ) by BSPACE:8;
suppose a = 0. Z_2 ; ::_thesis: (a * c) @ x = a * (c @ x)
then ( a * (c @ x) = 0. Z_2 & a * c = 0. (k -chain-space p) ) by VECTSP_1:7, VECTSP_1:14;
hence (a * c) @ x = a * (c @ x) by BSPACE:14; ::_thesis: verum
end;
supposeA1: a = 1. Z_2 ; ::_thesis: (a * c) @ x = a * (c @ x)
then a * (c @ x) = c @ x by VECTSP_1:def_6;
hence (a * c) @ x = a * (c @ x) by A1, VECTSP_1:def_17; ::_thesis: verum
end;
end;
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 - 1) -polytopes p holds incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
proof
let p be polyhedron; ::_thesis: 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))
let k be Integer; ::_thesis: 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))
let c be Element of (k -chain-space p); ::_thesis: 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))
let a be Element of Z_2; ::_thesis: for x being Element of (k - 1) -polytopes p holds incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
let x be Element of (k - 1) -polytopes p; ::_thesis: incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
set l = incidence-sequence (x,(a * c));
set isc = incidence-sequence (x,c);
set r = a * (incidence-sequence (x,c));
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
supposeA1: (k - 1) -polytopes p is empty ; ::_thesis: incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
then incidence-sequence (x,c) = <*> the carrier of Z_2 by Def16;
then reconsider isc = incidence-sequence (x,c) as Element of 0 -tuples_on the carrier of Z_2 by FINSEQ_2:131;
a * isc is Element of 0 -tuples_on the carrier of Z_2 ;
then reconsider r = a * (incidence-sequence (x,c)) as Element of 0 -tuples_on the carrier of Z_2 ;
r = <*> the carrier of Z_2 ;
hence incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c)) by A1, Def16; ::_thesis: verum
end;
supposeA2: not (k - 1) -polytopes p is empty ; ::_thesis: incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c))
set n = num-polytopes (p,k);
A3: ( len (incidence-sequence (x,(a * c))) = num-polytopes (p,k) & len (a * (incidence-sequence (x,c))) = num-polytopes (p,k) )
proof
len (incidence-sequence (x,c)) = num-polytopes (p,k) by A2, Def16;
then reconsider isc = incidence-sequence (x,c) as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 by FINSEQ_2:92;
set r = a * isc;
reconsider r = a * isc as Element of (num-polytopes (p,k)) -tuples_on the carrier of Z_2 ;
len r = num-polytopes (p,k) by CARD_1:def_7;
hence ( len (incidence-sequence (x,(a * c))) = num-polytopes (p,k) & len (a * (incidence-sequence (x,c))) = num-polytopes (p,k) ) by A2, Def16; ::_thesis: verum
end;
for m being Nat st 1 <= m & m <= len (incidence-sequence (x,(a * c))) holds
(incidence-sequence (x,(a * c))) . m = (a * (incidence-sequence (x,c))) . m
proof
A4: dom (a * (incidence-sequence (x,c))) = Seg (num-polytopes (p,k)) by A3, FINSEQ_1:def_3;
let m be Nat; ::_thesis: ( 1 <= m & m <= len (incidence-sequence (x,(a * c))) implies (incidence-sequence (x,(a * c))) . m = (a * (incidence-sequence (x,c))) . m )
assume A5: ( 1 <= m & m <= len (incidence-sequence (x,(a * c))) ) ; ::_thesis: (incidence-sequence (x,(a * c))) . m = (a * (incidence-sequence (x,c))) . m
set s = m -th-polytope (p,k);
set ivs = incidence-value (x,(m -th-polytope (p,k)));
A6: len (incidence-sequence (x,(a * c))) = num-polytopes (p,k) by A2, Def16;
then A7: (incidence-sequence (x,(a * c))) . m = ((a * c) @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) by A2, A5, Def16;
( len (incidence-sequence (x,(a * c))) = num-polytopes (p,k) & m in NAT ) by A2, Def16, ORDINAL1:def_12;
then A8: m in Seg (num-polytopes (p,k)) by A5;
(incidence-sequence (x,c)) . m = (c @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k)))) by A2, A5, A6, Def16;
then (a * (incidence-sequence (x,c))) . m = a * ((c @ (m -th-polytope (p,k))) * (incidence-value (x,(m -th-polytope (p,k))))) by A4, A8, FVSUM_1:50
.= (a * (c @ (m -th-polytope (p,k)))) * (incidence-value (x,(m -th-polytope (p,k)))) by GROUP_1:def_3
.= (incidence-sequence (x,(a * c))) . m by A7, Th41 ;
hence (incidence-sequence (x,(a * c))) . m = (a * (incidence-sequence (x,c))) . m ; ::_thesis: verum
end;
hence incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c)) by A3, FINSEQ_1:14; ::_thesis: verum
end;
end;
end;
theorem Th43: :: 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 )
proof
let p be polyhedron; ::_thesis: 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 )
let k be Integer; ::_thesis: 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 )
let c, d be Element of (k -chain-space p); ::_thesis: ( c = d iff for x being Element of k -polytopes p holds c @ x = d @ x )
thus ( c = d implies for x being Element of k -polytopes p holds c @ x = d @ x ) ; ::_thesis: ( ( for x being Element of k -polytopes p holds c @ x = d @ x ) implies c = d )
thus ( ( for x being Element of k -polytopes p holds c @ x = d @ x ) implies c = d ) ::_thesis: verum
proof
assume A1: for x being Element of k -polytopes p holds c @ x = d @ x ; ::_thesis: c = d
thus c c= d :: according to XBOOLE_0:def_10 ::_thesis: d c= c
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in c or x in d )
assume A2: x in c ; ::_thesis: x in d
reconsider x = x as Element of k -polytopes p by A2;
reconsider c = c as Subset of (k -polytopes p) ;
c @ x = 1. Z_2 by A2, BSPACE:def_3;
then d @ x = 1. Z_2 by A1;
hence x in d by BSPACE:9; ::_thesis: verum
end;
thus d c= c ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in d or x in c )
assume A3: x in d ; ::_thesis: x in c
reconsider x = x as Element of k -polytopes p by A3;
reconsider d = d as Subset of (k -polytopes p) ;
d @ x = 1. Z_2 by A3, BSPACE:def_3;
then c @ x = 1. Z_2 by A1;
hence x in c by BSPACE:9; ::_thesis: verum
end;
end;
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
( x in c iff x in d ) )
proof
let p be polyhedron; ::_thesis: 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 ) )
let k be Integer; ::_thesis: 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 ) )
let c, d be Element of (k -chain-space p); ::_thesis: ( c = d iff for x being Element of k -polytopes p holds
( x in c iff x in d ) )
thus ( c = d implies for x being Element of k -polytopes p holds
( x in c iff x in d ) ) ; ::_thesis: ( ( for x being Element of k -polytopes p holds
( x in c iff x in d ) ) implies c = d )
thus ( ( for x being Element of k -polytopes p holds
( x in c iff x in d ) ) implies c = d ) ::_thesis: verum
proof
assume A1: for x being Element of k -polytopes p holds
( x in c iff x in d ) ; ::_thesis: c = d
assume c <> d ; ::_thesis: contradiction
then consider x being Element of k -polytopes p such that
A2: c @ x <> d @ x by Th43;
( ( x in c & not x in d ) or ( x in d & not x in c ) ) by A2, BSPACE:13;
hence contradiction by A1; ::_thesis: verum
end;
end;
scheme :: POLYFORM:sch 1
ChainEx{ F1() -> polyhedron, F2() -> Integer, P1[ Element of F2() -polytopes F1()] } :
ex c being Subset of (F2() -polytopes F1()) st
for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
proof
set c = { x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() ) } ;
{ x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() ) } c= F2() -polytopes F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() ) } or x in F2() -polytopes F1() )
assume x in { x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() ) } ; ::_thesis: x in F2() -polytopes F1()
then ex y being Element of F2() -polytopes F1() st
( x = y & P1[y] & y in F2() -polytopes F1() ) ;
hence x in F2() -polytopes F1() ; ::_thesis: verum
end;
then reconsider c = { x where x is Element of F2() -polytopes F1() : ( P1[x] & x in F2() -polytopes F1() ) } as Subset of (F2() -polytopes F1()) ;
take c ; ::_thesis: for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
proof
let x be Element of F2() -polytopes F1(); ::_thesis: ( x in c iff ( P1[x] & x in F2() -polytopes F1() ) )
thus ( x in c implies ( P1[x] & x in F2() -polytopes F1() ) ) ::_thesis: ( P1[x] & x in F2() -polytopes F1() implies x in c )
proof
assume x in c ; ::_thesis: ( P1[x] & x in F2() -polytopes F1() )
then ex y being Element of F2() -polytopes F1() st
( y = x & P1[y] & y in F2() -polytopes F1() ) ;
hence ( P1[x] & x in F2() -polytopes F1() ) ; ::_thesis: verum
end;
thus ( P1[x] & x in F2() -polytopes F1() implies x in c ) ; ::_thesis: verum
end;
hence for x being Element of F2() -polytopes F1() holds
( x in c iff ( P1[x] & x in F2() -polytopes F1() ) ) ; ::_thesis: verum
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 b1 being Element of ((k - 1) -chain-space p) st
( ( (k - 1) -polytopes p is empty implies b1 = 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 b1 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) )
proof
defpred S1[ Element of (k - 1) -polytopes p] means Sum (incidence-sequence ($1,v)) = 1. Z_2;
consider c being Subset of ((k - 1) -polytopes p) such that
A1: for x being Element of (k - 1) -polytopes p holds
( x in c iff ( S1[x] & x in (k - 1) -polytopes p ) ) from POLYFORM:sch_1();
reconsider c = c as Element of ((k - 1) -chain-space p) ;
take c ; ::_thesis: ( ( (k - 1) -polytopes p is empty implies c = 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 c iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) )
thus ( ( (k - 1) -polytopes p is empty implies c = 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 c iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of ((k - 1) -chain-space p) st ( (k - 1) -polytopes p is empty implies b1 = 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 b1 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) & ( (k - 1) -polytopes p is empty implies b2 = 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 b2 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) holds
b1 = b2
proof
let c, d be Element of ((k - 1) -chain-space p); ::_thesis: ( ( (k - 1) -polytopes p is empty implies c = 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 c iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) & ( (k - 1) -polytopes p is empty implies d = 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 d iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) implies c = d )
assume that
A2: ( (k - 1) -polytopes p is empty implies c = 0. ((k - 1) -chain-space p) ) and
A3: ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in c iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) and
( (k - 1) -polytopes p is empty implies d = 0. ((k - 1) -chain-space p) ) and
A4: ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in d iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) ; ::_thesis: c = d
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
suppose (k - 1) -polytopes p is empty ; ::_thesis: c = d
hence c = d by A2; ::_thesis: verum
end;
supposeA5: not (k - 1) -polytopes p is empty ; ::_thesis: c = d
for x being Element of (k - 1) -polytopes p holds
( x in c iff x in d )
proof
let x be Element of (k - 1) -polytopes p; ::_thesis: ( x in c iff x in d )
thus ( x in c implies x in d ) ::_thesis: ( x in d implies x in c )
proof
assume x in c ; ::_thesis: x in d
then Sum (incidence-sequence (x,v)) = 1. Z_2 by A3;
hence x in d by A4, A5; ::_thesis: verum
end;
thus ( x in d implies x in c ) ::_thesis: verum
proof
assume x in d ; ::_thesis: x in c
then Sum (incidence-sequence (x,v)) = 1. Z_2 by A4;
hence x in c by A3, A5; ::_thesis: verum
end;
end;
hence c = d by Th44; ::_thesis: verum
end;
end;
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 b4 being Element of ((k - 1) -chain-space p) holds
( b4 = Boundary v iff ( ( (k - 1) -polytopes p is empty implies b4 = 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 b4 iff Sum (incidence-sequence (x,v)) = 1. Z_2 ) ) ) );
theorem Th45: :: 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))
proof
let p be polyhedron; ::_thesis: 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))
let k be Integer; ::_thesis: 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))
let c be Element of (k -chain-space p); ::_thesis: for x being Element of (k - 1) -polytopes p holds (Boundary c) @ x = Sum (incidence-sequence (x,c))
let x be Element of (k - 1) -polytopes p; ::_thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
set b = Boundary c;
percases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;
supposeA1: (k - 1) -polytopes p is empty ; ::_thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
set iscx = incidence-sequence (x,c);
incidence-sequence (x,c) = <*> the carrier of Z_2 by A1, Def16;
then A2: Sum (incidence-sequence (x,c)) = 0. Z_2 by RLVECT_1:43;
Boundary c = 0. ((k - 1) -chain-space p) by A1;
hence (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A2, BSPACE:14; ::_thesis: verum
end;
supposeA3: not (k - 1) -polytopes p is empty ; ::_thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
then A4: ( x in Boundary c iff Sum (incidence-sequence (x,c)) = 1. Z_2 ) by Def17;
percases ( x in Boundary c or not x in Boundary c ) ;
suppose x in Boundary c ; ::_thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
hence (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A4, BSPACE:def_3; ::_thesis: verum
end;
supposeA5: not x in Boundary c ; ::_thesis: (Boundary c) @ x = Sum (incidence-sequence (x,c))
then Sum (incidence-sequence (x,c)) <> 1. Z_2 by A3, Def17;
then Sum (incidence-sequence (x,c)) = 0. Z_2 by BSPACE:8;
hence (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A5, BSPACE:def_3; ::_thesis: verum
end;
end;
end;
end;
end;
definition
let p be polyhedron;
let k be Integer;
funck -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 b1 being Function of (k -chain-space p),((k - 1) -chain-space p) st
for c being Element of (k -chain-space p) holds b1 . c = Boundary c
proof
defpred S1[ set , set ] means ex c being Element of (k -chain-space p) st
( $1 = c & $2 = Boundary c );
A1: for x being set st x in k -chains p holds
ex y being set st
( y in (k - 1) -chains p & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in k -chains p implies ex y being set st
( y in (k - 1) -chains p & S1[x,y] ) )
assume x in k -chains p ; ::_thesis: ex y being set st
( y in (k - 1) -chains p & S1[x,y] )
then reconsider x = x as Element of (k -chain-space p) ;
set b = Boundary x;
take Boundary x ; ::_thesis: ( Boundary x in (k - 1) -chains p & S1[x, Boundary x] )
thus ( Boundary x in (k - 1) -chains p & S1[x, Boundary x] ) ; ::_thesis: verum
end;
consider f being Function of (k -chains p),((k - 1) -chains p) such that
A2: for x being set st x in k -chains p holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
reconsider f = f as Function of (k -chain-space p),((k - 1) -chain-space p) ;
take f ; ::_thesis: for c being Element of (k -chain-space p) holds f . c = Boundary c
for c being Element of (k -chain-space p) holds f . c = Boundary c
proof
let c be Element of (k -chain-space p); ::_thesis: f . c = Boundary c
S1[c,f . c] by A2;
hence f . c = Boundary c ; ::_thesis: verum
end;
hence for c being Element of (k -chain-space p) holds f . c = Boundary c ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (k -chain-space p),((k - 1) -chain-space p) st ( for c being Element of (k -chain-space p) holds b1 . c = Boundary c ) & ( for c being Element of (k -chain-space p) holds b2 . c = Boundary c ) holds
b1 = b2
proof
let f, g be Function of (k -chain-space p),((k - 1) -chain-space p); ::_thesis: ( ( for c being Element of (k -chain-space p) holds f . c = Boundary c ) & ( for c being Element of (k -chain-space p) holds g . c = Boundary c ) implies f = g )
assume that
A3: for c being Element of (k -chain-space p) holds f . c = Boundary c and
A4: for c being Element of (k -chain-space p) holds g . c = Boundary c ; ::_thesis: f = g
A5: for x being set st x in dom f holds
f . x = g . x
proof
let x be set ; ::_thesis: ( x in dom f implies f . x = g . x )
assume x in dom f ; ::_thesis: f . x = g . x
then reconsider x = x as Element of (k -chain-space p) ;
f . x = Boundary x by A3;
hence f . x = g . x by A4; ::_thesis: verum
end;
dom f = [#] (k -chain-space p) by FUNCT_2:def_1;
then dom f = dom g by FUNCT_2:def_1;
hence f = g by A5, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines -boundary POLYFORM:def_18_:_
for p being polyhedron
for k being Integer
for b3 being Function of (k -chain-space p),((k - 1) -chain-space p) holds
( b3 = k -boundary p iff for c being Element of (k -chain-space p) holds b3 . c = Boundary c );
theorem Th46: :: 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)
proof
let p be polyhedron; ::_thesis: for k being Integer
for c, d being Element of (k -chain-space p) holds Boundary (c + d) = (Boundary c) + (Boundary d)
let k be Integer; ::_thesis: for c, d being Element of (k -chain-space p) holds Boundary (c + d) = (Boundary c) + (Boundary d)
let c, d be Element of (k -chain-space p); ::_thesis: Boundary (c + d) = (Boundary c) + (Boundary d)
set bc = Boundary c;
set bd = Boundary d;
set s = c + d;
set l = Boundary (c + d);
set r = (Boundary c) + (Boundary d);
for x being Element of (k - 1) -polytopes p holds (Boundary (c + d)) @ x = ((Boundary c) + (Boundary d)) @ x
proof
let x be Element of (k - 1) -polytopes p; ::_thesis: (Boundary (c + d)) @ x = ((Boundary c) + (Boundary d)) @ x
set a = (Boundary c) @ x;
set b = (Boundary d) @ x;
A1: ( (Boundary c) @ x = Sum (incidence-sequence (x,c)) & (Boundary d) @ x = Sum (incidence-sequence (x,d)) ) by Th45;
( (Boundary (c + d)) @ x = Sum (incidence-sequence (x,(c + d))) & ((Boundary c) + (Boundary d)) @ x = ((Boundary c) @ x) + ((Boundary d) @ x) ) by Th37, Th45;
hence (Boundary (c + d)) @ x = ((Boundary c) + (Boundary d)) @ x by A1, Th40; ::_thesis: verum
end;
hence Boundary (c + d) = (Boundary c) + (Boundary d) by Th43; ::_thesis: verum
end;
theorem Th47: :: 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)
proof
let p be polyhedron; ::_thesis: 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)
let k be Integer; ::_thesis: for a being Element of Z_2
for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)
let a be Element of Z_2; ::_thesis: for c being Element of (k -chain-space p) holds Boundary (a * c) = a * (Boundary c)
let c be Element of (k -chain-space p); ::_thesis: Boundary (a * c) = a * (Boundary c)
set lsm = a * c;
set l = Boundary (a * c);
set rb = Boundary c;
set r = a * (Boundary c);
for x being Element of (k - 1) -polytopes p holds (Boundary (a * c)) @ x = (a * (Boundary c)) @ x
proof
let x be Element of (k - 1) -polytopes p; ::_thesis: (Boundary (a * c)) @ x = (a * (Boundary c)) @ x
set b = (Boundary c) @ x;
A1: ( (Boundary (a * c)) @ x = Sum (incidence-sequence (x,(a * c))) & (Boundary c) @ x = Sum (incidence-sequence (x,c)) ) by Th45;
( (a * (Boundary c)) @ x = a * ((Boundary c) @ x) & incidence-sequence (x,(a * c)) = a * (incidence-sequence (x,c)) ) by Th41, Th42;
hence (Boundary (a * c)) @ x = (a * (Boundary c)) @ x by A1, FVSUM_1:73; ::_thesis: verum
end;
hence Boundary (a * c) = a * (Boundary c) by Th43; ::_thesis: verum
end;
theorem Th48: :: 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)
proof
let p be polyhedron; ::_thesis: for k being Integer holds k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)
let k be Integer; ::_thesis: k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p)
set V = k -chain-space p;
set b = k -boundary p;
A1: for a being Element of Z_2
for x being Element of (k -chain-space p) holds (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
proof
let a be Element of Z_2; ::_thesis: for x being Element of (k -chain-space p) holds (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
let x be Element of (k -chain-space p); ::_thesis: (k -boundary p) . (a * x) = a * ((k -boundary p) . x)
(k -boundary p) . (a * x) = Boundary (a * x) by Def18
.= a * (Boundary x) by Th47
.= a * ((k -boundary p) . x) by Def18 ;
hence (k -boundary p) . (a * x) = a * ((k -boundary p) . x) ; ::_thesis: verum
end;
for x, y being Element of (k -chain-space p) holds (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y)
proof
let x, y be Element of (k -chain-space p); ::_thesis: (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y)
(k -boundary p) . (x + y) = Boundary (x + y) by Def18
.= (Boundary x) + (Boundary y) by Th46
.= ((k -boundary p) . x) + (Boundary y) by Def18
.= ((k -boundary p) . x) + ((k -boundary p) . y) by Def18 ;
hence (k -boundary p) . (x + y) = ((k -boundary p) . x) + ((k -boundary p) . y) ; ::_thesis: verum
end;
then ( k -boundary p is additive & k -boundary p is homogeneous ) by A1, VECTSP_1:def_20, MOD_2:def_2;
hence k -boundary p is linear-transformation of (k -chain-space p),((k - 1) -chain-space p) ; ::_thesis: verum
end;
registration
let p be polyhedron;
let k be Integer;
clusterk -boundary p -> additive homogeneous ;
coherence
( k -boundary p is homogeneous & k -boundary p is additive ) by Th48;
end;
definition
let p be polyhedron;
let k be Integer;
funck -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;
funck -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;
funck -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;
funck -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;
funck -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;
funck -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: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;
begin
definition
let p be polyhedron;
attrp 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 Th50: :: 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 )
proof
let p be polyhedron; ::_thesis: ( p is simply-connected iff for n being Integer holds n -circuit-space p = n -bounding-chain-space p )
defpred S1[ polyhedron] means for n being Integer holds n -circuit-space $1 = n -bounding-chain-space $1;
thus ( p is simply-connected implies S1[p] ) ::_thesis: ( ( for n being Integer holds n -circuit-space p = n -bounding-chain-space p ) implies p is simply-connected )
proof
assume A1: p is simply-connected ; ::_thesis: S1[p]
let n be Integer; ::_thesis: n -circuit-space p = n -bounding-chain-space p
n -circuits p = n -bounding-chains p by A1, Def25;
hence n -circuit-space p = n -bounding-chain-space p by VECTSP_4:29; ::_thesis: verum
end;
thus ( S1[p] implies p is simply-connected ) ::_thesis: verum
proof
assume A2: S1[p] ; ::_thesis: p is simply-connected
let n be Integer; :: according to POLYFORM:def_25 ::_thesis: n -circuits p = n -bounding-chains p
thus n -circuits p = n -bounding-chains p by A2; ::_thesis: verum
end;
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 b1 being FinSequence of INT st
( len b1 = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b1 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) )
proof
deffunc H1( Nat) -> Element of INT = ((- 1) |^ $1) * (num-polytopes (p,($1 - 2)));
consider s being FinSequence of INT such that
A1: len s = (dim p) + 2 and
A2: for j being Nat st j in dom s holds
s . j = H1(j) from FINSEQ_2:sch_1();
take s ; ::_thesis: ( len s = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) )
A3: dom s = Seg ((dim p) + 2) by A1, FINSEQ_1:def_3;
for j being Nat st 1 <= j & j <= (dim p) + 2 holds
s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2)))
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= (dim p) + 2 implies s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2))) )
assume ( 1 <= j & j <= (dim p) + 2 ) ; ::_thesis: s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2)))
then j in Seg ((dim p) + 2) by FINSEQ_1:1;
hence s . j = ((- 1) |^ j) * (num-polytopes (p,(j - 2))) by A2, A3; ::_thesis: verum
end;
hence ( len s = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of INT st len b1 = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b1 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) & len b2 = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b2 . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) holds
b1 = b2
proof
let s, t be FinSequence of INT ; ::_thesis: ( len s = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) & len t = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
t . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) implies s = t )
assume that
A4: len s = (dim p) + 2 and
A5: for k being Nat st 1 <= k & k <= (dim p) + 2 holds
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) and
A6: len t = (dim p) + 2 and
A7: for k being Nat st 1 <= k & k <= (dim p) + 2 holds
t . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ; ::_thesis: s = t
for k being Nat st 1 <= k & k <= len s holds
s . k = t . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len s implies s . k = t . k )
assume A8: ( 1 <= k & k <= len s ) ; ::_thesis: s . k = t . k
reconsider k = k as Nat ;
s . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) by A4, A5, A8;
hence s . k = t . k by A4, A7, A8; ::_thesis: verum
end;
hence s = t by A4, A6, FINSEQ_1:14; ::_thesis: verum
end;
end;
:: deftheorem Def26 defines alternating-f-vector POLYFORM:def_26_:_
for p being polyhedron
for b2 being FinSequence of INT holds
( b2 = alternating-f-vector p iff ( len b2 = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b2 . 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 b1 being FinSequence of INT st
( len b1 = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )
proof
deffunc H1( Nat) -> Element of INT = ((- 1) |^ ($1 + 1)) * (num-polytopes (p,($1 - 1)));
consider s being FinSequence of INT such that
A1: len s = dim p and
A2: for j being Nat st j in dom s holds
s . j = H1(j) from FINSEQ_2:sch_1();
take s ; ::_thesis: ( len s = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )
A3: dom s = Seg (dim p) by A1, FINSEQ_1:def_3;
for j being Nat st 1 <= j & j <= dim p holds
s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1)))
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= dim p implies s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1))) )
assume ( 1 <= j & j <= dim p ) ; ::_thesis: s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1)))
then j in Seg (dim p) by FINSEQ_1:1;
hence s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1))) by A2, A3; ::_thesis: verum
end;
hence ( len s = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of INT st len b1 = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len b2 = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) holds
b1 = b2
proof
let s, t be FinSequence of INT ; ::_thesis: ( len s = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len t = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
t . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) implies s = t )
assume that
A4: len s = dim p and
A5: for k being Nat st 1 <= k & k <= dim p holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) and
A6: len t = dim p and
A7: for k being Nat st 1 <= k & k <= dim p holds
t . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ; ::_thesis: s = t
for k being Nat st 1 <= k & k <= len s holds
s . k = t . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len s implies s . k = t . k )
assume A8: ( 1 <= k & k <= len s ) ; ::_thesis: s . k = t . k
reconsider k = k as Nat ;
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) by A4, A5, A8;
hence s . k = t . k by A4, A7, A8; ::_thesis: verum
end;
hence s = t by A4, A6, FINSEQ_1:14; ::_thesis: verum
end;
end;
:: deftheorem Def27 defines alternating-proper-f-vector POLYFORM:def_27_:_
for p being polyhedron
for b2 being FinSequence of INT holds
( b2 = alternating-proper-f-vector p iff ( len b2 = dim p & ( for k being Nat st 1 <= k & k <= dim p holds
b2 . 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 b1 being FinSequence of INT st
( len b1 = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )
proof
deffunc H1( Nat) -> Element of INT = ((- 1) |^ ($1 + 1)) * (num-polytopes (p,($1 - 1)));
consider s being FinSequence of INT such that
A1: len s = (dim p) + 1 and
A2: for j being Nat st j in dom s holds
s . j = H1(j) from FINSEQ_2:sch_1();
take s ; ::_thesis: ( len s = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) )
A3: dom s = Seg ((dim p) + 1) by A1, FINSEQ_1:def_3;
for j being Nat st 1 <= j & j <= (dim p) + 1 holds
s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1)))
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= (dim p) + 1 implies s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1))) )
assume ( 1 <= j & j <= (dim p) + 1 ) ; ::_thesis: s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1)))
then j in Seg ((dim p) + 1) by FINSEQ_1:1;
hence s . j = ((- 1) |^ (j + 1)) * (num-polytopes (p,(j - 1))) by A2, A3; ::_thesis: verum
end;
hence ( len s = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of INT st len b1 = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
b1 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len b2 = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) holds
b1 = b2
proof
let s, t be FinSequence of INT ; ::_thesis: ( len s = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) & len t = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
t . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) implies s = t )
assume that
A4: len s = (dim p) + 1 and
A5: for k being Nat st 1 <= k & k <= (dim p) + 1 holds
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) and
A6: len t = (dim p) + 1 and
A7: for k being Nat st 1 <= k & k <= (dim p) + 1 holds
t . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ; ::_thesis: s = t
for k being Nat st 1 <= k & k <= len s holds
s . k = t . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len s implies s . k = t . k )
assume A8: ( 1 <= k & k <= len s ) ; ::_thesis: s . k = t . k
reconsider k = k as Nat ;
s . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) by A4, A5, A8;
hence s . k = t . k by A4, A7, A8; ::_thesis: verum
end;
hence s = t by A4, A6, FINSEQ_1:14; ::_thesis: verum
end;
end;
:: deftheorem Def28 defines alternating-semi-proper-f-vector POLYFORM:def_28_:_
for p being polyhedron
for b2 being FinSequence of INT holds
( b2 = alternating-semi-proper-f-vector p iff ( len b2 = (dim p) + 1 & ( for k being Nat st 1 <= k & k <= (dim p) + 1 holds
b2 . k = ((- 1) |^ (k + 1)) * (num-polytopes (p,(k - 1))) ) ) );
theorem Th51: :: 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)))
proof
let p be polyhedron; ::_thesis: 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)))
let n be Nat; ::_thesis: ( 1 <= n & n <= len (alternating-proper-f-vector p) implies (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))) )
set apcs = alternating-proper-f-vector p;
assume A1: 1 <= n ; ::_thesis: ( not n <= len (alternating-proper-f-vector p) or (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))) )
set a = (- 1) |^ (n + 1);
assume n <= len (alternating-proper-f-vector p) ; ::_thesis: (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)))
then n <= dim p by Def27;
then (alternating-proper-f-vector p) . n = ((- 1) |^ (n + 1)) * (num-polytopes (p,(n - 1))) by A1, Def27
.= ((- 1) |^ (n + 1)) * (dim ((n - 1) -chain-space p)) by Th36
.= ((- 1) |^ (n + 1)) * ((rank ((n - 1) -boundary p)) + (nullity ((n - 1) -boundary p))) by RANKNULL:44
.= (((- 1) |^ (n + 1)) * (dim ((n - 2) -bounding-chain-space p))) + (((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p))) ;
hence (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))) ; ::_thesis: verum
end;
definition
let p be polyhedron;
attrp 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 Th52: :: POLYFORM:52
for p being polyhedron holds alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>
proof
let p be polyhedron; ::_thesis: alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>
set d = dim p;
set aspcs = alternating-semi-proper-f-vector p;
set apcs = alternating-proper-f-vector p;
set r = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>;
A1: len (alternating-semi-proper-f-vector p) = (dim p) + 1 by Def28;
A2: for n being Nat st 1 <= n & n <= len (alternating-semi-proper-f-vector p) holds
(alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len (alternating-semi-proper-f-vector p) implies (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n )
assume that
A3: 1 <= n and
A4: n <= len (alternating-semi-proper-f-vector p) ; ::_thesis: (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
percases ( n <= dim p or n = (dim p) + 1 ) by A1, A4, NAT_1:8;
supposeA5: n <= dim p ; ::_thesis: (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
A6: n in NAT by ORDINAL1:def_12;
( len (alternating-proper-f-vector p) = dim p & dom (alternating-proper-f-vector p) = Seg (len (alternating-proper-f-vector p)) ) by Def27, FINSEQ_1:def_3;
then n in dom (alternating-proper-f-vector p) by A3, A5, A6;
then ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n = (alternating-proper-f-vector p) . n by FINSEQ_1:def_7
.= ((- 1) |^ (n + 1)) * (num-polytopes (p,(n - 1))) by A3, A5, Def27 ;
hence (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n by A1, A3, A4, Def28; ::_thesis: verum
end;
supposeA7: n = (dim p) + 1 ; ::_thesis: (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n
then n = (len (alternating-proper-f-vector p)) + 1 by Def27;
then A8: ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n = (- 1) |^ (dim p) by FINSEQ_1:42
.= (- 1) |^ ((dim p) + 2) by Th14 ;
(alternating-semi-proper-f-vector p) . n = ((- 1) |^ (n + 1)) * (num-polytopes (p,(n - 1))) by A3, A7, Def28
.= ((- 1) |^ (n + 1)) * 1 by A7, Th31
.= (- 1) |^ (n + 1) ;
hence (alternating-semi-proper-f-vector p) . n = ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) . n by A7, A8; ::_thesis: verum
end;
end;
end;
len ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) = (len (alternating-proper-f-vector p)) + (len <*((- 1) |^ (dim p))*>) by FINSEQ_1:22
.= (dim p) + (len <*((- 1) |^ (dim p))*>) by Def27
.= (dim p) + 1 by FINSEQ_1:40 ;
then len (alternating-semi-proper-f-vector p) = len ((alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*>) by Def28;
hence alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*> by A2, FINSEQ_1:14; ::_thesis: verum
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
set aspcs = alternating-semi-proper-f-vector p;
set apcs = alternating-proper-f-vector p;
alternating-semi-proper-f-vector p = (alternating-proper-f-vector p) ^ <*((- 1) |^ (dim p))*> by Th52;
then A1: Sum (alternating-semi-proper-f-vector p) = (Sum (alternating-proper-f-vector p)) + ((- 1) |^ (dim p)) by RVSUM_1:74;
A2: ( Sum (alternating-semi-proper-f-vector p) = 1 implies p is eulerian )
proof
assume Sum (alternating-semi-proper-f-vector p) = 1 ; ::_thesis: p is eulerian
then Sum (alternating-proper-f-vector p) = 1 + ((- 1) * ((- 1) |^ (dim p))) by A1
.= 1 + ((- 1) |^ ((dim p) + 1)) by NEWTON:6 ;
hence p is eulerian by Def29; ::_thesis: verum
end;
( p is eulerian implies Sum (alternating-semi-proper-f-vector p) = 1 )
proof
assume p is eulerian ; ::_thesis: Sum (alternating-semi-proper-f-vector p) = 1
then Sum (alternating-semi-proper-f-vector p) = (1 + ((- 1) |^ ((dim p) + 1))) + ((- 1) |^ (dim p)) by A1, Def29
.= (1 + ((- 1) * ((- 1) |^ (dim p)))) + ((- 1) |^ (dim p)) by NEWTON:6
.= 1 ;
hence Sum (alternating-semi-proper-f-vector p) = 1 ; ::_thesis: verum
end;
hence ( p is eulerian iff Sum (alternating-semi-proper-f-vector p) = 1 ) by A2; ::_thesis: verum
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 Th53: :: POLYFORM:53
for p being polyhedron holds alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p)
proof
let p be polyhedron; ::_thesis: alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p)
set acs = alternating-f-vector p;
set aspcs = alternating-semi-proper-f-vector p;
set d = dim p;
set r = <*(- 1)*> ^ (alternating-semi-proper-f-vector p);
A1: len (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) = (len <*(- 1)*>) + (len (alternating-semi-proper-f-vector p)) by FINSEQ_1:22
.= (len <*(- 1)*>) + ((dim p) + 1) by Def28
.= 1 + ((dim p) + 1) by FINSEQ_1:40
.= (dim p) + 2 ;
A2: for n being Nat st 1 <= n & n <= len (alternating-f-vector p) holds
(alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len (alternating-f-vector p) implies (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n )
assume that
A3: 1 <= n and
A4: n <= len (alternating-f-vector p) ; ::_thesis: (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n
A5: n <= (dim p) + 2 by A4, Def26;
percases ( n = 1 or n > 1 ) by A3, XXREAL_0:1;
supposeA6: n = 1 ; ::_thesis: (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n
then (alternating-f-vector p) . n = ((- 1) |^ 1) * (num-polytopes (p,(1 - 2))) by A5, Def26
.= (- 1) * (num-polytopes (p,(- 1))) by NEWTON:5
.= (- 1) * 1 by Th30
.= - 1 ;
hence (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n by A6, FINSEQ_1:41; ::_thesis: verum
end;
supposeA7: n > 1 ; ::_thesis: (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n
then A8: 1 - 1 < n - 1 by XREAL_1:9;
then reconsider m = n - 1 as Element of NAT by INT_1:3;
n - 1 <= ((dim p) + 2) - 1 by A5, XREAL_1:9;
then A9: m <= (dim p) + 1 ;
len <*(- 1)*> = 1 by FINSEQ_1:39;
then A10: (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n = (alternating-semi-proper-f-vector p) . (n - 1) by A1, A5, A7, FINSEQ_1:24;
0 < 0 + m by A8;
then 1 <= m by NAT_1:19;
then (alternating-semi-proper-f-vector p) . m = ((- 1) |^ (m + 1)) * (num-polytopes (p,(m - 1))) by A9, Def28
.= ((- 1) |^ n) * (num-polytopes (p,(n - 2))) ;
hence (alternating-f-vector p) . n = (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) . n by A3, A5, A10, Def26; ::_thesis: verum
end;
end;
end;
len (alternating-f-vector p) = len (<*(- 1)*> ^ (alternating-semi-proper-f-vector p)) by A1, Def26;
hence alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p) by A2, FINSEQ_1:14; ::_thesis: verum
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
set aspcs = alternating-semi-proper-f-vector p;
set acs = alternating-f-vector p;
alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p) by Th53;
then A1: Sum (alternating-f-vector p) = (- 1) + (Sum (alternating-semi-proper-f-vector p)) by Th20;
( p is eulerian implies Sum (alternating-f-vector p) = 0 )
proof
assume p is eulerian ; ::_thesis: Sum (alternating-f-vector p) = 0
then Sum (alternating-f-vector p) = (- 1) + 1 by A1, Def30
.= 0 ;
hence Sum (alternating-f-vector p) = 0 ; ::_thesis: verum
end;
hence ( p is eulerian iff Sum (alternating-f-vector p) = 0 ) by A1, Def30; ::_thesis: verum
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 Th54: :: POLYFORM:54
for p being polyhedron holds not 0 -polytopes p is empty
proof
let p be polyhedron; ::_thesis: not 0 -polytopes p is empty
set d = dim p;
percases ( dim p = 0 or dim p > 0 ) ;
suppose dim p = 0 ; ::_thesis: not 0 -polytopes p is empty
then 0 -polytopes p = {p} by Def5;
hence not 0 -polytopes p is empty ; ::_thesis: verum
end;
suppose dim p > 0 ; ::_thesis: not 0 -polytopes p is empty
hence not 0 -polytopes p is empty by Th25; ::_thesis: verum
end;
end;
end;
theorem Th55: :: POLYFORM:55
for p being polyhedron holds card ([#] ((- 1) -chain-space p)) = 2
proof
let p be polyhedron; ::_thesis: card ([#] ((- 1) -chain-space p)) = 2
(- 1) -polytopes p = {{}} by Def5;
then card ((- 1) -polytopes p) = 1 by CARD_1:30;
then card ([#] ((- 1) -chain-space p)) = exp (2,1) by BSPACE:42
.= 2 by CARD_2:27 ;
hence card ([#] ((- 1) -chain-space p)) = 2 ; ::_thesis: verum
end;
theorem Th56: :: POLYFORM:56
for p being polyhedron holds [#] ((- 1) -chain-space p) = {{},{{}}}
proof
let p be polyhedron; ::_thesis: [#] ((- 1) -chain-space p) = {{},{{}}}
(- 1) -polytopes p = {{}} by Def5;
hence [#] ((- 1) -chain-space p) = {{},{{}}} by ZFMISC_1:24; ::_thesis: verum
end;
theorem Th57: :: 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
proof
let p be polyhedron; ::_thesis: 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
let k be Integer; ::_thesis: 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
let x be Element of k -polytopes p; ::_thesis: for e being Element of (k - 1) -polytopes p st k = 0 & e = {} holds
incidence-value (e,x) = 1. Z_2
let e be Element of (k - 1) -polytopes p; ::_thesis: ( k = 0 & e = {} implies incidence-value (e,x) = 1. Z_2 )
assume that
A1: k = 0 and
A2: e = {} ; ::_thesis: incidence-value (e,x) = 1. Z_2
A3: eta (p,k) = [:{{}},(0 -polytopes p):] --> (1. Z_2) by A1, Def6;
A4: k <= dim p by A1;
then ( {} in {{}} & not 0 -polytopes p is empty ) by Th25, TARSKI:def_1;
then A5: [{},x] in [:{{}},(0 -polytopes p):] by A1, ZFMISC_1:87;
incidence-value (e,x) = (eta (p,k)) . (e,x) by A1, A4, Def13
.= 1. Z_2 by A2, A3, A5, FUNCOP_1:7 ;
hence incidence-value (e,x) = 1. Z_2 ; ::_thesis: verum
end;
theorem Th58: :: 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
proof
let p be polyhedron; ::_thesis: 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
let k be Integer; ::_thesis: 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
let x be Element of k -polytopes p; ::_thesis: 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
let v be Element of (k -chain-space p); ::_thesis: 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
let e be Element of (k - 1) -polytopes p; ::_thesis: 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
let n be Nat; ::_thesis: ( k = 0 & v = {x} & e = {} & x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) implies (incidence-sequence (e,v)) . n = 1. Z_2 )
assume that
A1: k = 0 and
A2: v = {x} and
A3: e = {} and
A4: ( x = n -th-polytope (p,k) & 1 <= n & n <= num-polytopes (p,k) ) ; ::_thesis: (incidence-sequence (e,v)) . n = 1. Z_2
set iseq = incidence-sequence (e,v);
A5: x in v by A2, TARSKI:def_1;
not (k - 1) -polytopes p is empty by A1, Def5;
then (incidence-sequence (e,v)) . n = (v @ x) * (incidence-value (e,x)) by A4, Def16
.= (1. Z_2) * (incidence-value (e,x)) by A5, BSPACE:def_3
.= (1. Z_2) * (1. Z_2) by A1, A3, Th57
.= 1. Z_2 by VECTSP_1:def_6 ;
hence (incidence-sequence (e,v)) . n = 1. Z_2 ; ::_thesis: verum
end;
theorem Th59: :: 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
proof
let p be polyhedron; ::_thesis: 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
let k be Integer; ::_thesis: 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
let x be Element of k -polytopes p; ::_thesis: 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
let e be Element of (k - 1) -polytopes p; ::_thesis: 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
let v be Element of (k -chain-space p); ::_thesis: 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
let m, n be Nat; ::_thesis: ( 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 implies (incidence-sequence (e,v)) . m = 0. Z_2 )
assume that
A1: k = 0 and
A2: v = {x} and
A3: x = n -th-polytope (p,k) and
A4: ( 1 <= m & m <= num-polytopes (p,k) ) and
A5: ( 1 <= n & n <= num-polytopes (p,k) & m <> n ) ; ::_thesis: (incidence-sequence (e,v)) . m = 0. Z_2
A6: m -th-polytope (p,k) <> x by A3, A4, A5, Th34;
now__::_thesis:_not_v_@_(m_-th-polytope_(p,k))_=_1._Z_2
assume v @ (m -th-polytope (p,k)) = 1. Z_2 ; ::_thesis: contradiction
then m -th-polytope (p,k) in {x} by A2, BSPACE:9;
hence contradiction by A6, TARSKI:def_1; ::_thesis: verum
end;
then A7: v @ (m -th-polytope (p,k)) = 0. Z_2 by BSPACE:11;
set iseq = incidence-sequence (e,v);
not (k - 1) -polytopes p is empty by A1, Def5;
then (incidence-sequence (e,v)) . m = (0. Z_2) * (incidence-value (e,(m -th-polytope (p,k)))) by A4, A7, Def16
.= 0. Z_2 by VECTSP_1:7 ;
hence (incidence-sequence (e,v)) . m = 0. Z_2 ; ::_thesis: verum
end;
theorem Th60: :: 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
proof
let p be polyhedron; ::_thesis: 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
let k be Integer; ::_thesis: 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
let x be Element of k -polytopes p; ::_thesis: 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
let v be Element of (k -chain-space p); ::_thesis: for e being Element of (k - 1) -polytopes p st k = 0 & v = {x} & e = {} holds
Sum (incidence-sequence (e,v)) = 1. Z_2
let e be Element of (k - 1) -polytopes p; ::_thesis: ( k = 0 & v = {x} & e = {} implies Sum (incidence-sequence (e,v)) = 1. Z_2 )
assume that
A1: k = 0 and
A2: v = {x} and
A3: e = {} ; ::_thesis: Sum (incidence-sequence (e,v)) = 1. Z_2
set iseq = incidence-sequence (e,v);
k <= dim p by A1;
then consider n being Nat such that
A4: x = n -th-polytope (p,k) and
A5: ( 1 <= n & n <= num-polytopes (p,k) ) by A1, Th32;
not (k - 1) -polytopes p is empty by A1, Def5;
then A6: len (incidence-sequence (e,v)) = num-polytopes (p,k) by Def16;
A7: for m being Nat st m in dom (incidence-sequence (e,v)) & m <> n holds
(incidence-sequence (e,v)) . m = 0. Z_2
proof
let m be Nat; ::_thesis: ( m in dom (incidence-sequence (e,v)) & m <> n implies (incidence-sequence (e,v)) . m = 0. Z_2 )
assume that
A8: m in dom (incidence-sequence (e,v)) and
A9: m <> n ; ::_thesis: (incidence-sequence (e,v)) . m = 0. Z_2
m in Seg (len (incidence-sequence (e,v))) by A8, FINSEQ_1:def_3;
then ( 1 <= m & m <= len (incidence-sequence (e,v)) ) by FINSEQ_1:1;
hence (incidence-sequence (e,v)) . m = 0. Z_2 by A1, A2, A4, A5, A6, A9, Th59; ::_thesis: verum
end;
dom (incidence-sequence (e,v)) = Seg (len (incidence-sequence (e,v))) by FINSEQ_1:def_3;
then A10: n in dom (incidence-sequence (e,v)) by A5, A6, FINSEQ_1:1;
(incidence-sequence (e,v)) . n = 1. Z_2 by A1, A2, A3, A4, A5, Th58;
hence Sum (incidence-sequence (e,v)) = 1. Z_2 by A10, A7, MATRIX_3:12; ::_thesis: verum
end;
theorem Th61: :: POLYFORM:61
for p being polyhedron
for x being Element of 0 -polytopes p holds (0 -boundary p) . {x} = {{}}
proof
let p be polyhedron; ::_thesis: for x being Element of 0 -polytopes p holds (0 -boundary p) . {x} = {{}}
reconsider minusone = 0 - 1 as Integer ;
let x be Element of 0 -polytopes p; ::_thesis: (0 -boundary p) . {x} = {{}}
set T = 0 -boundary p;
not 0 -polytopes p is empty by Th54;
then reconsider v = {x} as Subset of (0 -polytopes p) by ZFMISC_1:31;
(0 - 1) -polytopes p = {{}} by Def5;
then reconsider null = {} as Element of (0 - 1) -polytopes p by TARSKI:def_1;
reconsider v = v as Element of (0 -chain-space p) ;
reconsider bv = Boundary v as Element of (minusone -chain-space p) ;
A1: bv c= {null}
proof
A2: [#] (minusone -chain-space p) = {{},{{}}} by Th56;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in bv or y in {null} )
assume A3: y in bv ; ::_thesis: y in {null}
percases ( bv = {} or bv = {{}} ) by A2, TARSKI:def_2;
suppose bv = {} ; ::_thesis: y in {null}
hence y in {null} by A3; ::_thesis: verum
end;
suppose bv = {{}} ; ::_thesis: y in {null}
hence y in {null} by A3; ::_thesis: verum
end;
end;
end;
not minusone -polytopes p is empty by Def5;
then ( null in bv iff Sum (incidence-sequence (null,v)) = 1. Z_2 ) by Def17;
then A4: {null} c= bv by Th60, ZFMISC_1:31;
(0 -boundary p) . v = Boundary v by Def18;
hence (0 -boundary p) . {x} = {{}} by A4, A1, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th62: :: POLYFORM:62
for p being polyhedron
for k being Integer st k = - 1 holds
dim (k -bounding-chain-space p) = 1
proof
let p be polyhedron; ::_thesis: for k being Integer st k = - 1 holds
dim (k -bounding-chain-space p) = 1
let k be Integer; ::_thesis: ( k = - 1 implies dim (k -bounding-chain-space p) = 1 )
set T = 0 -boundary p;
set V = k -bounding-chain-space p;
assume A1: k = - 1 ; ::_thesis: dim (k -bounding-chain-space p) = 1
card ([#] (k -bounding-chain-space p)) = 2
proof
[#] (k -bounding-chain-space p) c= [#] (k -chain-space p) by VECTSP_4:def_2;
then card ([#] (k -bounding-chain-space p)) c= card ([#] (k -chain-space p)) by CARD_1:11;
then A2: card ([#] (k -bounding-chain-space p)) c= 2 by A1, Th55;
0 -polytopes p <> {} by Th54;
then consider x being set such that
A3: x in 0 -polytopes p by XBOOLE_0:def_1;
reconsider x = x as Element of 0 -polytopes p by A3;
set v = {x};
A4: (0 -boundary p) . {x} = {{}} by Th61;
reconsider v = {x} as Subset of (0 -polytopes p) by A3, ZFMISC_1:31;
reconsider v = v as Element of (0 -chain-space p) ;
A5: dom (0 -boundary p) = [#] (0 -chain-space p) by RANKNULL:7;
then v in dom (0 -boundary p) ;
then A6: {{}} in rng (0 -boundary p) by A4, FUNCT_1:3;
(0 -boundary p) . (0. (0 -chain-space p)) = 0. (k -chain-space p) by A1, RANKNULL:9
.= {} ;
then {} in rng (0 -boundary p) by A5, FUNCT_1:3;
then A7: {{},{{}}} c= rng (0 -boundary p) by A6, ZFMISC_1:32;
card {{},{{}}} = 2 by CARD_2:57;
then A8: 2 c= card (rng (0 -boundary p)) by A7, CARD_1:11;
card (rng (0 -boundary p)) = card ((0 -boundary p) .: ([#] (0 -chain-space p))) by RELSET_1:22
.= card ([#] (k -bounding-chain-space p)) by A1, RANKNULL:def_2 ;
hence card ([#] (k -bounding-chain-space p)) = 2 by A8, A2, XBOOLE_0:def_10; ::_thesis: verum
end;
hence dim (k -bounding-chain-space p) = 1 by RANKNULL:6; ::_thesis: verum
end;
theorem Th63: :: POLYFORM:63
for p being polyhedron holds card ([#] ((dim p) -chain-space p)) = 2
proof
let p be polyhedron; ::_thesis: card ([#] ((dim p) -chain-space p)) = 2
(dim p) -polytopes p = {p} by Def5;
then card ((dim p) -polytopes p) = 1 by CARD_1:30;
then card ([#] ((dim p) -chain-space p)) = exp (2,1) by BSPACE:42
.= 2 by CARD_2:27 ;
hence card ([#] ((dim p) -chain-space p)) = 2 ; ::_thesis: verum
end;
theorem Th64: :: POLYFORM:64
for p being polyhedron holds {p} is Element of ((dim p) -chain-space p)
proof
let p be polyhedron; ::_thesis: {p} is Element of ((dim p) -chain-space p)
(dim p) -polytopes p = {p} by Def5;
hence {p} is Element of ((dim p) -chain-space p) by ZFMISC_1:def_1; ::_thesis: verum
end;
theorem Th65: :: POLYFORM:65
for p being polyhedron holds {p} in [#] ((dim p) -chain-space p)
proof
let p be polyhedron; ::_thesis: {p} in [#] ((dim p) -chain-space p)
{p} is Element of ((dim p) -chain-space p) by Th64;
hence {p} in [#] ((dim p) -chain-space p) ; ::_thesis: verum
end;
theorem Th66: :: POLYFORM:66
for p being polyhedron holds not ((dim p) - 1) -polytopes p is empty
proof
let p be polyhedron; ::_thesis: not ((dim p) - 1) -polytopes p is empty
set n = (dim p) - 1;
0 - 1 = - 1 ;
then A1: - 1 <= (dim p) - 1 by XREAL_1:9;
(dim p) - 1 <= dim p by XREAL_1:146;
hence not ((dim p) - 1) -polytopes p is empty by A1, Th25; ::_thesis: verum
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 Th66;
end;
theorem Th67: :: POLYFORM:67
for p being polyhedron holds [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}}
proof
let p be polyhedron; ::_thesis: [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}}
set V = (dim p) -chain-space p;
set C = [#] ((dim p) -chain-space p);
A1: card ([#] ((dim p) -chain-space p)) = 2 by Th63;
reconsider C = [#] ((dim p) -chain-space p) as finite set ;
A2: {p} in C by Th65;
ex a, b being set st
( a <> b & C = {a,b} ) by A1, CARD_2:60;
hence [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}} by A2, Th1; ::_thesis: verum
end;
theorem Th68: :: 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} )
proof
let p be polyhedron; ::_thesis: for x being Element of ((dim p) -chain-space p) holds
( x = 0. ((dim p) -chain-space p) or x = {p} )
set V = (dim p) -chain-space p;
let x be Element of ((dim p) -chain-space p); ::_thesis: ( x = 0. ((dim p) -chain-space p) or x = {p} )
x in [#] ((dim p) -chain-space p) ;
then x in {(0. ((dim p) -chain-space p)),{p}} by Th67;
hence ( x = 0. ((dim p) -chain-space p) or x = {p} ) by TARSKI:def_2; ::_thesis: verum
end;
theorem Th69: :: 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) )
proof
let p be polyhedron; ::_thesis: 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) )
set V = (dim p) -chain-space p;
let x, y be Element of ((dim p) -chain-space p); ::_thesis: ( not x <> y or x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )
assume A1: x <> y ; ::_thesis: ( x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )
assume x <> 0. ((dim p) -chain-space p) ; ::_thesis: y = 0. ((dim p) -chain-space p)
then A2: x = {p} by Th68;
assume y <> 0. ((dim p) -chain-space p) ; ::_thesis: contradiction
hence contradiction by A1, A2, Th68; ::_thesis: verum
end;
theorem :: POLYFORM:70
for p being polyhedron holds (dim p) -polytope-seq p = <*p*> by Def7;
theorem Th71: :: POLYFORM:71
for p being polyhedron holds 1 -th-polytope (p,(dim p)) = p
proof
let p be polyhedron; ::_thesis: 1 -th-polytope (p,(dim p)) = p
reconsider egy = 1 as Nat ;
set s = (dim p) -polytope-seq p;
A1: (dim p) -polytope-seq p = <*p*> by Def7;
egy <= num-polytopes (p,(dim p)) by Th31;
then egy -th-polytope (p,(dim p)) = ((dim p) -polytope-seq p) . egy by Def12
.= p by A1, FINSEQ_1:40 ;
hence 1 -th-polytope (p,(dim p)) = p ; ::_thesis: verum
end;
theorem Th72: :: 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
proof
let p be polyhedron; ::_thesis: 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
A1: (dim p) -polytopes p = {p} by Def5;
let c be Element of ((dim p) -chain-space p); ::_thesis: for x being Element of (dim p) -polytopes p st c = {p} holds
c @ x = 1. Z_2
let x be Element of (dim p) -polytopes p; ::_thesis: ( c = {p} implies c @ x = 1. Z_2 )
assume c = {p} ; ::_thesis: c @ x = 1. Z_2
hence c @ x = 1. Z_2 by A1, BSPACE:def_3; ::_thesis: verum
end;
theorem Th73: :: 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
proof
let p be polyhedron; ::_thesis: 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
set f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2);
let x be Element of ((dim p) - 1) -polytopes p; ::_thesis: for c being Element of (dim p) -polytopes p st c = p holds
incidence-value (x,c) = 1. Z_2
let c be Element of (dim p) -polytopes p; ::_thesis: ( c = p implies incidence-value (x,c) = 1. Z_2 )
assume c = p ; ::_thesis: incidence-value (x,c) = 1. Z_2
then ( dom ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) = [:(((dim p) - 1) -polytopes p),{p}:] & c in {p} ) by FUNCOP_1:13, TARSKI:def_1;
then [x,c] in dom ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) by ZFMISC_1:87;
then ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) . (x,c) in rng ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) by FUNCT_1:3;
then ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) . (x,c) in {(1. Z_2)} by FUNCOP_1:8;
then A1: ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) . (x,c) = 1. Z_2 by TARSKI:def_1;
eta (p,(dim p)) = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2) by Def6;
hence incidence-value (x,c) = 1. Z_2 by A1, Def13; ::_thesis: verum
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) -chain-space p) st c = {p} holds
incidence-sequence (x,c) = <*(1. Z_2)*>
proof
let p be polyhedron; ::_thesis: 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)*>
let x be Element of ((dim p) - 1) -polytopes p; ::_thesis: for c being Element of ((dim p) -chain-space p) st c = {p} holds
incidence-sequence (x,c) = <*(1. Z_2)*>
let c be Element of ((dim p) -chain-space p); ::_thesis: ( c = {p} implies incidence-sequence (x,c) = <*(1. Z_2)*> )
assume A1: c = {p} ; ::_thesis: incidence-sequence (x,c) = <*(1. Z_2)*>
set iseq = incidence-sequence (x,c);
A2: (incidence-sequence (x,c)) . 1 = 1. Z_2
proof
reconsider egy = 1 as Nat ;
set z = egy -th-polytope (p,(dim p));
egy <= num-polytopes (p,(dim p)) by Th31;
then A3: (incidence-sequence (x,c)) . egy = (c @ (egy -th-polytope (p,(dim p)))) * (incidence-value (x,(egy -th-polytope (p,(dim p))))) by Def16;
( c @ (egy -th-polytope (p,(dim p))) = 1. Z_2 & incidence-value (x,(egy -th-polytope (p,(dim p)))) = 1. Z_2 ) by A1, Th71, Th72, Th73;
hence (incidence-sequence (x,c)) . 1 = 1. Z_2 by A3, VECTSP_1:def_6; ::_thesis: verum
end;
num-polytopes (p,(dim p)) = 1 by Th31;
then len (incidence-sequence (x,c)) = 1 by Def16;
hence incidence-sequence (x,c) = <*(1. Z_2)*> by A2, FINSEQ_1:40; ::_thesis: verum
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
Sum (incidence-sequence (x,c)) = 1. Z_2
proof
let p be polyhedron; ::_thesis: 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
let x be Element of ((dim p) - 1) -polytopes p; ::_thesis: for c being Element of ((dim p) -chain-space p) st c = {p} holds
Sum (incidence-sequence (x,c)) = 1. Z_2
let c be Element of ((dim p) -chain-space p); ::_thesis: ( c = {p} implies Sum (incidence-sequence (x,c)) = 1. Z_2 )
assume c = {p} ; ::_thesis: Sum (incidence-sequence (x,c)) = 1. Z_2
then incidence-sequence (x,c) = <*(1. Z_2)*> by Th74;
hence Sum (incidence-sequence (x,c)) = 1. Z_2 by FINSOP_1:11; ::_thesis: verum
end;
theorem Th76: :: POLYFORM:76
for p being polyhedron holds ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p
proof
let p be polyhedron; ::_thesis: ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p
reconsider c = {p} as Element of ((dim p) -chain-space p) by Th64;
set T = (dim p) -boundary p;
set X = ((dim p) - 1) -polytopes p;
reconsider d = ((dim p) - 1) -polytopes p as Element of (((dim p) - 1) -chain-space p) by ZFMISC_1:def_1;
reconsider Tc = ((dim p) -boundary p) . c as Element of (((dim p) - 1) -chain-space p) ;
for x being Element of ((dim p) - 1) -polytopes p holds
( x in Tc iff x in d )
proof
let x be Element of ((dim p) - 1) -polytopes p; ::_thesis: ( x in Tc iff x in d )
thus ( x in Tc implies x in d ) ; ::_thesis: ( x in d implies x in Tc )
thus ( x in d implies x in Tc ) ::_thesis: verum
proof
assume x in d ; ::_thesis: x in Tc
Sum (incidence-sequence (x,c)) = 1. Z_2 by Th75;
then x in Boundary c by Def17;
hence x in Tc by Def18; ::_thesis: verum
end;
end;
hence ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p by SUBSET_1:3; ::_thesis: verum
end;
theorem Th77: :: POLYFORM:77
for p being polyhedron holds (dim p) -boundary p is one-to-one
proof
let p be polyhedron; ::_thesis: (dim p) -boundary p is one-to-one
set T = (dim p) -boundary p;
set U = ((dim p) - 1) -chain-space p;
set V = (dim p) -chain-space p;
set B = {p};
assume not (dim p) -boundary p is one-to-one ; ::_thesis: contradiction
then consider x1, x2 being set such that
A1: x1 in dom ((dim p) -boundary p) and
A2: x2 in dom ((dim p) -boundary p) and
A3: ((dim p) -boundary p) . x1 = ((dim p) -boundary p) . x2 and
A4: x1 <> x2 by FUNCT_1:def_4;
reconsider x2 = x2 as Element of ((dim p) -chain-space p) by A2;
reconsider x1 = x1 as Element of ((dim p) -chain-space p) by A1;
percases ( x1 = 0. ((dim p) -chain-space p) or x2 = 0. ((dim p) -chain-space p) ) by A4, Th69;
suppose x1 = 0. ((dim p) -chain-space p) ; ::_thesis: contradiction
then ( x2 = {p} & ((dim p) -boundary p) . x1 = 0. (((dim p) - 1) -chain-space p) ) by A4, Th68, RANKNULL:9;
hence contradiction by A3, Th76; ::_thesis: verum
end;
suppose x2 = 0. ((dim p) -chain-space p) ; ::_thesis: contradiction
then ( x1 = {p} & ((dim p) -boundary p) . x2 = 0. (((dim p) - 1) -chain-space p) ) by A4, Th68, RANKNULL:9;
hence contradiction by A3, Th76; ::_thesis: verum
end;
end;
end;
theorem Th78: :: POLYFORM:78
for p being polyhedron holds dim (((dim p) - 1) -bounding-chain-space p) = 1
proof
let p be polyhedron; ::_thesis: dim (((dim p) - 1) -bounding-chain-space p) = 1
set d = dim p;
set T = (dim p) -boundary p;
set U = (dim p) -chain-space p;
set V = ((dim p) - 1) -bounding-chain-space p;
A1: card ([#] (((dim p) - 1) -bounding-chain-space p)) = card (((dim p) -boundary p) .: ([#] ((dim p) -chain-space p))) by RANKNULL:def_2
.= card (rng ((dim p) -boundary p)) by RELSET_1:22 ;
A2: card (dom ((dim p) -boundary p)) = card ([#] ((dim p) -chain-space p)) by RANKNULL:7
.= 2 by Th63 ;
(dim p) -boundary p is one-to-one by Th77;
then card ([#] (((dim p) - 1) -bounding-chain-space p)) = 2 by A1, A2, CARD_1:70;
hence dim (((dim p) - 1) -bounding-chain-space p) = 1 by RANKNULL:6; ::_thesis: verum
end;
theorem Th79: :: POLYFORM:79
for p being polyhedron st p is simply-connected holds
dim (((dim p) - 1) -circuit-space p) = 1
proof
let p be polyhedron; ::_thesis: ( p is simply-connected implies dim (((dim p) - 1) -circuit-space p) = 1 )
set d = dim p;
set U = ((dim p) - 1) -bounding-chain-space p;
set V = ((dim p) - 1) -circuit-space p;
assume p is simply-connected ; ::_thesis: dim (((dim p) - 1) -circuit-space p) = 1
then ((dim p) - 1) -bounding-chain-space p = ((dim p) - 1) -circuit-space p by Th50;
hence dim (((dim p) - 1) -circuit-space p) = 1 by Th78; ::_thesis: verum
end;
theorem Th80: :: 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)
proof
let p be polyhedron; ::_thesis: for n being Nat st 1 < n & n < (dim p) + 2 holds
(alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)
let n be Nat; ::_thesis: ( 1 < n & n < (dim p) + 2 implies (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1) )
assume A1: 1 < n ; ::_thesis: ( not n < (dim p) + 2 or (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1) )
1 - 1 = 0 ;
then reconsider m = n - 1 as Element of NAT by A1, INT_1:3, XREAL_1:13;
reconsider m = m as Nat ;
set apcs = alternating-proper-f-vector p;
set acs = alternating-f-vector p;
A2: 2 - 1 = 1 ;
1 + 1 = 2 ;
then 2 <= n by A1, INT_1:7;
then A3: 1 <= m by A2, XREAL_1:13;
assume A4: n < (dim p) + 2 ; ::_thesis: (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)
then n < ((dim p) + 1) + 1 ;
then n <= (dim p) + 1 by NAT_1:13;
then n - 1 <= ((dim p) + 1) - 1 by XREAL_1:9;
then A5: (alternating-proper-f-vector p) . m = ((- 1) |^ (m + 1)) * (num-polytopes (p,(m - 1))) by A3, Def27;
(alternating-f-vector p) . n = ((- 1) |^ n) * (num-polytopes (p,(n - 2))) by A1, A4, Def26;
hence (alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1) by A5; ::_thesis: verum
end;
theorem Th81: :: POLYFORM:81
for p being polyhedron holds alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>
proof
let p be polyhedron; ::_thesis: alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
set r = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>;
set n = dim p;
A1: len <*((- 1) |^ (dim p))*> = 1 by FINSEQ_1:39;
A2: len (alternating-proper-f-vector p) = dim p by Def27;
A3: len (alternating-f-vector p) = (dim p) + 2 by Def26;
A4: for k being Nat st 1 <= k & k <= len (alternating-f-vector p) holds
(alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k
proof
let k be Nat; ::_thesis: ( 1 <= k & k <= len (alternating-f-vector p) implies (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k )
assume A5: ( 1 <= k & k <= len (alternating-f-vector p) ) ; ::_thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k
percases ( k = 1 or k = (dim p) + 2 or ( 1 < k & k < (dim p) + 2 ) ) by A3, A5, XXREAL_0:1;
supposeA6: k = 1 ; ::_thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k
reconsider o = 1 as Nat ;
( 1 <= (dim p) + 2 & o - 2 = - 1 ) by Th12;
then A7: (alternating-f-vector p) . o = ((- 1) |^ o) * (num-polytopes (p,(- 1))) by Def26;
( (- 1) |^ 1 = - 1 & num-polytopes (p,(- 1)) = 1 ) by Th4, Th9, Th30;
hence (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A6, A7, Th17; ::_thesis: verum
end;
supposeA8: k = (dim p) + 2 ; ::_thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k
len <*(- 1)*> = 1 by FINSEQ_1:39;
then k = ((len <*(- 1)*>) + (len (alternating-proper-f-vector p))) + 1 by A2, A8;
then A9: ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k = (- 1) |^ (dim p) by Th18
.= (- 1) |^ k by A8, Th14 ;
1 <= k by A8, Th12;
then A10: (alternating-f-vector p) . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) by A8, Def26;
num-polytopes (p,(k - 2)) = 1 by A8, Th31;
hence (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A10, A9; ::_thesis: verum
end;
supposeA11: ( 1 < k & k < (dim p) + 2 ) ; ::_thesis: (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k
set m = k - 1;
A12: ( (k + 1) - 1 = k & ((dim p) + 2) - 1 = (dim p) + 1 ) ;
A13: k + 1 <= (dim p) + 2 by A11, INT_1:7;
len (<*(- 1)*> ^ (alternating-proper-f-vector p)) = (len <*(- 1)*>) + (len (alternating-proper-f-vector p)) by FINSEQ_1:22
.= (dim p) + 1 by A2, FINSEQ_1:39 ;
then ( len <*(- 1)*> = 1 & k <= len (<*(- 1)*> ^ (alternating-proper-f-vector p)) ) by A13, A12, FINSEQ_1:39, XREAL_1:9;
then ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k = (alternating-proper-f-vector p) . (k - 1) by A11, Th19;
hence (alternating-f-vector p) . k = ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) . k by A11, Th80; ::_thesis: verum
end;
end;
end;
( len ((<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*>) = ((len <*(- 1)*>) + (len (alternating-proper-f-vector p))) + (len <*((- 1) |^ (dim p))*>) & len <*(- 1)*> = 1 ) by Th16, FINSEQ_1:39;
hence alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*> by A3, A2, A1, A4, FINSEQ_1:14; ::_thesis: verum
end;
begin
theorem Th82: :: POLYFORM:82
for p being polyhedron st dim p is odd holds
Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2
proof
let p be polyhedron; ::_thesis: ( dim p is odd implies Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2 )
reconsider minusone = - 1 as Integer ;
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
reconsider lastterm = (- 1) |^ (dim p) as Integer ;
assume dim p is odd ; ::_thesis: Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2
then A1: (- 1) |^ (dim p) = - 1 by Th9;
alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*> by Th81;
then Sum (alternating-f-vector p) = ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + (Sum <*lastterm*>) by Th21
.= ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + (- 1) by A1, RVSUM_1:73
.= ((- 1) + (Sum (alternating-proper-f-vector p))) + (- 1) by RVSUM_1:73
.= (Sum (alternating-proper-f-vector p)) - 2 ;
hence Sum (alternating-f-vector p) = (Sum (alternating-proper-f-vector p)) - 2 ; ::_thesis: verum
end;
theorem Th83: :: POLYFORM:83
for p being polyhedron st dim p is even holds
Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p)
proof
let p be polyhedron; ::_thesis: ( dim p is even implies Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p) )
reconsider minusone = - 1 as Integer ;
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
reconsider lastterm = (- 1) |^ (dim p) as Integer ;
assume dim p is even ; ::_thesis: Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p)
then A1: (- 1) |^ (dim p) = 1 by Th8;
alternating-f-vector p = (<*(- 1)*> ^ (alternating-proper-f-vector p)) ^ <*((- 1) |^ (dim p))*> by Th81;
then Sum (alternating-f-vector p) = ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + (Sum <*lastterm*>) by Th21
.= ((Sum <*minusone*>) + (Sum (alternating-proper-f-vector p))) + 1 by A1, RVSUM_1:73
.= ((- 1) + (Sum (alternating-proper-f-vector p))) + 1 by RVSUM_1:73
.= Sum (alternating-proper-f-vector p) ;
hence Sum (alternating-f-vector p) = Sum (alternating-proper-f-vector p) ; ::_thesis: verum
end;
theorem Th84: :: POLYFORM:84
for p being polyhedron st dim p = 1 holds
Sum (alternating-proper-f-vector p) = num-polytopes (p,0)
proof
let p be polyhedron; ::_thesis: ( dim p = 1 implies Sum (alternating-proper-f-vector p) = num-polytopes (p,0) )
reconsider egy = 1 as Nat ;
set apcs = alternating-proper-f-vector p;
assume dim p = 1 ; ::_thesis: Sum (alternating-proper-f-vector p) = num-polytopes (p,0)
then A1: ( len (alternating-proper-f-vector p) = 1 & (alternating-proper-f-vector p) . egy = ((- 1) |^ (egy + 1)) * (num-polytopes (p,(egy - 1))) ) by Def27;
(- 1) |^ (egy + 1) = 1 by Th5, Th8;
then alternating-proper-f-vector p = <*(num-polytopes (p,0))*> by A1, FINSEQ_1:40;
hence Sum (alternating-proper-f-vector p) = num-polytopes (p,0) by RVSUM_1:73; ::_thesis: verum
end;
theorem Th85: :: 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))
proof
let p be polyhedron; ::_thesis: ( dim p = 2 implies Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1)) )
reconsider t = 2 as Nat ;
reconsider o = 1 as Nat ;
set apcs = alternating-proper-f-vector p;
reconsider apcso = (alternating-proper-f-vector p) . o as Integer ;
reconsider apcst = (alternating-proper-f-vector p) . t as Integer ;
assume A1: dim p = 2 ; ::_thesis: Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1))
then A2: ( (alternating-proper-f-vector p) . o = ((- 1) |^ (o + 1)) * (num-polytopes (p,(o - 1))) & (alternating-proper-f-vector p) . t = ((- 1) |^ (t + 1)) * (num-polytopes (p,(t - 1))) ) by Def27;
A3: ( (- 1) |^ (o + 1) = 1 & (- 1) |^ (t + 1) = - 1 ) by Th5, Th8, Th9;
len (alternating-proper-f-vector p) = 2 by A1, Def27;
then alternating-proper-f-vector p = <*apcso,apcst*> by FINSEQ_1:44;
then Sum (alternating-proper-f-vector p) = apcso + apcst by RVSUM_1:77
.= (num-polytopes (p,0)) - (num-polytopes (p,1)) by A2, A3 ;
hence Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1)) ; ::_thesis: verum
end;
theorem Th86: :: 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))
proof
let p be polyhedron; ::_thesis: ( dim p = 3 implies Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) )
reconsider mo = - 1 as Integer ;
reconsider th = 3 as Nat ;
reconsider tw = 2 as Nat ;
reconsider o = 1 as Nat ;
assume A1: dim p = 3 ; ::_thesis: Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2))
set apcs = alternating-proper-f-vector p;
(- 1) |^ (tw + 1) = - 1 by Th6, Th9;
then A2: (alternating-proper-f-vector p) . tw = mo * (num-polytopes (p,(tw - 1))) by A1, Def27;
(- 1) |^ (th + 1) = 1 by Th7, Th8;
then A3: (alternating-proper-f-vector p) . th = o * (num-polytopes (p,(th - 1))) by A1, Def27;
reconsider apcsth = (alternating-proper-f-vector p) . th as Integer ;
reconsider apcstw = (alternating-proper-f-vector p) . tw as Integer ;
reconsider apcson = (alternating-proper-f-vector p) . o as Integer ;
(- 1) |^ (o + 1) = 1 by Th5, Th8;
then A4: (alternating-proper-f-vector p) . o = o * (num-polytopes (p,(o - 1))) by A1, Def27;
len (alternating-proper-f-vector p) = 3 by A1, Def27;
then alternating-proper-f-vector p = <*apcson,apcstw,apcsth*> by FINSEQ_1:45;
then Sum (alternating-proper-f-vector p) = (apcson + apcstw) + apcsth by RVSUM_1:78
.= ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) by A4, A2, A3 ;
hence Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) ; ::_thesis: verum
end;
theorem Th87: :: POLYFORM:87
for p being polyhedron st dim p = 0 holds
p is eulerian
proof
let p be polyhedron; ::_thesis: ( dim p = 0 implies p is eulerian )
set d = dim p;
set apcs = alternating-proper-f-vector p;
assume A1: dim p = 0 ; ::_thesis: p is eulerian
then (- 1) |^ ((dim p) + 1) = - 1 by NEWTON:5;
then A2: 1 + ((- 1) |^ ((dim p) + 1)) = 0 ;
len (alternating-proper-f-vector p) = 0 by A1, Def27;
then alternating-proper-f-vector p = <*> INT ;
hence p is eulerian by A2, Def29, GR_CY_1:3; ::_thesis: verum
end;
theorem Th88: :: POLYFORM:88
for p being polyhedron st p is simply-connected holds
p is eulerian
proof
let p be polyhedron; ::_thesis: ( p is simply-connected implies p is eulerian )
assume A1: p is simply-connected ; ::_thesis: p is eulerian
set apcs = alternating-proper-f-vector p;
percases ( dim p = 0 or dim p > 0 ) ;
suppose dim p = 0 ; ::_thesis: p is eulerian
hence p is eulerian by Th87; ::_thesis: verum
end;
supposeA2: dim p > 0 ; ::_thesis: p is eulerian
deffunc H1( Nat) -> Element of INT = ((- 1) |^ ($1 + 1)) * (dim (($1 - 1) -circuit-space p));
deffunc H2( Nat) -> Element of INT = ((- 1) |^ ($1 + 1)) * (dim (($1 - 2) -bounding-chain-space p));
consider a being FinSequence such that
A3: len a = len (alternating-proper-f-vector p) and
A4: for n being Nat st n in dom a holds
a . n = H2(n) from FINSEQ_1:sch_2();
A5: rng a c= INT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng a or y in INT )
assume y in rng a ; ::_thesis: y in INT
then consider x being set such that
A6: x in dom a and
A7: y = a . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A6;
a . x = ((- 1) |^ (x + 1)) * (dim ((x - 2) -bounding-chain-space p)) by A4, A6;
hence y in INT by A7; ::_thesis: verum
end;
consider b being FinSequence such that
A8: len b = len (alternating-proper-f-vector p) and
A9: for n being Nat st n in dom b holds
b . n = H1(n) from FINSEQ_1:sch_2();
rng b c= INT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng b or y in INT )
assume y in rng b ; ::_thesis: y in INT
then consider x being set such that
A10: x in dom b and
A11: y = b . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A10;
b . x = ((- 1) |^ (x + 1)) * (dim ((x - 1) -circuit-space p)) by A9, A10;
hence y in INT by A11; ::_thesis: verum
end;
then reconsider a = a, b = b as FinSequence of INT by A5, FINSEQ_1:def_4;
A12: len (alternating-proper-f-vector p) > 0 by A2, Def27;
A13: a . 1 = 1
proof
reconsider egy = 1 as Element of NAT ;
1 <= 0 + 1 ;
then egy <= len (alternating-proper-f-vector p) by A12, NAT_1:13;
then egy in dom a by A3, FINSEQ_3:25;
then a . egy = ((- 1) |^ (1 + 1)) * (dim ((egy - 2) -bounding-chain-space p)) by A4
.= 1 * (dim ((egy - 2) -bounding-chain-space p)) by Th5, Th8
.= 1 by Th62 ;
hence a . 1 = 1 ; ::_thesis: verum
end;
A14: for n being Nat st 1 <= n & n < len (alternating-proper-f-vector p) holds
b . n = - (a . (n + 1))
proof
let n be Nat; ::_thesis: ( 1 <= n & n < len (alternating-proper-f-vector p) implies b . n = - (a . (n + 1)) )
assume that
A15: 1 <= n and
A16: n < len (alternating-proper-f-vector p) ; ::_thesis: b . n = - (a . (n + 1))
A17: n in dom b by A8, A15, A16, FINSEQ_3:25;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
A18: b . n = ((- 1) |^ (n + 1)) * (dim ((n - 1) -circuit-space p)) by A9, A17;
A19: 1 <= n + 1 by NAT_1:11;
n + 1 <= len (alternating-proper-f-vector p) by A16, INT_1:7;
then n + 1 in dom a by A3, A19, FINSEQ_3:25;
then a . (n + 1) = H2(n + 1) by A4
.= (((- 1) |^ (n + 1)) * ((- 1) |^ 1)) * (dim ((n - 1) -bounding-chain-space p)) by NEWTON:8
.= (((- 1) |^ (n + 1)) * (- 1)) * (dim ((n - 1) -bounding-chain-space p)) by NEWTON:5
.= - (((- 1) |^ (n + 1)) * (dim ((n - 1) -bounding-chain-space p)))
.= - (b . n) by A1, A18, Th50 ;
hence b . n = - (a . (n + 1)) ; ::_thesis: verum
end;
A20: b . (len (alternating-proper-f-vector p)) = (- 1) |^ ((dim p) + 1)
proof
reconsider n = len (alternating-proper-f-vector p) as Element of NAT ;
A21: n = dim p by Def27;
0 + 1 = 1 ;
then 1 <= len (alternating-proper-f-vector p) by A12, NAT_1:13;
then n in dom b by A8, FINSEQ_3:25;
then b . n = H1(n) by A9
.= ((- 1) |^ (n + 1)) * 1 by A1, A21, Th79
.= (- 1) |^ (n + 1) ;
hence b . (len (alternating-proper-f-vector p)) = (- 1) |^ ((dim p) + 1) by Def27; ::_thesis: verum
end;
for n being Nat st 1 <= n & n <= len (alternating-proper-f-vector p) holds
(alternating-proper-f-vector p) . n = (a . n) + (b . n)
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len (alternating-proper-f-vector p) implies (alternating-proper-f-vector p) . n = (a . n) + (b . n) )
assume A22: ( 1 <= n & n <= len (alternating-proper-f-vector p) ) ; ::_thesis: (alternating-proper-f-vector p) . n = (a . n) + (b . n)
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
n9 in dom a by A3, A22, FINSEQ_3:25;
then A23: a . n9 = ((- 1) |^ (n9 + 1)) * (dim ((n9 - 2) -bounding-chain-space p)) by A4;
( (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))) & n9 in dom b ) by A8, A22, Th51, FINSEQ_3:25;
hence (alternating-proper-f-vector p) . n = (a . n) + (b . n) by A9, A23; ::_thesis: verum
end;
then Sum (alternating-proper-f-vector p) = (a . 1) + (b . (len (alternating-proper-f-vector p))) by A12, A3, A8, A14, Th15;
hence p is eulerian by A13, A20, Def29; ::_thesis: verum
end;
end;
end;
theorem :: POLYFORM:89
for p being polyhedron st p is simply-connected & dim p = 1 holds
num-vertices p = 2
proof
let p be polyhedron; ::_thesis: ( p is simply-connected & dim p = 1 implies num-vertices p = 2 )
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
assume p is simply-connected ; ::_thesis: ( not dim p = 1 or num-vertices p = 2 )
then A1: p is eulerian by Th88;
assume A2: dim p = 1 ; ::_thesis: num-vertices p = 2
0 = Sum (alternating-f-vector p) by A1, Def31
.= (Sum (alternating-proper-f-vector p)) - 2 by A2, Th4, Th82
.= (num-polytopes (p,0)) - 2 by A2, Th84 ;
hence num-vertices p = 2 ; ::_thesis: verum
end;
theorem :: POLYFORM:90
for p being polyhedron st p is simply-connected & dim p = 2 holds
num-vertices p = num-edges p
proof
let p be polyhedron; ::_thesis: ( p is simply-connected & dim p = 2 implies num-vertices p = num-edges p )
set s = (num-polytopes (p,0)) - (num-polytopes (p,1));
set c = alternating-f-vector p;
assume p is simply-connected ; ::_thesis: ( not dim p = 2 or num-vertices p = num-edges p )
then A1: p is eulerian by Th88;
assume A2: dim p = 2 ; ::_thesis: num-vertices p = num-edges p
then A3: (num-polytopes (p,0)) - (num-polytopes (p,1)) = Sum (alternating-proper-f-vector p) by Th85;
0 = Sum (alternating-f-vector p) by A1, Def31
.= (num-polytopes (p,0)) - (num-polytopes (p,1)) by A2, A3, Th5, Th83 ;
hence num-vertices p = num-edges p ; ::_thesis: verum
end;
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
proof
let p be polyhedron; ::_thesis: ( p is simply-connected & dim p = 3 implies ((num-vertices p) - (num-edges p)) + (num-faces p) = 2 )
set s = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2));
set c = alternating-f-vector p;
assume p is simply-connected ; ::_thesis: ( not dim p = 3 or ((num-vertices p) - (num-edges p)) + (num-faces p) = 2 )
then A1: p is eulerian by Th88;
assume A2: dim p = 3 ; ::_thesis: ((num-vertices p) - (num-edges p)) + (num-faces p) = 2
then A3: ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2)) = Sum (alternating-proper-f-vector p) by Th86;
0 = Sum (alternating-f-vector p) by A1, Def31
.= (((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2))) - 2 by A2, A3, Th6, Th82 ;
hence ((num-vertices p) - (num-edges p)) + (num-faces p) = 2 ; ::_thesis: verum
end;