:: Chains on a Grating in Euclidean Space
:: by Freek Wiedijk
::
:: Received January 27, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

theorem Th1: :: CHAIN_1:1
for x, y being real number st x < y holds
ex z being Real st
( x < z &amp; z < y )
proofend;

theorem Th2: :: CHAIN_1:2
for x, y being real number ex z being Real st
( x < z &amp; y < z )
proofend;

scheme :: CHAIN_1:sch 1
FrSet12{ F1() ->  non empty set , F2() ->  non empty set , P1[ set , set ], F3( set , set ) ->  Element of F1() } :
  {  F3(x,y) where x, y is Element of F2() : P1[x,y]  }  c= F1()
proofend;

:: Subset A -> Subset B
definition
let B be set ;
let A be Subset of B;
:: original:bool
redefine func bool A ->  Subset-Family of B;
coherence
 bool A is Subset-Family of B by ZFMISC_1:67;
end;

:: non-zero numbers
definition
let d be real Element of NAT ;
redefine attr d is empty  means :: CHAIN_1:def 1
 not d > 0 ;
compatibility
 ( d is zero iff not d > 0 ) ;
end;

:: deftheorem  defines zero CHAIN_1:def_1_:_
 for d being real Element of NAT holds
( d is zero iff not d > 0 );

definition
let d be Element of NAT ;
redefine attr d is empty  means :Def2: :: CHAIN_1:def 2
 not d >= 1;
compatibility
 ( d is zero iff not d >= 1 )
proofend;
end;

:: deftheorem Def2 defines zero CHAIN_1:def_2_:_
 for d being Element of NAT holds
( d is zero iff not d >= 1 );

:: non trivial sets
theorem Th3: :: CHAIN_1:3
for x, y being set holds
( {x,y} is trivial iff x = y )
proofend;

registration
cluster non trivial finite for set ;
existence
 ex b1 being set st
( not b1 is trivial &amp; b1 is finite )
proofend;
end;

registration
let X be non trivial set ;
let Y be set ;
clusterX \/ Y ->  non trivial ;
coherence
 not X \/ Y is trivial
proofend;
clusterY \/ X ->  non trivial ;
coherence
 not Y \/ X is trivial ;
end;

registration
let X be non trivial set ;
cluster non trivial finite for Element of bool X;
existence
 ex b1 being Subset of X st
( not b1 is trivial &amp; b1 is finite )
proofend;
end;

theorem Th4: :: CHAIN_1:4
for X, y being set st X is trivial &amp; not X \/ {y} is trivial holds
ex x being set st X = {x}
proofend;

scheme :: CHAIN_1:sch 2
NonEmptyFinite{ F1() ->  non empty set , F2() ->  non empty finite Subset of F1(), P1[ set ] } :
 P1[F2()]
provided
A1: for x being Element of F1() st x in F2() holds
P1[{x}] and
A2: for x being Element of F1()
for B being non empty finite Subset of F1() st x in F2() &amp; B c= F2() &amp; not x in B &amp; P1[B] holds
P1[B \/ {x}]
proofend;

scheme :: CHAIN_1:sch 3
NonTrivialFinite{ F1() ->  non trivial set , F2() ->  non trivial finite Subset of F1(), P1[ set ] } :
 P1[F2()]
provided
A1: for x, y being Element of F1() st x in F2() &amp; y in F2() &amp; x <> y holds
P1[{x,y}] and
A2: for x being Element of F1()
for B being non trivial finite Subset of F1() st x in F2() &amp; B c= F2() &amp; not x in B &amp; P1[B] holds
P1[B \/ {x}]
proofend;

:: sets of cardinality 2
theorem Th5: :: CHAIN_1:5
for X being set holds
( card X = 2 iff ex x, y being set st
( x in X &amp; y in X &amp; x <> y &amp; ( for z being set holds
( not z in X or z = x or z = y ) ) ) )
proofend;

theorem :: CHAIN_1:6
for m, n being Element of NAT holds
( ( m is even iff n is even ) iff m + n is even ) ;

theorem Th7: :: CHAIN_1:7
for X, Y being finite set st X misses Y holds
( ( card X is even iff card Y is even ) iff card (X \/ Y) is even )
proofend;

