:: POLYFORM semantic presentation

theorem Th1: :: POLYFORM:1
for X, c, d being set st ex a, b being set st
( a <> b & X = {a,b} ) & c in X & d in X & c <> d holds
X = {c,d}
proof end;

theorem Th2: :: POLYFORM:2
for f being Function st f is one-to-one holds
Card (dom f) = Card (rng f)
proof end;

theorem Th3: :: POLYFORM:3
for k being Integer st 1 <= k holds
k is Nat
proof end;

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

theorem Th4: :: POLYFORM:4
not 1 is even
proof end;

theorem Th5: :: POLYFORM:5
2 is even
proof end;

theorem Th6: :: POLYFORM:6
not 3 is even
proof end;

theorem Th7: :: POLYFORM:7
4 is even
proof end;

theorem Th8: :: POLYFORM:8
for n being Nat st n is even holds
(- 1) |^ n = 1
proof end;

theorem Th9: :: POLYFORM:9
for n being Nat st not n is even holds
(- 1) |^ n = - 1
proof end;

theorem Th10: :: POLYFORM:10
for n being Nat holds (- 1) |^ n is Integer
proof end;

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

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

theorem Th11: :: POLYFORM:11
for p, q, r being FinSequence holds len (p ^ q) <= len (p ^ (q ^ r))
proof end;

theorem Th12: :: POLYFORM:12
for n being Nat holds 1 < n + 2
proof end;

theorem Th13: :: POLYFORM:13
(- 1) |^ 2 = 1
proof end;

theorem Th14: :: POLYFORM:14
for n being Nat holds (- 1) |^ n = (- 1) |^ (n + 2)
proof end;

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

theorem Th15: :: POLYFORM:15
for a, b, s being FinSequence of INT st len s > 0 & len a = len s & len b = len s & ( for n being Nat st 1 <= n & n <= len s holds
s . n = (a . n) + (b . n) ) & ( for k being Nat st 1 <= k & k < len s holds
b . k = - (a . (k + 1)) ) holds
Sum s = (a . 1) + (b . (len s))
proof end;

theorem Th16: :: POLYFORM:16
for p, q, r being FinSequence holds len ((p ^ q) ^ r) = ((len p) + (len q)) + (len r)
proof end;

theorem Th17: :: POLYFORM:17
for x being set
for p, q being FinSequence holds ((<*x*> ^ p) ^ q) . 1 = x
proof end;

theorem Th18: :: POLYFORM:18
for x being set
for p, q being FinSequence holds ((p ^ q) ^ <*x*>) . (((len p) + (len q)) + 1) = x
proof end;

theorem Th19: :: POLYFORM:19
for p, q, r being FinSequence
for k being Nat st len p < k & k <= len (p ^ q) holds
((p ^ q) ^ r) . k = q . (k - (len p))
proof end;

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

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

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

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

theorem Th20: :: POLYFORM:20
for p, q being FinSequence of INT holds Sum (p ^ q) = (Sum p) + (Sum q)
proof end;

theorem Th21: :: POLYFORM:21
for k being Integer
for p being FinSequence of INT holds Sum (<*k*> ^ p) = k + (Sum p)
proof end;

theorem Th22: :: POLYFORM:22
for p, q, r being FinSequence of INT holds Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r)
proof end;

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

definition
let X, Y be set ;
mode incidence-matrix of X,Y is Element of Funcs [:X,Y:],{(0. Z_2 ),(1. Z_2 )};
end;

theorem Th24: :: POLYFORM:24
for X, Y being set holds [:X,Y:] --> (1. Z_2 ) is incidence-matrix of X,Y
proof end;

