:: by Freek Wiedijk

::

:: Received January 27, 2003

:: Copyright (c) 2003-2016 Association of Mizar Users

:: 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;
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;

:: non-zero numbers

:: deftheorem defines zero CHAIN_1:def 1 :

for d being real Element of NAT holds

( d is zero iff not d > 0 );

for d being real Element of NAT holds

( d is zero iff not d > 0 );

:: non trivial sets

registration
end;

registration

let X be non trivial set ;

let Y be set ;

coherence

not X \/ Y is trivial

not Y \/ X is trivial ;

end;
let Y be set ;

coherence

not X \/ Y is trivial

proof end;

coherence not Y \/ X is trivial ;

registration

let X be non trivial set ;

existence

ex b_{1} being Subset of X st

( not b_{1} is trivial & b_{1} is finite )

end;
existence

ex b

( not b

proof end;

scheme :: CHAIN_1:sch 2

NonEmptyFinite{ F_{1}() -> non empty set , F_{2}() -> non empty finite Subset of F_{1}(), P_{1}[ set ] } :

provided

NonEmptyFinite{ F

provided

A1:
for x being Element of F_{1}() st x in F_{2}() holds

P_{1}[{x}]
and

A2: for x being Element of F_{1}()

for B being non empty finite Subset of F_{1}() st x in F_{2}() & B c= F_{2}() & not x in B & P_{1}[B] holds

P_{1}[B \/ {x}]

P

A2: for x being Element of F

for B being non empty finite Subset of F

P

proof end;

scheme :: CHAIN_1:sch 3

NonTrivialFinite{ F_{1}() -> non trivial set , F_{2}() -> non trivial finite Subset of F_{1}(), P_{1}[ set ] } :

provided

NonTrivialFinite{ F

provided

A1:
for x, y being Element of F_{1}() st x in F_{2}() & y in F_{2}() & x <> y holds

P_{1}[{x,y}]
and

A2: for x being Element of F_{1}()

for B being non trivial finite Subset of F_{1}() st x in F_{2}() & B c= F_{2}() & not x in B & P_{1}[B] holds

P_{1}[B \/ {x}]

P

A2: for x being Element of F

for B being non trivial finite Subset of F

P

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 ) ) ) )

( 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;

::$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 )

( ( 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 )

( ( 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;

for b_{1} being FinSequenceSet of REAL holds

( b_{1} = REAL n iff for x being object holds

( x in b_{1} iff x is Function of (Seg n),REAL ) )

end;
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 x being object holds

( x in it iff x is Function of (Seg n),REAL );

for b

( b

( x in b

proof end;

:: deftheorem Def3 defines REAL CHAIN_1:def 3 :

for n being Nat

for b_{2} being FinSequenceSet of REAL holds

( b_{2} = REAL n iff for x being object holds

( x in b_{2} iff x is Function of (Seg n),REAL ) );

for n being Nat

for b

( b

( x in b

:: gratings

definition

let d be non zero Nat;

ex b_{1} being Function of (Seg d),(bool REAL) st

for i being Element of Seg d holds

( not b_{1} . i is trivial & b_{1} . i is finite )

end;
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 for i being Element of Seg d holds

( not it . i is trivial & it . i is finite );

ex b

for i being Element of Seg d holds

( not b

proof end;

:: deftheorem Def4 defines Grating CHAIN_1:def 4 :

for d being non zero Nat

for b_{2} being Function of (Seg d),(bool REAL) holds

( b_{2} is Grating of d iff for i being Element of Seg d holds

( not b_{2} . i is trivial & b_{2} . i is finite ) );

for d being non zero Nat

for b

( b

( not b

registration
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;
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;

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 )

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;

:: gaps

::$CT

::$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 ) )

( 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 ) )

( 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 ) )

( li in Gi & ri in Gi & li < ri & ( for xi being Real st xi in Gi & li < xi holds

not xi < ri ) )

proof end;

::$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 ) ) )

( 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;

ex b_{1} being Element of [:REAL,REAL:] ex li, ri being Real st

( b_{1} = [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 ) ) ) ) )

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

ex b

( b

not xi < ri ) ) or ( ri < li & ( for xi being Real st xi in Gi holds

( not li < xi & not xi < ri ) ) ) ) )

proof end;

:: deftheorem Def5 defines Gap CHAIN_1:def 5 :

for Gi being non trivial finite Subset of REAL