theorem Th8: :: CHAIN_1:8
for X, Y being finite set holds
( ( card X is even iff card Y is even ) iff card (X \+\ Y) is even )
proofend;

:: elements of REAL d as functions to REAL
definition
let n be Element of NAT ;
redefine func REAL n means :Def3: :: CHAIN_1:def 3
 for x being set holds
( x in it iff x is Function of (Seg n),REAL );
compatibility
 for b1 being FinSequenceSet of REAL holds
( b1 = REAL n iff for x being set holds
( x in b1 iff x is Function of (Seg n),REAL ) )
proofend;
end;

:: deftheorem Def3 defines REAL CHAIN_1:def_3_:_
 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

:: gratings
definition
let d be non zero Element of NAT ;
mode Grating of d ->  Function of (Seg d),(bool REAL) means :Def4: :: CHAIN_1:def 4
 for i being Element of Seg d holds
( not it . i is trivial &amp; it . i is finite );
existence
 ex b1 being Function of (Seg d),(bool REAL) st
for i being Element of Seg d holds
( not b1 . i is trivial &amp; b1 . i is finite )
proofend;
end;

:: deftheorem Def4 defines Grating CHAIN_1:def_4_:_
 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 &amp; b2 . i is finite ) );

registration
let d be non zero Element of NAT ;
cluster  -> V25() for Grating of d;
coherence
 for b1 being Grating of d holds b1 is V25()
proofend;
end;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let i be Element of Seg d;
:: original:.
redefine funcG . i ->  non trivial finite Subset of REAL;
coherence
 G . i is non trivial finite Subset of REAL by Def4;
end;

theorem Th9: :: CHAIN_1:9
for d being non zero Element of NAT
for x being Element of REAL d
for G being Grating of d holds
( x in product G iff for i being Element of Seg d holds x . i in G . i )
proofend;

theorem :: CHAIN_1:10
canceled;

theorem Th11: :: CHAIN_1:11
for X being non empty finite Subset of REAL ex ri being Real st
( ri in X &amp; ( for xi being Real st xi in X holds
ri >= xi ) )
proofend;

theorem Th12: :: CHAIN_1:12
for X being non empty finite Subset of REAL ex li being Real st
( li in X &amp; ( for xi being Real st xi in X holds
li <= xi ) )
proofend;

theorem Th13: :: CHAIN_1:13
for Gi being non trivial finite Subset of REAL ex li, ri being Real st
( li in Gi &amp; ri in Gi &amp; li < ri &amp; ( for xi being Real st xi in Gi &amp; li < xi holds
not xi < ri ) )
proofend;

theorem :: CHAIN_1:14
for X being non empty finite Subset of REAL ex ri being Real st
( ri in X &amp; ( for xi being Real st xi in X holds
ri >= xi ) ) by Th11;

theorem :: CHAIN_1:15
for Gi being non trivial finite Subset of REAL ex li, ri being Real st
( li in Gi &amp; ri in Gi &amp; ri < li &amp; ( for xi being Real st xi in Gi holds
( not xi < ri &amp; not li < xi ) ) )
proofend;

definition
let Gi be non trivial finite Subset of REAL;
mode Gap of Gi ->  Element of [:REAL,REAL:] means :Def5: :: CHAIN_1:def 5
 ex li, ri being Real st
( it = [li,ri] &amp; li in Gi &amp; ri in Gi &amp; ( ( li < ri &amp; ( for xi being Real st xi in Gi &amp; li < xi holds
not xi < ri ) ) or ( ri < li &amp; ( for xi being Real st xi in Gi holds
( not li < xi &amp; not xi < ri ) ) ) ) );
existence
 ex b1 being Element of [:REAL,REAL:] ex li, ri being Real st
( b1 = [li,ri] &amp; li in Gi &amp; ri in Gi &amp; ( ( li < ri &amp; ( for xi being Real st xi in Gi &amp; li < xi holds
not xi < ri ) ) or ( ri < li &amp; ( for xi being Real st xi in Gi holds
( not li < xi &amp; not xi < ri ) ) ) ) )
proofend;
end;

:: deftheorem Def5 defines Gap CHAIN_1:def_5_:_
 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] &amp; li in Gi &amp; ri in Gi &amp; ( ( li < ri &amp; ( for xi being Real st xi in Gi &amp; li < xi holds
not xi < ri ) ) or ( ri < li &amp; ( for xi being Real st xi in Gi holds
( not li < xi &amp; not xi < ri ) ) ) ) ) );

