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


theorem Th1: :: CHAIN_1:1
for x, y being Real st x < y holds
ex z being Element of REAL st
( x < z & z < y )
proof end;

theorem Th2: :: CHAIN_1:2
for x, y being Real ex z being Element of REAL st
( x < z & y < z )
proof end;

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()
proof end;

:: 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 zero 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 Nat;
redefine attr d is zero means :Def2: :: CHAIN_1:def 2
 not d >= 1;
compatibility
( d is zero iff not d >= 1 )
proof end;
end;

:: deftheorem Def2 defines zero CHAIN_1:def 2 :
for d being Nat holds
( d is zero iff not d >= 1 );

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

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

registration
let X be non trivial set ;
let Y be set ;
cluster X \/ Y -> non trivial ;
coherence
not X \/ Y is trivial
proof end;
cluster Y \/ 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 & b1 is finite )
proof end;
end;

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

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() & B c= F2() & not x in B & P1[B] holds
P1[B \/ {x}]
proof end;

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() & y in F2() & 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() & B c= F2() & not x in B & P1[B] holds
P1[B \/ {x}]
proof end;

:: 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 & y in X & x <> y & ( for z being set holds
( not z in X or z = x or z = y ) ) ) )
proof end;

theorem :: CHAIN_1:6
canceled;

::$CT
theorem Th6: :: 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 )
proof end;

theorem Th7: :: 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 )
proof end;

:: elements of REAL d as functions to REAL
definition
let n be Nat;
redefine func REAL n means :Def3: :: CHAIN_1:def 3
 for x being object 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 object holds
( x in b1 iff x is Function of (Seg n),REAL ) )
proof end;
end;

:: deftheorem Def3 defines REAL CHAIN_1:def 3 :
for n being Nat
for b2 being FinSequenceSet of REAL holds
( b2 = REAL n iff for x being object holds
( x in b2 iff x is Function of (Seg n),REAL ) );

:: gratings
definition
let d be non zero 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 & 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 & b1 . i is finite )
proof end;
end;

:: deftheorem Def4 defines Grating CHAIN_1:def 4 :
for d being non zero 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 ) );

registration
let d be non zero Nat;
cluster -> V27() for Grating of d;
coherence
for b1 being Grating of d holds b1 is V27()
proof end;
end;

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

theorem Th8: :: CHAIN_1:9
for d being non zero 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 )
proof end;

theorem :: CHAIN_1:10
canceled;

:: gaps
::$CT
theorem Th9: :: CHAIN_1:11
for X being non empty finite Subset of REAL ex ri being Element of REAL st
( ri in X & ( for xi being Real st xi in X holds
ri >= xi ) )
proof end;

theorem Th10: :: CHAIN_1:12
for X being non empty finite Subset of REAL ex li being Element of REAL st
( li in X & ( for xi being Real st xi in X holds
li <= xi ) )
proof end;

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

theorem :: CHAIN_1:14
canceled;

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

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] & 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 ) ) ) ) );
existence
ex b1 being Element of [:REAL,REAL:] ex li, ri being Real st
( b1 = [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 ) ) ) ) )
proof end;
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] & 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 Th13: :: 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 & 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 ) ) ) ) ) )
proof end;

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 & ri9 = ri ) or ( li9 = ri & ri9 = li ) ) )
proof end;

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

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

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

theorem Th17: :: 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 & [li,ri9] is Gap of Gi holds
ri = ri9
proof end;

theorem Th18: :: 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 & [li9,ri] is Gap of Gi holds
li = li9
proof end;

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

:: cells, chains
definition
let d be non zero 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 & 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 ) ) ) } ;
coherence
{ 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 ) ) ) } is non empty Subset of (REAL d)
proof end;
end;

:: deftheorem defines cell CHAIN_1:def 6 :
for d being non zero 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 Th20: :: CHAIN_1:23
for d being non zero Nat
for l, r, x being Element of REAL d holds
( x in cell (l,r) iff ( 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 ) ) ) )
proof end;

theorem Th21: :: CHAIN_1:24
for d being non zero 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 & x . i <= r . i ) )
proof end;

theorem Th22: :: CHAIN_1:25
for d being non zero Nat
for l, r, 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 & ( x . i <= r . i or l . i <= x . i ) ) )
proof end;

theorem Th23: :: CHAIN_1:26
for d being non zero Nat
for l, r being Element of REAL d holds
( l in cell (l,r) & r in cell (l,r) )
proof end;

theorem Th24: :: CHAIN_1:27
for d being non zero Nat
for x being Element of REAL d holds cell (x,x) = {x}
proof end;

theorem Th25: :: CHAIN_1:28
for d being non zero Nat
for l, r, l9, r9 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 & l . i <= r . i & r . i <= r9 . i ) )
proof end;