for b_{2} being Element of [:REAL,REAL:] holds

( b_{2} is Gap of Gi iff ex li, ri being Real st

( b_{2} = [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 ) ) ) ) ) );

for Gi being non trivial finite Subset of REAL

for b

( b

( b

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 ) ) ) ) ) )

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 ) ) )

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 H

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

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

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

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

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 )

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;

{ 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)

end;
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 ) ) ) } ;

{ 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;

:: 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 ) ) ) } ;

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 ) ) ) )

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 ) )

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 ) ) )

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) )

for l, r being Element of REAL d holds

( l in cell (l,r) & r in cell (l,r) )

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 ) )

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 ) )

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 ) )

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 ) )

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 ;

{ (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)

end;
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 ) ) ) ) } ;

{ (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;

:: 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 ) ) ) ) } ;

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 ) ) ) ) ) )

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 ) ) ) ) )

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 )

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 )

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

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 ) ) )

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 ) ) )

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 ) ) )

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 ) ) )

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 ) ) ) )

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 ) ) ) )

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 ) ) ) )

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 ) ) ) )

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 ) )

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 ) )

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 ) ) )

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;
let G be Grating of d;

let k be Nat;

mode Cell of k,G is Element of cells (k,G);

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;
let G be Grating of d;

let k be Nat;

mode Chain of k,G is Subset of (cells (k,G));

definition

let d be non zero Nat;

let G be Grating of d;

let k be Nat;

coherence

{} is Chain of k,G by SUBSET_1:1;

end;
let G be Grating of d;

let k be Nat;

coherence

{} is Chain of k,G by SUBSET_1:1;

:: 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) = {} ;

for d being non zero Nat

for G being Grating of d

for k being Nat holds 0_ (k,G) = {} ;

definition
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);

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;
let G be Grating of d;

let k be Nat;

let C1, C2 be Chain of k,G;

synonym C1 + C2 for d \+\ G;

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

end;
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;

definition

let d be non zero Nat;

let G be Grating of d;

ex b_{1} being Cell of d,G ex l, r being Element of REAL d st

( b_{1} = cell (l,r) & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) )

for b_{1}, b_{2} being Cell of d,G st ex l, r being Element of REAL d st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}

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

ex b

( b

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) )

proof end;

uniqueness for b

( b

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) & ex l, r being Element of REAL d st

( b

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) holds

b

proof end;

:: deftheorem Def10 defines infinite-cell CHAIN_1:def 10 :

for d being non zero Nat

for G being Grating of d

for b_{3} being Cell of d,G holds

( b_{3} = infinite-cell G iff ex l, r being Element of REAL d st

( b_{3} = cell (l,r) & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) );

for d being non zero Nat

for G being Grating of d

for b

( b

( b

( 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 )

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 ) )

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{ F_{1}() -> non zero Nat, F_{2}() -> Grating of F_{1}(), F_{3}() -> Nat, F_{4}() -> Chain of F_{3}(),F_{2}(), P_{1}[ set ] } :

provided

ChainInd{ F

provided

A1:
P_{1}[ 0_ (F_{3}(),F_{2}())]
and

A2: for A being Cell of F_{3}(),F_{2}() st A in F_{4}() holds

P_{1}[{A}]
and

A3: for C1, C2 being Chain of F_{3}(),F_{2}() st C1 c= F_{4}() & C2 c= F_{4}() & P_{1}[C1] & P_{1}[C2] holds

P_{1}[C1 + C2]

A2: for A being Cell of F

P

A3: for C1, C2 being Chain of F

P

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;

{ B where B is Cell of (k + 1),G : A c= B } is Chain of (k + 1),G

end;
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 } ;

{ B where B is Cell of (k + 1),G : A c= B } is Chain of (k + 1),G

proof 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 } ;

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 )

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;

{ A where A is Cell of k,G : ( k + 1 <= d & card ((star A) /\ C) is odd ) } is Chain of k,G

end;
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 ) } ;

{ A where A is Cell of k,G : ( k + 1 <= d & card ((star A) /\ C) is odd ) } is Chain of k,G

proof 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 ) } ;

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;
let G be Grating of d;

let k be Nat;

let C be Chain of (k + 1),G;

synonym . C for del C;

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;

end;
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;