theorem Th16: :: CHAIN_1:16
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 &amp; ri in Gi &amp; ( ( li < ri &amp; ( for xi being Real st xi in Gi &amp; li < xi holds
not xi < ri ) ) or ( ri < li &amp; ( for xi being Real st xi in Gi holds
( not li < xi &amp; not xi < ri ) ) ) ) ) )
proofend;

theorem :: CHAIN_1:17
for Gi being non trivial finite Subset of REAL
for li, ri, li9, ri9 being Real st Gi = {li,ri} holds
( [li9,ri9] is Gap of Gi iff ( ( li9 = li &amp; ri9 = ri ) or ( li9 = ri &amp; ri9 = li ) ) )
proofend;

deffunc H1( set ) ->  set = $1;

theorem Th18: :: CHAIN_1:18
for Gi being non trivial finite Subset of REAL
for xi being Real st xi in Gi holds
ex ri being Real st [xi,ri] is Gap of Gi
proofend;

theorem Th19: :: CHAIN_1:19
for Gi being non trivial finite Subset of REAL
for xi being Real st xi in Gi holds
ex li being Real st [li,xi] is Gap of Gi
proofend;

theorem Th20: :: CHAIN_1:20
for Gi being non trivial finite Subset of REAL
for li, ri, ri9 being Real st [li,ri] is Gap of Gi &amp; [li,ri9] is Gap of Gi holds
ri = ri9
proofend;

theorem Th21: :: CHAIN_1:21
for Gi being non trivial finite Subset of REAL
for li, ri, li9 being Real st [li,ri] is Gap of Gi &amp; [li9,ri] is Gap of Gi holds
li = li9
proofend;

theorem Th22: :: CHAIN_1:22
for Gi being non trivial finite Subset of REAL
for ri, li, ri9, li9 being Real st ri < li &amp; [li,ri] is Gap of Gi &amp; ri9 < li9 &amp; [li9,ri9] is Gap of Gi holds
( li = li9 &amp; ri = ri9 )
proofend;

:: cells, chains
definition
let d be non zero Element of NAT ;
let l, r be Element of REAL d;
func cell (l,r) ->  non empty Subset of (REAL d) equals :: CHAIN_1:def 6
 {  x where x is Element of REAL d : ( for i being Element of Seg d holds
( l . i <= x . i &amp; x . i <= r . i ) or ex i being Element of Seg d st
( r . i < l . i &amp; ( x . i <= r . i or l . i <= x . i ) ) )  }  ;
coherence
  {  x where x is Element of REAL d : ( for i being Element of Seg d holds
( l . i <= x . i &amp; x . i <= r . i ) or ex i being Element of Seg d st
( r . i < l . i &amp; ( x . i <= r . i or l . i <= x . i ) ) )  }  is non empty Subset of (REAL d)
proofend;
end;

:: deftheorem  defines cell CHAIN_1:def_6_:_
 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 &amp; x . i <= r . i ) or ex i being Element of Seg d st
( r . i < l . i &amp; ( x . i <= r . i or l . i <= x . i ) ) )  }  ;

theorem Th23: :: CHAIN_1:23
for d being non zero Element of NAT
for x, l, r being Element of REAL d holds
( x in cell (l,r) iff ( for i being Element of Seg d holds
( l . i <= x . i &amp; x . i <= r . i ) or ex i being Element of Seg d st
( r . i < l . i &amp; ( x . i <= r . i or l . i <= x . i ) ) ) )
proofend;

theorem Th24: :: CHAIN_1:24
for d being non zero Element of NAT
for l, r, x being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i ) holds
( x in cell (l,r) iff for i being Element of Seg d holds
( l . i <= x . i &amp; x . i <= r . i ) )
proofend;

theorem Th25: :: CHAIN_1:25
for d being non zero Element of NAT
for r, l, x being Element of REAL d st ex i being Element of Seg d st r . i < l . i holds
( x in cell (l,r) iff ex i being Element of Seg d st
( r . i < l . i &amp; ( x . i <= r . i or l . i <= x . i ) ) )
proofend;