definition
attr c1 is strict;
struct PolyhedronStr -> ;
aggr PolyhedronStr(# PolytopsF, IncidenceF #) -> PolyhedronStr ;
sel PolytopsF c1 -> FinSequence-yielding FinSequence;
sel IncidenceF c1 -> Function-yielding FinSequence;
end;

definition
let p be PolyhedronStr ;
attr p is polyhedron_1 means :Def1: :: POLYFORM:def 1
 len the IncidenceF of p = (len the PolytopsF of p) - 1;
attr p is polyhedron_2 means :Def2: :: POLYFORM:def 2
for n being Nat st 1 <= n & n < len the PolytopsF of p holds
the IncidenceF of p . n is incidence-matrix of (rng (the PolytopsF of p . n)),(rng (the PolytopsF of p . (n + 1)));
attr p is polyhedron_3 means :Def3: :: POLYFORM:def 3
for n being Nat st 1 <= n & n <= len the PolytopsF of p holds
( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one );
end;

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

:: deftheorem Def2 defines polyhedron_2 POLYFORM:def 2 :
for p being PolyhedronStr holds
( p is polyhedron_2 iff for n being Nat st 1 <= n & n < len the PolytopsF of p holds
the IncidenceF of p . n is incidence-matrix of (rng (the PolytopsF of p . n)),(rng (the PolytopsF of p . (n + 1))) );

:: deftheorem Def3 defines polyhedron_3 POLYFORM:def 3 :
for p being PolyhedronStr holds
( p is polyhedron_3 iff for n being Nat st 1 <= n & n <= len the PolytopsF of p holds
( not the PolytopsF of p . n is empty & the PolytopsF of p . n is one-to-one ) );

registration
cluster polyhedron_1 polyhedron_2 polyhedron_3 PolyhedronStr ;
existence
ex b1 being PolyhedronStr st
( b1 is polyhedron_1 & b1 is polyhedron_2 & b1 is polyhedron_3 )
proof end;
end;

definition
mode polyhedron is polyhedron_1 polyhedron_2 polyhedron_3 PolyhedronStr ;
end;

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

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

definition
let p be polyhedron;
let k be Integer;
func k -polytopes p -> finite set means :Def5: :: POLYFORM:def 5
( ( k < - 1 implies it = {} ) & ( k = - 1 implies it = {{} } ) & ( - 1 < k & k < dim p implies it = rng (the PolytopsF of p . (k + 1)) ) & ( k = dim p implies it = {p} ) & ( k > dim p implies it = {} ) );
existence
ex 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 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 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 Th25: :: POLYFORM:25
for p being polyhedron
for k being Integer st - 1 < k & k < dim p holds
( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )
proof end;

theorem Th26: :: POLYFORM:26
for p being polyhedron
for k being Integer holds
( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )
proof end;

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

definition
let p be polyhedron;
let k be Integer;
func eta p,k -> incidence-matrix of ((k - 1) -polytopes p),(k -polytopes p) means :Def6: :: POLYFORM:def 6
( ( k < 0 implies it = {} ) & ( k = 0 implies it = [:{{} },(0 -polytopes p):] --> (1. Z_2 ) ) & ( 0 < k & k < dim p implies it = the IncidenceF of p . k ) & ( k = dim p implies it = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 ) ) & ( k > dim p implies it = {} ) );
existence
ex 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 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 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;
func k -polytope-seq p -> FinSequence means :Def7: :: POLYFORM:def 7
( ( k < - 1 implies it = <*> {} ) & ( k = - 1 implies it = <*{} *> ) & ( - 1 < k & k < dim p implies it = the PolytopsF of p . (k + 1) ) & ( k = dim p implies it = <*p*> ) & ( k > dim p implies it = <*> {} ) );
existence
ex 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 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 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 Th28: :: POLYFORM:28
for p being polyhedron
for k being Integer holds dom (k -polytope-seq p) = Seg (num-polytopes p,k)
proof end;

theorem Th29: :: POLYFORM:29
for p being polyhedron
for k being Integer holds len (k -polytope-seq p) = num-polytopes p,k
proof end;

theorem Th30: :: POLYFORM:30
for p being polyhedron
for k being Integer holds rng (k -polytope-seq p) = k -polytopes p
proof end;

theorem Th31: :: POLYFORM:31
for p being polyhedron holds num-polytopes p,(- 1) = 1
proof end;

theorem Th32: :: POLYFORM:32
for p being polyhedron holds num-polytopes p,(dim p) = 1
proof end;

definition
let p be polyhedron;
let k be Integer;
let n be Nat;
assume A1: ( 1 <= n & n <= num-polytopes p,k & - 1 <= k & k <= dim p ) ;
func n -th-polytope p,k -> Element of k -polytopes p equals :Def12: :: POLYFORM:def 12
(k -polytope-seq p) . n;
coherence
(k -polytope-seq p) . n is Element of k -polytopes p
proof end;
end;

:: deftheorem Def12 defines -th-polytope POLYFORM:def 12 :
for p being polyhedron
for k being Integer
for n being Nat st 1 <= n & n <= num-polytopes p,k & -