begin
theorem Th1:
theorem Th2:
:: deftheorem defines zero CHAIN_1:def 1 :
for d being real Element of NAT holds
( d is zero iff not d > 0 );
:: deftheorem Def2 defines zero CHAIN_1:def 2 :
for d being Element of NAT holds
( d is zero iff not d >= 1 );
theorem
canceled;
theorem Th4:
theorem Th5:
theorem Th6:
for
X being
set holds
(
card X = 2 iff ex
x,
y being
set st
(
x in X &
y in X &
x <> y & ( for
z being
set holds
( not
z in X or
z = x or
z = y ) ) ) )
theorem
theorem Th8:
theorem Th9:
:: deftheorem CHAIN_1:def 3 :
canceled;
:: deftheorem Def4 defines REAL CHAIN_1:def 4 :
for n being Element of NAT
for b2 being FinSequenceSet of REAL holds
( b2 = REAL n iff for x being set holds
( x in b2 iff x is Function of (Seg n),REAL ) );
begin
:: deftheorem Def5 defines Grating CHAIN_1:def 5 :
for d being non zero Element of NAT
for b2 being Function of (Seg d),(bool REAL) holds
( b2 is Grating of d iff for i being Element of Seg d holds
( not b2 . i is trivial & b2 . i is finite ) );
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem
:: deftheorem Def6 defines Gap CHAIN_1:def 6 :
for Gi being non trivial finite Subset of REAL
for b2 being Element of [:REAL,REAL:] holds
( b2 is Gap of Gi iff ex li, ri being Real st
( b2 = [li,ri] & li in Gi & ri in Gi & ( ( li < ri & ( for xi being Real st xi in Gi & li < xi holds
not xi < ri ) ) or ( ri < li & ( for xi being Real st xi in Gi holds
( not li < xi & not xi < ri ) ) ) ) ) );
theorem Th17:
for
Gi being non
trivial finite Subset of
REAL for
li,
ri being
Real holds
(
[li,ri] is
Gap of
Gi iff (
li in Gi &
ri in Gi & ( (
li < ri & ( for
xi being
Real st
xi in Gi &
li < xi holds
not
xi < ri ) ) or (
ri < li & ( for
xi being
Real st
xi in Gi holds
( not
li < xi & not
xi < ri ) ) ) ) ) )
theorem
deffunc H1( set ) -> set = $1;
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
:: deftheorem defines cell CHAIN_1:def 7 :
for d being non zero Element of NAT
for l, r being Element of REAL d holds cell (l,r) = { x where x is Element of REAL d : ( for i being Element of Seg d holds
( l . i <= x . i & x . i <= r . i ) or ex i being Element of Seg d st
( r . i < l . i & ( x . i <= r . i or l . i <= x . i ) ) ) } ;
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
:: deftheorem Def8 defines cells CHAIN_1:def 8 :
for d being non zero Element of NAT
for G being Grating of d
for k being Element of NAT st k <= d holds
cells (k,G) = { (cell (l,r)) where l, r is Element of REAL d : ( ex X being Subset of (Seg d) st
( card X = k & ( for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) ) ) or ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) } ;
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem
theorem Th46:
for
k,
k9 being
Element of
NAT for
d being non
zero Element of
NAT for
l,
r,
l9,
r9 being
Element of
REAL d for
G being
Grating of
d st
k <= d &
k9 <= d &
cell (
l,
r)
in cells (
k,
G) &
cell (
l9,
r9)
in cells (
k9,
G) &
cell (
l,
r)
c= cell (
l9,
r9) holds
for
i being
Element of
Seg d holds
( (
l . i = l9 . i &
r . i = r9 . i ) or (
l . i = l9 . i &
r . i = l9 . i ) or (
l . i = r9 . i &
r . i = r9 . i ) or (
l . i <= r . i &
r9 . i < l9 . i &
r9 . i <= l . i &
r . i <= l9 . i ) )
theorem Th47:
for
k,
k9 being
Element of
NAT for
d being non
zero Element of
NAT for
l,
r,
l9,
r9 being
Element of
REAL d for
G being
Grating of
d st
k < k9 &
k9 <= d &
cell (
l,
r)
in cells (
k,
G) &
cell (
l9,
r9)
in cells (
k9,
G) &
cell (
l,
r)
c= cell (
l9,
r9) holds
ex
i being
Element of
Seg d st
( (
l . i = l9 . i &
r . i = l9 . i ) or (
l . i = r9 . i &
r . i = r9 . i ) )
theorem Th48:
:: deftheorem defines 0_ CHAIN_1:def 9 :
for d being non zero Element of NAT
for G being Grating of d
for k being Element of NAT holds 0_ (k,G) = {} ;
:: deftheorem defines Omega CHAIN_1:def 10 :
for d being non zero Element of NAT
for G being Grating of d holds Omega G = cells (d,G);
definition
let d be non
zero Element of
NAT ;
let G be
Grating of
d;
func infinite-cell G -> Cell of
d,
G means :
Def11:
ex
l,
r being
Element of
REAL d st
(
it = cell (
l,
r) & ( for
i being
Element of
Seg d holds
(
r . i < l . i &
[(l . i),(r . i)] is
Gap of
G . i ) ) );
existence
ex b1 being Cell of d,G ex l, r being Element of REAL d st
( b1 = cell (l,r) & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) )
uniqueness
for b1, b2 being Cell of d,G st ex l, r being Element of REAL d st
( b1 = cell (l,r) & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) & ex l, r being Element of REAL d st
( b2 = cell (l,r) & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) holds
b1 = b2
end;
:: deftheorem Def11 defines infinite-cell CHAIN_1:def 11 :
for d being non zero Element of NAT
for G being Grating of d
for b3 being Cell of d,G holds
( b3 = infinite-cell G iff ex l, r being Element of REAL d st
( b3 = cell (l,r) & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) );
theorem Th49:
theorem Th50:
scheme
ChainInd{
F1()
-> non
zero Element of
NAT ,
F2()
-> Grating of
F1(),
F3()
-> Element of
NAT ,
F4()
-> Chain of
F3(),
F2(),
P1[
set ] } :
provided
A1:
P1[
0_ (
F3(),
F2())]
and A2:
for
A being
Cell of
F3(),
F2() st
A in F4() holds
P1[
{A}]
and A3:
for
C1,
C2 being
Chain of
F3(),
F2() st
C1 c= F4() &
C2 c= F4() &
P1[
C1] &
P1[
C2] holds
P1[
C1 + C2]
:: deftheorem defines star CHAIN_1:def 12 :
for d being non zero Element of NAT
for G being Grating of d
for k being Element of NAT
for A being Cell of k,G holds star A = { B where B is Cell of (k + 1),G : A c= B } ;
theorem Th51:
:: deftheorem defines del CHAIN_1:def 13 :
for d being non zero Element of NAT
for G being Grating of d
for k being Element of NAT
for C being Chain of (k + 1),G holds del C = { A where A is Cell of k,G : ( k + 1 <= d & not card ((star A) /\ C) is even ) } ;
:: deftheorem defines bounds CHAIN_1:def 14 :
for d being non zero Element of NAT
for G being Grating of d
for k being Element of NAT
for C being Chain of (k + 1),G
for C9 being Chain of k,G holds
( C9 bounds C iff C9 = del C );
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem
theorem
theorem
canceled;
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
:: deftheorem Def15 defines Cycle CHAIN_1:def 15 :
for d being non zero Element of NAT
for G being Grating of d
for k being Element of NAT
for b4 being Chain of k,G holds
( b4 is Cycle of k,G iff ( ( k = 0 & card b4 is even ) or ex k9 being Element of NAT st
( k = k9 + 1 & ex C being Chain of (k9 + 1),G st
( C = b4 & del C = 0_ (k9,G) ) ) ) );
theorem Th66:
theorem
theorem Th68:
:: deftheorem defines del CHAIN_1:def 16 :
for d being non zero Element of NAT
for G being Grating of d
for k being Element of NAT
for C being Cycle of k + 1,G holds del C = 0_ (k,G);
theorem
begin
definition
let d be non
zero Element of
NAT ;
let G be
Grating of
d;
let k be
Element of
NAT ;
func Chains (
k,
G)
-> strict AbGroup means :
Def17:
( the
carrier of
it = bool (cells (k,G)) &
0. it = 0_ (
k,
G) & ( for
A,
B being
Element of
it for
A9,
B9 being
Chain of
k,
G st
A = A9 &
B = B9 holds
A + B = A9 + B9 ) );
existence
ex b1 being strict AbGroup st
( the carrier of b1 = bool (cells (k,G)) & 0. b1 = 0_ (k,G) & ( for A, B being Element of b1
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) )
uniqueness
for b1, b2 being strict AbGroup st the carrier of b1 = bool (cells (k,G)) & 0. b1 = 0_ (k,G) & ( for A, B being Element of b1
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) & the carrier of b2 = bool (cells (k,G)) & 0. b2 = 0_ (k,G) & ( for A, B being Element of b2
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) holds
b1 = b2
end;
:: deftheorem Def17 defines Chains CHAIN_1:def 17 :
for d being non zero Element of NAT
for G being Grating of d
for k being Element of NAT
for b4 being strict AbGroup holds
( b4 = Chains (k,G) iff ( the carrier of b4 = bool (cells (k,G)) & 0. b4 = 0_ (k,G) & ( for A, B being Element of b4
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) ) );
theorem
definition
let d be non
zero Element of
NAT ;
let G be
Grating of
d;
let k be
Element of
NAT ;
func del (
k,
G)
-> Homomorphism of
(Chains ((k + 1),G)),
(Chains (k,G)) means
for
A being
Element of
(Chains ((k + 1),G)) for
A9 being
Chain of
(k + 1),
G st
A = A9 holds
it . A = del A9;
existence
ex b1 being Homomorphism of (Chains ((k + 1),G)),(Chains (k,G)) st
for A being Element of (Chains ((k + 1),G))
for A9 being Chain of (k + 1),G st A = A9 holds
b1 . A = del A9
uniqueness
for b1, b2 being Homomorphism of (Chains ((k + 1),G)),(Chains (k,G)) st ( for A being Element of (Chains ((k + 1),G))
for A9 being Chain of (k + 1),G st A = A9 holds
b1 . A = del A9 ) & ( for A being Element of (Chains ((k + 1),G))
for A9 being Chain of (k + 1),G st A = A9 holds
b2 . A = del A9 ) holds
b1 = b2
end;
:: deftheorem defines del CHAIN_1:def 18 :
for d being non zero Element of NAT
for G being Grating of d
for k being Element of NAT
for b4 being Homomorphism of (Chains ((k + 1),G)),(Chains (k,G)) holds
( b4 = del (k,G) iff for A being Element of (Chains ((k + 1),G))
for A9 being Chain of (k + 1),G st A = A9 holds
b4 . A = del A9 );