theorem Th26: :: CHAIN_1:26
for d being non zero Element of NAT
for l, r being Element of REAL d holds
( l in cell (l,r) &amp; r in cell (l,r) )
proofend;

theorem Th27: :: CHAIN_1:27
for d being non zero Element of NAT
for x being Element of REAL d holds cell (x,x) = {x}
proofend;

theorem Th28: :: CHAIN_1:28
for d being non zero Element of NAT
for l9, r9, l, r being Element of REAL d st ( for i being Element of Seg d holds l9 . i <= r9 . i ) holds
( cell (l,r) c= cell (l9,r9) iff for i being Element of Seg d holds
( l9 . i <= l . i &amp; l . i <= r . i &amp; r . i <= r9 . i ) )
proofend;

theorem Th29: :: CHAIN_1:29
for d being non zero Element of NAT
for r, l, l9, r9 being Element of REAL d st ( for i being Element of Seg d holds r . i < l . i ) holds
( cell (l,r) c= cell (l9,r9) iff for i being Element of Seg d holds
( r . i <= r9 . i &amp; r9 . i < l9 . i &amp; l9 . i <= l . i ) )
proofend;

theorem Th30: :: CHAIN_1:30
for d being non zero Element of NAT
for l, r, r9, l9 being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i ) &amp; ( for i being Element of Seg d holds r9 . i < l9 . i ) holds
( cell (l,r) c= cell (l9,r9) iff ex i being Element of Seg d st
( r . i <= r9 . i or l9 . i <= l . i ) )
proofend;

theorem Th31: :: CHAIN_1:31
for d being non zero Element of NAT
for l, r, l9, r9 being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i or for i being Element of Seg d holds l . i > r . i ) holds
( cell (l,r) = cell (l9,r9) iff ( l = l9 &amp; r = r9 ) )
proofend;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
assume A1: k <= d ;
func cells (k,G) ->  non empty finite Subset-Family of (REAL d) equals :Def7: :: CHAIN_1:def 7
 {  (cell (l,r)) where l, r is Element of REAL d : ( ex X being Subset of (Seg d) st
( card X = k &amp; ( for i being Element of Seg d holds
( ( i in X &amp; l . i < r . i &amp; [(l . i),(r . i)] is Gap of G . i ) or ( not i in X &amp; l . i = r . i &amp; l . i in G . i ) ) ) ) or ( k = d &amp; ( for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) ) )  }  ;
coherence
  {  (cell (l,r)) where l, r is Element of REAL d : ( ex X being Subset of (Seg d) st
( card X = k &amp; ( for i being Element of Seg d holds
( ( i in X &amp; l . i < r . i &amp; [(l . i),(r . i)] is Gap of G . i ) or ( not i in X &amp; l . i = r . i &amp; l . i in G . i ) ) ) ) or ( k = d &amp; ( for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) ) )  }  is non empty finite Subset-Family of (REAL d)
proofend;
end;

:: deftheorem Def7 defines cells CHAIN_1:def_7_:_
 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 &amp; ( for i being Element of Seg d holds
( ( i in X &amp; l . i < r . i &amp; [(l . i),(r . i)] is Gap of G . i ) or ( not i in X &amp; l . i = r . i &amp; l . i in G . i ) ) ) ) or ( k = d &amp; ( for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) ) )  }  ;