:: 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 );

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 ) )

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)

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 )

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

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

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) ` )

for G being Grating of d holds

( Omega G = (0_ (d,G)) ` & 0_ (d,G) = (Omega G) ` )

proof end;

theorem :: CHAIN_1:57

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)

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)

for d being non zero Nat

for G being Grating of d holds del (0_ ((k + 1),G)) = 0_ (k,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)

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

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)

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;

ex b_{1} being Chain of k,G st

( ( k = 0 & card b_{1} is even ) or ex k9 being Nat st

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = b_{1} & del C = 0_ (k9,G) ) ) )

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

ex b

( ( k = 0 & card b

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = b

proof 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 b_{4} being Chain of k,G holds

( b_{4} is Cycle of k,G iff ( ( k = 0 & card b_{4} is even ) or ex k9 being Nat st

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = b_{4} & del C = 0_ (k9,G) ) ) ) );

for d being non zero Nat

for G being Grating of d

for k being Nat

for b

( b

( k = k9 + 1 & ex C being Chain of (k9 + 1),G st

( C = b

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) )

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

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 )

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;

compatibility

for b_{1} being Chain of k,G holds

( b_{1} = del C iff b_{1} = 0_ (k,G) )
by Th61;

end;
let G be Grating of d;

let k be Nat;

let C be Cycle of k + 1,G;

compatibility

for b

( b

:: 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);

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

end;
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;

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

end;
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;

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

end;
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;

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

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

end;
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;

definition

let d be non zero Nat;

let G be Grating of d;

let k be Nat;

ex b_{1} being strict AbGroup st

( the carrier of b_{1} = bool (cells (k,G)) & 0. b_{1} = 0_ (k,G) & ( for A, B being Element of b_{1}

for A9, B9 being Chain of k,G st A = A9 & B = B9 holds

A + B = A9 + B9 ) )

for b_{1}, b_{2} being strict AbGroup st the carrier of b_{1} = bool (cells (k,G)) & 0. b_{1} = 0_ (k,G) & ( for A, B being Element of b_{1}

for A9, B9 being Chain of k,G st A = A9 & B = B9 holds

A + B = A9 + B9 ) & the carrier of b_{2} = bool (cells (k,G)) & 0. b_{2} = 0_ (k,G) & ( for A, B being Element of b_{2}

for A9, B9 being Chain of k,G st A = A9 & B = B9 holds

A + B = A9 + B9 ) holds

b_{1} = b_{2}

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

ex b

( the carrier of b

for A9, B9 being Chain of k,G st A = A9 & B = B9 holds

A + B = A9 + B9 ) )

proof end;

uniqueness for b

for A9, B9 being Chain of k,G st A = A9 & B = B9 holds

A + B = A9 + B9 ) & the carrier of b

for A9, B9 being Chain of k,G st A = A9 & B = B9 holds

A + B = A9 + B9 ) holds

b

proof 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 b_{4} being strict AbGroup holds

( b_{4} = Chains (k,G) iff ( the carrier of b_{4} = bool (cells (k,G)) & 0. b_{4} = 0_ (k,G) & ( for A, B being Element of b_{4}

for A9, B9 being Chain of k,G st A = A9 & B = B9 holds

A + B = A9 + B9 ) ) );

for d being non zero Nat

for G being Grating of d

for k being Nat

for b

( b

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;
let G be Grating of d;

let k be Nat;

mode GrChain of k,G is Element of (Chains (k,G));

theorem :: CHAIN_1:68

definition

let d be non zero Nat;

let G be Grating of d;

let k be Nat;

ex b_{1} 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

b_{1} . A = del A9

for b_{1}, b_{2} 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

b_{1} . A = del A9 ) & ( for A being Element of (Chains ((k + 1),G))

for A9 being Chain of (k + 1),G st A = A9 holds

b_{2} . A = del A9 ) holds

b_{1} = b_{2}

end;
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 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;

ex b

for A being Element of (Chains ((k + 1),G))

for A9 being Chain of (k + 1),G st A = A9 holds

b

proof end;

uniqueness for b

for A9 being Chain of (k + 1),G st A = A9 holds

b

for A9 being Chain of (k + 1),G st A = A9 holds

b

b

proof 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 b_{4} being Homomorphism of (Chains ((k + 1),G)),(Chains (k,G)) holds

( b_{4} = 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

b_{4} . A = del A9 );

for d being non zero Nat

for G being Grating of d

for k being Nat

for b

( b

for A9 being Chain of (k + 1),G st A = A9 holds

b