:: 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{ F₁() -> non empty set , F₂() -> non empty set , P₁[ set , set ], F₃( set , set ) -> Element of F₁() } :

{ F₃(x,y) where x, y is Element of F₂() : P₁[x,y] } c= F₁()

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 b₁ being set st
( not b₁ is trivial & b₁ 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 b₁ being Subset of X st
( not b₁ is trivial & b₁ 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{ F₁() -> non empty set , F₂() -> non empty finite Subset of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

A1: for x being Element of F₁() st x in F₂() holds
P₁[{x}] and
A2: for x being Element of F₁()
for B being non empty finite Subset of F₁() st x in F₂() & B c= F₂() & not x in B & P₁[B] holds
P₁[B \/ {x}]

proof end;

scheme :: CHAIN_1:sch 3
NonTrivialFinite{ F₁() -> non trivial set , F₂() -> non trivial finite Subset of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

A1: for x, y being Element of F₁() st x in F₂() & y in F₂() & x <> y holds
P₁[{x,y}] and
A2: for x being Element of F₁()
for B being non trivial finite Subset of F₁() st x in F₂() & B c= F₂() & not x in B & P₁[B] holds
P₁[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 b₁ being FinSequenceSet of REAL holds
( b₁ = REAL n iff for x being object holds
( x in b₁ iff x is Function of (Seg n),REAL ) )

proof end;

end;

:: deftheorem Def3 defines REAL CHAIN_1:def 3 :
for n being Nat
for b₂ being FinSequenceSet of REAL holds
( b₂ = REAL n iff for x being object holds
( x in b₂ 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 b₁ being Function of (Seg d),(bool REAL) st
for i being Element of Seg d holds
( not b₁ . i is trivial & b₁ . i is finite )

proof end;

end;

:: deftheorem Def4 defines Grating CHAIN_1:def 4 :
for d being non zero Nat
for b₂ being Function of (Seg d),(bool REAL) holds
( b₂ is Grating of d iff for i being Element of Seg d holds
( not b₂ . i is trivial & b₂ . i is finite ) );

registration

let d be non zero Nat;

cluster -> V27() for Grating of d;

coherence
for b₁ being Grating of d holds b₁ 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 b₁ being Element of [:REAL,REAL:] ex li, ri being Real st
( b₁ = [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 b₂ being Element of [:REAL,REAL:] holds
( b₂ is Gap of Gi iff ex li, ri being Real st
( b₂ = [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 H₁( 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 b₁ being Cell of d,G ex l, r being Element of REAL d st
( b₁ = 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 b₁, b₂ being Cell of d,G st ex l, r being Element of REAL d st
( b₁ = 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₂ = 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₁ = b₂

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 b₃ being Cell of d,G holds
( b₃ = infinite-cell G iff ex l, r being Element of REAL d st
( b₃ = 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{ F₁() -> non zero Nat, F₂() -> Grating of F₁(), F₃() -> Nat, F₄() -> Chain of F₃(),F₂(), P₁[ set ] } :

P₁[F₄()]

provided

A1: P₁[ 0_ (F₃(),F₂())] and
A2: for A being Cell of F₃(),F₂() st A in F₄() holds
P₁[{A}] and
A3: for C1, C2 being Chain of F₃(),F₂() st C1 c= F₄() & C2 c= F₄() & P₁[C1] & P₁[C2] holds
P₁[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 b₁ being Chain of k,G st
( ( k = 0 & card b₁ is even ) or ex k9 being Nat st
( k = k9 + 1 & ex C being Chain of (k9 + 1),G st
( C = b₁ & 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 b₄ being Chain of k,G holds
( b₄ is Cycle of k,G iff ( ( k = 0 & card b₄ is even ) or ex k9 being Nat st
( k = k9 + 1 & ex C being Chain of (k9 + 1),G st
( C = b₄ & 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 b₁ being Chain of k,G holds
( b₁ = del C iff b₁ = 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 b₁ being strict AbGroup st
( the carrier of b₁ = bool (cells (k,G)) & 0. b₁ = 0_ (k,G) & ( for A, B being Element 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₁, b₂ being strict AbGroup st the carrier of b₁ = bool (cells (k,G)) & 0. b₁ = 0_ (k,G) & ( for A, B being Element of b₁
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) & the carrier of b₂ = bool (cells (k,G)) & 0. b₂ = 0_ (k,G) & ( for A, B being Element of b₂
for A9, B9 being Chain of k,G st A = A9 & B = B9 holds
A + B = A9 + B9 ) holds
b₁ = b₂

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 b₄ being strict AbGroup holds
( b₄ = Chains (k,G) iff ( the carrier of b₄ = bool (cells (k,G)) & 0. b₄ = 0_ (k,G) & ( for A, B being Element of 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;

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 b₁ 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₁ . A = del A9

proof end;

uniqueness
for b₁, b₂ 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₁ . 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₂ . A = del A9 ) holds
b₁ = b₂

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 b₄ being Homomorphism of (Chains ((k + 1),G)),(Chains (k,G)) holds
( b₄ = 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₄ . A = del A9 );