theorem Th32: :: CHAIN_1:32
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d st k <= d holds
for A being Subset of (REAL d) holds
( A in cells (k,G) iff ex l, r being Element of REAL d st
( A = cell (l,r) &amp; ( ex X being Subset of (Seg d) st
( card X = k &amp; ( for i being Element of Seg d holds
( ( i in X &amp; l . i < r . i &amp; [(l . i),(r . i)] is Gap of G . i ) or ( not i in X &amp; l . i = r . i &amp; l . i in G . i ) ) ) ) or ( k = d &amp; ( for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )
proofend;

theorem Th33: :: CHAIN_1:33
for k being Element of NAT
for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d st k <= d holds
( cell (l,r) in cells (k,G) iff ( ex X being Subset of (Seg d) st
( card X = k &amp; ( for i being Element of Seg d holds
( ( i in X &amp; l . i < r . i &amp; [(l . i),(r . i)] is Gap of G . i ) or ( not i in X &amp; l . i = r . i &amp; l . i in G . i ) ) ) ) or ( k = d &amp; ( for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) ) ) )
proofend;

theorem Th34: :: CHAIN_1:34
for k being Element of NAT
for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d st k <= d &amp; cell (l,r) in cells (k,G) &amp; ex i being Element of Seg d st
( not ( l . i < r . i &amp; [(l . i),(r . i)] is Gap of G . i ) &amp; not ( l . i = r . i &amp; l . i in G . i ) ) holds
for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i )
proofend;

theorem Th35: :: CHAIN_1:35
for k being Element of NAT
for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d st k <= d &amp; cell (l,r) in cells (k,G) holds
for i being Element of Seg d holds
( l . i in G . i &amp; r . i in G . i )
proofend;

theorem :: CHAIN_1:36
for k being Element of NAT
for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d st k <= d &amp; cell (l,r) in cells (k,G) &amp; not  for i being Element of Seg d holds l . i <= r . i holds
for i being Element of Seg d holds r . i < l . i by Th34;

theorem Th37: :: CHAIN_1:37
for d being non zero Element of NAT
for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells (0,G) iff ex x being Element of REAL d st
( A = cell (x,x) &amp; ( for i being Element of Seg d holds x . i in G . i ) ) )
proofend;

theorem Th38: :: CHAIN_1:38
for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d holds
( cell (l,r) in cells (0,G) iff ( l = r &amp; ( for i being Element of Seg d holds l . i in G . i ) ) )
proofend;

theorem Th39: :: CHAIN_1:39
for d being non zero Element of NAT
for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells (d,G) iff ex l, r being Element of REAL d st
( A = cell (l,r) &amp; ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) &amp; ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )
proofend;

theorem Th40: :: CHAIN_1:40
for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d holds
( cell (l,r) in cells (d,G) iff ( ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) &amp; ( for i being Element of Seg d holds l . i < r . i or for i being Element of Seg d holds r . i < l . i ) ) )
proofend;

theorem Th41: :: CHAIN_1:41
for d9 being Element of NAT
for d being non zero Element of NAT
for G being Grating of d st d = d9 + 1 holds
for A being Subset of (REAL d) holds
( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) &amp; l . i0 = r . i0 &amp; l . i0 in G . i0 &amp; ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) ) )
proofend;

theorem :: CHAIN_1:42
for d9 being Element of NAT
for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d st d = d9 + 1 holds
( cell (l,r) in cells (d9,G) iff ex i0 being Element of Seg d st
( l . i0 = r . i0 &amp; l . i0 in G . i0 &amp; ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) ) )
proofend;

theorem Th43: :: CHAIN_1:43
for d being non zero Element of NAT
for G being Grating of d
for A being Subset of (REAL d) holds
( A in cells (1,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st
( A = cell (l,r) &amp; ( l . i0 < r . i0 or ( d = 1 &amp; r . i0 < l . i0 ) ) &amp; [(l . i0),(r . i0)] is Gap of G . i0 &amp; ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i &amp; l . i in G . i ) ) ) )
proofend;

theorem :: CHAIN_1:44
for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d holds
( cell (l,r) in cells (1,G) iff ex i0 being Element of Seg d st
( ( l . i0 < r . i0 or ( d = 1 &amp; r . i0 < l . i0 ) ) &amp; [(l . i0),(r . i0)] is Gap of G . i0 &amp; ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i &amp; l . i in G . i ) ) ) )
proofend;

theorem Th45: :: CHAIN_1:45
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 &amp; k9 <= d &amp; cell (l,r) in cells (k,G) &amp; cell (l9,r9) in cells (k9,G) &amp; cell (l,r) c= cell (l9,r9) holds
for i being Element of Seg d holds
( ( l . i = l9 . i &amp; r . i = r9 . i ) or ( l . i = l9 . i &amp; r . i = l9 . i ) or ( l . i = r9 . i &amp; r . i = r9 . i ) or ( l . i <= r . i &amp; r9 . i < l9 . i &amp; r9 . i <= l . i &amp; r . i <= l9 . i ) )
proofend;

theorem Th46: :: CHAIN_1:46
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 &amp; k9 <= d &amp; cell (l,r) in cells (k,G) &amp; cell (l9,r9) in cells (k9,G) &amp; cell (l,r) c= cell (l9,r9) holds
ex i being Element of Seg d st
( ( l . i = l9 . i &amp; r . i = l9 . i ) or ( l . i = r9 . i &amp; r . i = r9 . i ) )
proofend;