theorem Th26: :: CHAIN_1:29
for d being non zero Nat
for l, r, 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 & r9 . i < l9 . i & l9 . i <= l . i ) )
proof end;

theorem Th27: :: CHAIN_1:30
for d being non zero Nat
for l, r, l9, r9 being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i ) & ( 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 ) )
proof end;

theorem Th28: :: CHAIN_1:31
for d being non zero 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 & r = r9 ) )
proof end;

definition
let d be non zero Nat;
let G be Grating of d;
let k be 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 & ( 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 ) ) ) ) } ;
coherence
{ (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 ) ) ) ) } is non empty finite Subset-Family of (REAL d)
proof end;
end;

:: deftheorem Def7 defines cells CHAIN_1:def 7 :
for d being non zero Nat
for G being Grating of d
for k being 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 Th29: :: CHAIN_1:32
for k being Nat
for d being non zero 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) & ( 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 ) ) ) ) ) )
proof end;

theorem Th30: :: CHAIN_1:33
for k being Nat
for d being non zero 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 & ( 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 ) ) ) ) )
proof end;

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

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

theorem :: CHAIN_1:36
for k being Nat
for d being non zero Nat
for l, r being Element of REAL d
for G being Grating of d st k <= d & cell (l,r) in cells (k,G) & 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 Th31;

theorem Th34: :: CHAIN_1:37
for d being non zero 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) & ( for i being Element of Seg d holds x . i in G . i ) ) )
proof end;

theorem Th35: :: CHAIN_1:38
for d being non zero 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 & ( for i being Element of Seg d holds l . i in G . i ) ) )
proof end;

theorem Th36: :: CHAIN_1:39
for d being non zero 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) & ( for i being Element of Seg d holds [(l . i),(r . i)] is Gap of G . i ) & ( 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 ) ) )
proof end;

theorem Th37: :: CHAIN_1:40
for d being non zero 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 ) & ( 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 ) ) )
proof end;

theorem Th38: :: CHAIN_1:41
for d9 being Nat
for d being non zero 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) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
proof end;

theorem :: CHAIN_1:42
for d9 being Nat
for d being non zero 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 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
proof end;

theorem Th40: :: CHAIN_1:43
for d being non zero 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) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) )
proof end;

theorem :: CHAIN_1:44
for d being non zero 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 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds
( l . i = r . i & l . i in G . i ) ) ) )
proof end;

theorem Th42: :: CHAIN_1:45
for k, k9 being Nat
for d being non zero 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 ) )
proof end;

theorem Th43: :: CHAIN_1:46
for k, k9 being Nat
for d being non zero 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 ) )
proof end;

theorem Th44: :: CHAIN_1:47
for d being non zero 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) & ( 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 ) ) ) & ( for i being Element of Seg d holds
( ( i in X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ) holds
( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds
( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds
( l . i = r9 . i & r . i = r9 . i ) ) )
proof end;

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

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

definition
let d be non zero Nat;
let G be Grating of d;
let k be 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 Nat
for G being Grating of d
for k being Nat holds 0_ (k,G) = {} ;

definition
let d be non zero 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
proof end;
end;

:: deftheorem defines Omega CHAIN_1:def 9 :
for d being non zero Nat
for G being Grating of d holds Omega G = cells (d,G);

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

definition
let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let C1, C2 be Chain of k,G;
:: original: +
redefine func C1 + C2 -> Chain of k,G;
coherence
+ is Chain of k,G
proof end;
end;

definition
let d be non zero 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) & ( 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 ) ) )
proof end;
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
proof end;
end;

:: deftheorem Def10 defines infinite-cell CHAIN_1:def 10 :
for d being non zero 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 Th45: :: CHAIN_1:48
for d being non zero 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 )
proof end;

theorem Th46: :: CHAIN_1:49
for d being non zero 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 & [(l . i),(r . i)] is Gap of G . i ) )
proof end;

scheme :: CHAIN_1:sch 4
ChainInd{ F1() -> non zero Nat, F2() -> Grating of F1(), F3() -> 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() & C2 c= F4() & P1[C1] & P1[C2] holds
P1[C1 + C2]
proof end;

:: the boundary operator
definition
let d be non zero Nat;
let G be Grating of d;
let k be 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
proof end;
end;

:: deftheorem defines star CHAIN_1:def 11 :
for d being non zero Nat
for G being Grating of d
for k being Nat
for A being Cell of k,G holds star A = { B where B is Cell of (k + 1),G : A c= B } ;

theorem Th47: :: CHAIN_1:50
for k being Nat
for d being non zero 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 )
proof end;

definition
let d be non zero Nat;
let G be Grating of d;
let k be 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 & card ((star A) /\ C) is odd ) } ;
coherence
{ A where A is Cell of k,G : ( k + 1 <= d & card ((star A) /\ C) is odd ) } is Chain of k,G
proof end;
end;