theorem Th47: :: CHAIN_1:47
for d being non zero Element of NAT
for l, r, l9, r9 being Element of REAL d
for G being Grating of d
for X, X9 being Subset of (Seg d) st cell (l,r) c= cell (l9,r9) &amp; ( for i being Element of Seg d holds
( ( i in X &amp; l . i < r . i &amp; [(l . i),(r . i)] is Gap of G . i ) or ( not i in X &amp; l . i = r . i &amp; l . i in G . i ) ) ) &amp; ( for i being Element of Seg d holds
( ( i in X9 &amp; l9 . i < r9 . i &amp; [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 &amp; l9 . i = r9 . i &amp; l9 . i in G . i ) ) ) holds
( X c= X9 &amp; ( for i being Element of Seg d st ( i in X or not i in X9 ) holds
( l . i = l9 . i &amp; r . i = r9 . i ) ) &amp; ( for i being Element of Seg d st not i in X &amp; i in X9 &amp; not ( l . i = l9 . i &amp; r . i = l9 . i ) holds
( l . i = r9 . i &amp; r . i = r9 . i ) ) )
proofend;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
mode Cell of k,G is Element of cells (k,G);
end;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
mode Chain of k,G is Subset of (cells (k,G));
end;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
func 0_ (k,G) ->  Chain of k,G equals :: CHAIN_1:def 8
 {} ;
coherence
 {} is Chain of k,G by SUBSET_1:1;
end;

:: deftheorem  defines 0_ CHAIN_1:def_8_:_
 for d being non zero Element of NAT
for G being Grating of d
for k being Element of NAT holds 0_ (k,G) = {} ;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
func Omega G ->  Chain of d,G equals :: CHAIN_1:def 9
 cells (d,G);
coherence
 cells (d,G) is Chain of d,G
proofend;
end;

:: deftheorem  defines Omega CHAIN_1:def_9_:_
 for d being non zero Element of NAT
for G being Grating of d holds Omega G = cells (d,G);

notation
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
let C1, C2 be Chain of k,G;
synonym C1 + C2 for d \+\ G;
end;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
let C1, C2 be Chain of k,G;
:: original:+
redefine funcC1 + C2 ->  Chain of k,G;
coherence
 + is Chain of k,G
proofend;
end;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
func infinite-cell G ->  Cell of d,G means :Def10: :: CHAIN_1:def 10
 ex l, r being Element of REAL d st
( it = cell (l,r) &amp; ( for i being Element of Seg d holds
( r . i < l . i &amp; [(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) &amp; ( for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) )
proofend;
uniqueness
 for b1, b2 being Cell of d,G st ex l, r being Element of REAL d st
( b1 = cell (l,r) &amp; ( for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) ) &amp; ex l, r being Element of REAL d st
( b2 = cell (l,r) &amp; ( for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines infinite-cell CHAIN_1:def_10_:_
 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) &amp; ( for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i ) ) ) );

theorem Th48: :: CHAIN_1:48
for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d st cell (l,r) is Cell of d,G holds
( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds r . i < l . i )
proofend;

theorem Th49: :: CHAIN_1:49
for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d holds
( cell (l,r) = infinite-cell G iff for i being Element of Seg d holds
( r . i < l . i &amp; [(l . i),(r . i)] is Gap of G . i ) )
proofend;

scheme :: CHAIN_1:sch 4
ChainInd{ F1() ->  non zero Element of NAT , F2() ->  Grating of F1(), F3() ->  Element of NAT , F4() ->  Chain of F3(),F2(), P1[ set ] } :
 P1[F4()]
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() &amp; C2 c= F4() &amp; P1[C1] &amp; P1[C2] holds
P1[C1 + C2]
proofend;

:: the boundary operator
definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
let A be Cell of k,G;
func star A ->  Chain of (k + 1),G equals :: CHAIN_1:def 11
 {  B where B is Cell of (k + 1),G : A c= B  }  ;
coherence
  {  B where B is Cell of (k + 1),G : A c= B  }  is Chain of (k + 1),G
proofend;
end;

:: deftheorem  defines star CHAIN_1:def_11_:_
 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 Th50: :: CHAIN_1:50
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d
for A being Cell of k,G
for B being Cell of (k + 1),G holds
( B in star A iff A c= B )
proofend;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
let C be Chain of (k + 1),G;
func del C ->  Chain of k,G equals :: CHAIN_1:def 12
 {  A where A is Cell of k,G : ( k + 1 <= d &amp; card ((star A) /\ C) is odd )  }  ;
coherence
  {  A where A is Cell of k,G : ( k + 1 <= d &amp; card ((star A) /\ C) is odd )  }  is Chain of k,G
proofend;
end;

:: deftheorem  defines del 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 C being Chain of (k + 1),G holds del C =  {  A where A is Cell of k,G : ( k + 1 <= d &amp; card ((star A) /\ C) is odd )  }  ;

notation
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
let C be Chain of (k + 1),G;
synonym  . C for  del C;
end;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
let C be Chain of (k + 1),G;
let C9 be Chain of k,G;
predC9 bounds C means :: CHAIN_1:def 13
C9 = del C;
end;

:: deftheorem  defines bounds 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
for C9 being Chain of k,G holds
( C9 bounds C iff C9 = del C );

theorem Th51: :: CHAIN_1:51
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d
for A being Cell of k,G
for C being Chain of (k + 1),G holds
( A in del C iff ( k + 1 <= d &amp; card ((star A) /\ C) is odd ) )
proofend;

theorem Th52: :: CHAIN_1:52
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d st k + 1 > d holds
for C being Chain of (k + 1),G holds del C = 0_ (k,G)
proofend;

theorem Th53: :: CHAIN_1:53
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d st k + 1 <= d holds
for A being Cell of k,G
for B being Cell of (k + 1),G holds
( A in del {B} iff A c= B )
proofend;

:: lemmas
theorem Th54: :: CHAIN_1:54
for d9 being Element of NAT
for d being non zero Element of NAT
for G being Grating of d st d = d9 + 1 holds
for A being Cell of d9,G holds card (star A) = 2
proofend;

theorem Th55: :: CHAIN_1:55
for d being non zero Element of NAT
for G being Grating of d
for B being Cell of (0 + 1),G holds card (del {B}) = 2
proofend;

:: theorems
theorem :: CHAIN_1:56
for d being non zero Element of NAT
for G being Grating of d holds
( Omega G = (0_ (d,G)) ` &amp; 0_ (d,G) = (Omega G) ` )
proofend;

theorem :: CHAIN_1:57
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d
for C being Chain of k,G holds C + (0_ (k,G)) = C ;

theorem Th58: :: CHAIN_1:58
for d being non zero Element of NAT
for G being Grating of d
for C being Chain of d,G holds C ` = C + (Omega G)
proofend;

theorem Th59: :: CHAIN_1:59
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d holds del (0_ ((k + 1),G)) = 0_ (k,G)
proofend;

theorem Th60: :: CHAIN_1:60
for d9 being Element of NAT
for G being Grating of d9 + 1 holds del (Omega G) = 0_ (d9,G)
proofend;

theorem Th61: :: CHAIN_1:61
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d
for C1, C2 being Chain of (k + 1),G holds del (C1 + C2) = (del C1) + (del C2)
proofend;

theorem Th62: :: CHAIN_1:62
for d9 being Element of NAT
for G being Grating of d9 + 1
for C being Chain of (d9 + 1),G holds del (C `) = del C
proofend;

theorem Th63: :: CHAIN_1:63
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d
for C being Chain of ((k + 1) + 1),G holds del (del C) = 0_ (k,G)
proofend;

:: cycles
definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
mode Cycle of k,G ->  Chain of k,G means :Def14: :: CHAIN_1:def 14
( ( k = 0 &amp; card it is even ) or ex k9 being Element of NAT st
( k = k9 + 1 &amp; ex C being Chain of (k9 + 1),G st
( C = it &amp; del C = 0_ (k9,G) ) ) );
existence
 ex b1 being Chain of k,G st
( ( k = 0 &amp; card b1 is even ) or ex k9 being Element of NAT st
( k = k9 + 1 &amp; ex C being Chain of (k9 + 1),G st
( C = b1 &amp; del C = 0_ (k9,G) ) ) )
proofend;
end;

:: deftheorem Def14 defines Cycle 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 b4 being Chain of k,G holds
( b4 is Cycle of k,G iff ( ( k = 0 &amp; card b4 is even ) or ex k9 being Element of NAT st
( k = k9 + 1 &amp; ex C being Chain of (k9 + 1),G st
( C = b4 &amp; del C = 0_ (k9,G) ) ) ) );

theorem Th64: :: CHAIN_1:64
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d
for C being Chain of (k + 1),G holds
( C is Cycle of k + 1,G iff del C = 0_ (k,G) )
proofend;

theorem :: CHAIN_1:65
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d st k > d holds
for C being Chain of k,G holds C is Cycle of k,G
proofend;

theorem Th66: :: CHAIN_1:66
for d being non zero Element of NAT
for G being Grating of d
for C being Chain of 0,G holds
( C is Cycle of 0 ,G iff card C is even )
proofend;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
let C be Cycle of k + 1,G;
redefine func del C equals :: CHAIN_1:def 15
 0_ (k,G);
compatibility
 for b1 being Chain of k,G holds
( b1 = del C iff b1 = 0_ (k,G) ) by Th64;
end;

:: deftheorem  defines del 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 C being Cycle of k + 1,G holds del C = 0_ (k,G);

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
:: original:0_
redefine func 0_ (k,G) ->  Cycle of k,G;
coherence
 0_ (k,G) is Cycle of k,G
proofend;
end;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
:: original:Omega
redefine func Omega G ->  Cycle of d,G;
coherence
 Omega G is Cycle of d,G
proofend;
end;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
let C1, C2 be Cycle of k,G;
:: original:+
redefine funcC1 + C2 ->  Cycle of k,G;
coherence
 + is Cycle of k,G
proofend;
end;

theorem :: CHAIN_1:67
for d being non zero Element of NAT
for G being Grating of d
for C being Cycle of d,G holds C ` is Cycle of d,G
proofend;

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
let C be Chain of (k + 1),G;
:: original:del
redefine func del C ->  Cycle of k,G;
coherence
 del C is Cycle of k,G
proofend;
end;

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 :Def16: :: CHAIN_1:def 16
( the carrier of it = bool (cells (k,G)) &amp; 0. it = 0_ (k,G) &amp; ( for A, B being Element of it
for A9, B9 being Chain of k,G st A = A9 &amp; B = B9 holds
A + B = A9 + B9 ) );
existence
 ex b1 being strict AbGroup st
( the carrier of b1 = bool (cells (k,G)) &amp; 0. b1 = 0_ (k,G) &amp; ( for A, B being Element of b1
for A9, B9 being Chain of k,G st A = A9 &amp; B = B9 holds
A + B = A9 + B9 ) )
proofend;
uniqueness
 for b1, b2 being strict AbGroup st the carrier of b1 = bool (cells (k,G)) &amp; 0. b1 = 0_ (k,G) &amp; ( for A, B being Element of b1
for A9, B9 being Chain of k,G st A = A9 &amp; B = B9 holds
A + B = A9 + B9 ) &amp; the carrier of b2 = bool (cells (k,G)) &amp; 0. b2 = 0_ (k,G) &amp; ( for A, B being Element of b2
for A9, B9 being Chain of k,G st A = A9 &amp; B = B9 holds
A + B = A9 + B9 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def16 defines Chains 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 b4 being strict AbGroup holds
( b4 = Chains (k,G) iff ( the carrier of b4 = bool (cells (k,G)) &amp; 0. b4 = 0_ (k,G) &amp; ( for A, B being Element of b4
for A9, B9 being Chain of k,G st A = A9 &amp; B = B9 holds
A + B = A9 + B9 ) ) );

definition
let d be non zero Element of NAT ;
let G be Grating of d;
let k be Element of NAT ;
mode GrChain of k,G is Element of (Chains (k,G));
end;

theorem :: CHAIN_1:68
for k being Element of NAT
for d being non zero Element of NAT
for G being Grating of d
for x being set holds
( x is Chain of k,G iff x is GrChain of k,G ) by Def16;

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 :: CHAIN_1:def 17
 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
proofend;
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 ) &amp; ( 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
proofend;
end;

:: deftheorem  defines del 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 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 );