:: deftheorem defines del CHAIN_1:def 12 :
for d being non zero Nat
for G being Grating of d
for k being Nat
for C being Chain of (k + 1),G holds del C = { A where A is Cell of k,G : ( k + 1 <= d & card ((star A) /\ C) is odd ) } ;

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

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

:: deftheorem defines bounds CHAIN_1:def 13 :
for d being non zero Nat
for G being Grating of d
for k being 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 Th48: :: CHAIN_1:51
for k being Nat
for d being non zero 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 & card ((star A) /\ C) is odd ) )
proof end;

theorem Th49: :: CHAIN_1:52
for k being Nat
for d being non zero 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)
proof end;

theorem Th50: :: CHAIN_1:53
for k being Nat
for d being non zero 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 )
proof end;

:: lemmas
theorem Th51: :: CHAIN_1:54
for d9 being Nat
for d being non zero Nat
for G being Grating of d st d = d9 + 1 holds
for A being Cell of d9,G holds card (star A) = 2
proof end;

theorem Th52: :: CHAIN_1:55
for d being non zero Nat
for G being Grating of d
for B being Cell of (0 + 1),G holds card (del {B}) = 2
proof end;

:: theorems
theorem :: CHAIN_1:56
for d being non zero Nat
for G being Grating of d holds
( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` )
proof end;

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

theorem Th55: :: CHAIN_1:58
for d being non zero Nat
for G being Grating of d
for C being Chain of d,G holds C ` = C + (Omega G)
proof end;

theorem Th56: :: CHAIN_1:59
for k being Nat
for d being non zero Nat
for G being Grating of d holds del (0_ ((k + 1),G)) = 0_ (k,G)
proof end;

theorem Th57: :: CHAIN_1:60
for d9 being Nat
for G being Grating of d9 + 1 holds del (Omega G) = 0_ (d9,G)
proof end;

theorem Th58: :: CHAIN_1:61
for k being Nat
for d being non zero Nat
for G being Grating of d
for C1, C2 being Chain of (k + 1),G holds del (C1 + C2) = (del C1) + (del C2)
proof end;

theorem Th59: :: CHAIN_1:62
for d9 being Nat
for G being Grating of d9 + 1
for C being Chain of (d9 + 1),G holds del (C `) = del C
proof end;

theorem Th60: :: CHAIN_1:63
for k being Nat
for d being non zero Nat
for G being Grating of d
for C being Chain of ((k + 1) + 1),G holds del (del C) = 0_ (k,G)
proof end;

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

:: deftheorem Def14 defines Cycle CHAIN_1:def 14 :
for d being non zero Nat
for G being Grating of d
for k being 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 Nat st
( k = k9 + 1 & ex C being Chain of (k9 + 1),G st
( C = b4 & del C = 0_ (k9,G) ) ) ) );

theorem Th61: :: CHAIN_1:64
for k being Nat
for d being non zero 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) )
proof end;

theorem :: CHAIN_1:65
for k being Nat
for d being non zero 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
proof end;

theorem Th63: :: CHAIN_1:66
for d being non zero 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 )
proof end;

definition
let d be non zero Nat;
let G be Grating of d;
let k be 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 Th61;
end;

:: deftheorem defines del CHAIN_1:def 15 :
for d being non zero Nat
for G being Grating of d
for k being Nat
for C being Cycle of k + 1,G holds del C = 0_ (k,G);

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

definition
let d be non zero 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
proof end;
end;

definition
let d be non zero Nat;
let G be Grating of d;
let k be Nat;
let C1, C2 be Cycle of k,G;
:: original: +
redefine func C1 + C2 -> Cycle of k,G;
coherence
+ is Cycle of k,G
proof end;
end;

theorem :: CHAIN_1:67
for d being non zero Nat
for G being Grating of d
for C being Cycle of d,G holds C ` is Cycle of d,G
proof end;

definition
let d be non zero Nat;
let G be Grating of d;
let k be 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
proof end;
end;

definition
let d be non zero Nat;
let G be Grating of d;
let k be Nat;
func Chains (k,G) -> strict AbGroup means :Def16: :: CHAIN_1:def 16
( 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 ) )
proof end;
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
proof end;
end;

:: deftheorem Def16 defines Chains CHAIN_1:def 16 :
for d being non zero Nat
for G being Grating of d
for k being 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 ) ) );

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

theorem :: CHAIN_1:68
for k being Nat
for d being non zero 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 Nat;
let G be Grating of d;
let k be 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
proof end;
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
proof end;
end;

:: deftheorem defines del CHAIN_1:def 17 :
for d being non zero Nat
for G being Grating of d
for k being 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 );