The abstract of the Mizar article:

Chains on a Grating in Euclidean Space

by

Freek Wiedijk

Received January 27, 2003

MML identifier: CHAIN_1

[ Mizar article, MML identifier index ]

environ

 vocabulary CHAIN_1, FINSEQ_1, RELAT_1, FUNCT_1, FINSET_1, CARD_1, ORDERS_1,
      BOOLE, MATRIX_2, RLVECT_1, WAYBEL25, SUBSET_1, FINSEQ_2, FUNCT_2,
      GRAPH_1, ARYTM_1, MCART_1, VECTSP_1, GROUP_6, CARD_3, GOBOARD5, BINOP_1,
      PRE_TOPC, SQUARE_1, REALSET1, ARYTM, XREAL_0, POLYNOM1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, ORDINAL1, XCMPLX_0,
      XREAL_0, FUNCT_1, REAL_1, EUCLID, FUNCT_2, ABIAN, CARD_1, DOMAIN_1,
      MOD_4, CARD_3, BINOP_1, VECTSP_1, PRE_TOPC, SQUARE_1, NAT_1, NUMBERS,
      FINSET_1, STRUCT_0, FINSEQ_1, FINSEQ_2, RLVECT_1, REALSET1;
 constructors REAL_1, EUCLID, NAT_1, ABIAN, INT_1, DOMAIN_1, MOD_4, SQUARE_1,
      REALSET1, MEMBERED, ORDINAL2, RAT_1;
 clusters FINSET_1, SUBSET_1, RELSET_1, INT_1, ABIAN, FINSEQ_1, VECTSP_1,
      STRUCT_0, AFINSQ_1, REALSET1, FINSEQ_5, TEX_2, NAT_1, MEMBERED;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;


begin :: stuff I could not find in MML

 reserve X,x,y,z for set;
 reserve n,m,k,k',d' for Nat;

theorem :: CHAIN_1:1
 for x,y being real number st x < y ex z being Real st x < z & z < y;

theorem :: CHAIN_1:2
 for x,y being real number ex z being Real st x < z & y < z;

scheme FrSet_1_2 { D()->non empty set, A()->non empty set, P[set,set],
   F(set,set)->Element of D() } :
 { F(x,y) where x,y is Element of A() : P[x,y] } c= D();

:: Subset A -> Subset B

definition let B be set;
           let A be Subset of B;
 redefine func bool A -> Subset of bool B;
end;

definition let X be set;
 mode Subset of X is Element of bool X;
end;

:: non-zero numbers

definition
 let d be real Nat;
 redefine attr d is zero means
:: CHAIN_1:def 1
  not d > 0;
end;

definition
 let d be Nat;
 redefine attr d is zero means
:: CHAIN_1:def 2
  not d >= 1;
end;

definition
 cluster non zero Nat;
end;

 reserve d for non zero Nat;

definition let d;
 cluster Seg d -> non empty;
end;

 reserve i,i0,i1 for Element of Seg d;

:: non trivial sets

definition let X;
 redefine attr X is trivial means
:: CHAIN_1:def 3
  for x,y st x in X & y in X holds x = y;
end;

canceled;

theorem :: CHAIN_1:4
 {x,y} is trivial iff x = y;

definition
 cluster non trivial finite set;
end;

definition
 let X be non trivial set;
 let Y be set;
 cluster X \/ Y -> non trivial;
 cluster Y \/ X -> non trivial;
end;

definition
 cluster REAL -> non trivial;
end;

definition
 let X be non trivial set;
 cluster non trivial finite Subset of X;
end;

theorem :: CHAIN_1:5
 X is trivial & X \/ {y} is non trivial implies ex x st X = {x};

scheme NonEmptyFinite
 { X()->non empty set, A()->non empty finite Subset of X(), P[set] } :
P[A()]
provided
 for x being Element of X() st x in A() holds P[{x}] and
 for x being Element of X(), B being non empty finite Subset of X()
  st x in A() & B c= A() & not x in B & P[B] holds P[B \/ {x}];

scheme NonTrivialFinite
 { X()->non trivial set, A()->non trivial finite Subset of X(), P[set] } :
   P[A()]
provided
 for x,y being Element of X() st x in A() & y in A() & x <> y
  holds P[{x,y}] and
 for x being Element of X(), B being non trivial finite Subset of X()
  st x in A() & B c= A() & not x in B & P[B] holds P[B \/ {x}];

:: sets of cardinality 2

theorem :: CHAIN_1:6
 Card X = 2 iff
 ex x,y st x in X & y in X & x <> y & for z st z in X holds z = x or z = y;

:: cardinality of symmetric difference

definition
 let X,Y be finite set;
 cluster X \+\ Y -> finite;
end;

theorem :: CHAIN_1:7
 (m is even iff n is even) iff m + n is even;

theorem :: CHAIN_1:8
 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;

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

:: elements of REAL d as functions to REAL

definition let n;
 redefine func REAL n means
:: CHAIN_1:def 4
  for x holds x in it iff x is Function of Seg n,REAL;
end;

 reserve l,r,l',r',l'',r'',x,x',l1,r1,l2,r2 for Element of REAL d;
 reserve Gi for non trivial finite Subset of REAL;
 reserve li,ri,li',ri',xi,xi' for Real;

definition let d,x,i;
 redefine func x.i -> Real;
end;

begin :: gratings, cells, chains, cycles

:: gratings

definition let d;
 mode Grating of d -> Function of Seg d,bool REAL means
:: CHAIN_1:def 5
  for i holds it.i is non trivial finite;
end;

 reserve G for Grating of d;

definition let d,G,i;
 redefine func G.i -> non trivial finite Subset of REAL;
end;

theorem :: CHAIN_1:10
 x in product G iff for i holds x.i in G.i;

theorem :: CHAIN_1:11
 product G is finite;

:: gaps

theorem :: CHAIN_1:12
 for X being non empty finite Subset of REAL holds
  ex ri st ri in X & for xi st xi in X holds ri >= xi;

theorem :: CHAIN_1:13
 for X being non empty finite Subset of REAL holds
  ex li st li in X & for xi st xi in X holds li <= xi;

theorem :: CHAIN_1:14
 ex li,ri st li in Gi & ri in Gi &
  li < ri & for xi st xi in Gi holds not (li < xi & xi < ri);

theorem :: CHAIN_1:15
   ex li,ri st li in Gi & ri in Gi &
  ri < li & for xi st xi in Gi holds not (xi < ri or li < xi);

definition let Gi;
 mode Gap of Gi -> Element of [:REAL,REAL:] means
:: CHAIN_1:def 6
  ex li,ri st it = [li,ri] & li in Gi & ri in Gi &
   ((li < ri & for xi st xi in Gi holds not (li < xi & xi < ri)) or
    (ri < li & for xi st xi in Gi holds not (li < xi or xi < ri)));
end;

theorem :: CHAIN_1:16
 [li,ri] is Gap of Gi iff
  li in Gi & ri in Gi &
   ((li < ri & for xi st xi in Gi holds not (li < xi & xi < ri)) or
    (ri < li & for xi st xi in Gi holds not (li < xi or xi < ri)));

theorem :: CHAIN_1:17
   Gi = {li,ri} implies
  ([li',ri'] is Gap of Gi iff li' = li & ri' = ri or li' = ri & ri' = li);

theorem :: CHAIN_1:18
 xi in Gi implies ex ri st [xi,ri] is Gap of Gi;

theorem :: CHAIN_1:19
 xi in Gi implies ex li st [li,xi] is Gap of Gi;

theorem :: CHAIN_1:20
 [li,ri] is Gap of Gi & [li,ri'] is Gap of Gi implies ri = ri';

theorem :: CHAIN_1:21
 [li,ri] is Gap of Gi & [li',ri] is Gap of Gi implies li = li';

theorem :: CHAIN_1:22
 ri < li & [li,ri] is Gap of Gi & ri' < li' & [li',ri'] is Gap of Gi implies
  li = li' & ri = ri';

:: cells, chains

definition let d,l,r;
 func cell(l,r) -> non empty Subset of REAL d equals
:: CHAIN_1:def 7
  { x : (for i holds l.i <= x.i & x.i <= r.i) or
    (ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i)) };
end;

theorem :: CHAIN_1:23
 x in cell(l,r) iff
  ((for i holds l.i <= x.i & x.i <= r.i) or
   (ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i)));

theorem :: CHAIN_1:24
 (for i holds l.i <= r.i) implies
  (x in cell(l,r) iff for i holds l.i <= x.i & x.i <= r.i);

theorem :: CHAIN_1:25
 (ex i st r.i < l.i) implies
  (x in cell(l,r) iff ex i st r.i < l.i & (x.i <= r.i or l.i <= x.i));

theorem :: CHAIN_1:26
 l in cell(l,r) & r in cell(l,r);

theorem :: CHAIN_1:27
 cell(x,x) = {x};

theorem :: CHAIN_1:28
 (for i holds l'.i <= r'.i) implies
  (cell(l,r) c= cell(l',r') iff
    for i holds l'.i <= l.i & l.i <= r.i & r.i <= r'.i);

theorem :: CHAIN_1:29
 (for i holds r.i < l.i) implies
  (cell(l,r) c= cell(l',r') iff
    for i holds r.i <= r'.i & r'.i < l'.i & l'.i <= l.i);

theorem :: CHAIN_1:30
 (for i holds l.i <= r.i) & (for i holds r'.i < l'.i) implies
  (cell(l,r) c= cell(l',r') iff
    ex i st r.i <= r'.i or l'.i <= l.i);

theorem :: CHAIN_1:31
 (for i holds l.i <= r.i) or (for i holds l.i > r.i) implies
  (cell(l,r) = cell(l',r') iff l = l' & r = r');

definition
 let d,G,k;
 assume
  k <= d;
 func cells(k,G) -> finite non empty Subset of bool(REAL d) equals
:: CHAIN_1:def 8
  { cell(l,r) : ((ex X being Subset of Seg d st card X = k &
        for i 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 holds r.i < l.i & [l.i,r.i] is Gap of G.i)) };
end;

theorem :: CHAIN_1:32
 k <= d implies
 for A being Subset of REAL d holds
  A in cells(k,G) iff
  ex l,r st A = cell(l,r) &
   ((ex X being Subset of Seg d st card X = k &
      for i 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 holds r.i < l.i & [l.i,r.i] is Gap of G.i));

theorem :: CHAIN_1:33
 k <= d implies
 (cell(l,r) in cells(k,G) iff
   ((ex X being Subset of Seg d st card X = k &
      for i 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 holds r.i < l.i & [l.i,r.i] is Gap of G.i)));

theorem :: CHAIN_1:34
 k <= d & cell(l,r) in cells(k,G) implies
  (for i holds (l.i < r.i & [l.i,r.i] is Gap of G.i) or
    (l.i = r.i & l.i in G.i)) or
  (for i holds r.i < l.i & [l.i,r.i] is Gap of G.i);

theorem :: CHAIN_1:35
 k <= d & cell(l,r) in cells(k,G) implies
  for i holds l.i in G.i & r.i in G.i;

theorem :: CHAIN_1:36
   k <= d & cell(l,r) in cells(k,G) implies
  (for i holds l.i <= r.i) or (for i holds r.i < l.i);

theorem :: CHAIN_1:37
 for A being Subset of REAL d holds
  A in cells(0,G) iff ex x st A = cell(x,x) & for i holds x.i in G.i;

theorem :: CHAIN_1:38
 cell(l,r) in cells(0,G) iff l = r & for i holds l.i in G.i;

theorem :: CHAIN_1:39
 for A being Subset of REAL d holds
  A in cells(d,G) iff
  ex l,r st A = cell(l,r) & (for i holds [l.i,r.i] is Gap of G.i) &
   ((for i holds l.i < r.i) or (for i holds r.i < l.i));

theorem :: CHAIN_1:40
 cell(l,r) in cells(d,G) iff
  (for i holds [l.i,r.i] is Gap of G.i) &
   ((for i holds l.i < r.i) or (for i holds r.i < l.i));

theorem :: CHAIN_1:41
 d = d' + 1 implies
 for A being Subset of REAL d holds
  A in cells(d',G) iff
  ex l,r,i0 st A = cell(l,r) & l.i0 = r.i0 & l.i0 in G.i0 &
    for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i;

theorem :: CHAIN_1:42
   d = d' + 1 implies
 (cell(l,r) in cells(d',G) iff
  ex i0 st l.i0 = r.i0 & l.i0 in G.i0 &
    for i st i <> i0 holds l.i < r.i & [l.i,r.i] is Gap of G.i);

theorem :: CHAIN_1:43
 for A being Subset of REAL d holds
  A in cells(1,G) iff
  ex l,r,i0 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 st i <> i0 holds l.i = r.i & l.i in G.i;

theorem :: CHAIN_1:44
   cell(l,r) in cells(1,G) iff
  ex i0 st (l.i0 < r.i0 or d = 1 & r.i0 < l.i0) & [l.i0,r.i0] is Gap of G.i0
&
   for i st i <> i0 holds l.i = r.i & l.i in G.i;

theorem :: CHAIN_1:45
 k <= d & k' <= d & cell(l,r) in cells(k,G) & cell(l',r') in cells(k',G) &
  cell(l,r) c= cell(l',r') implies
 for i holds (l.i = l'.i & r.i = r'.i) or
  (l.i = l'.i & r.i = l'.i) or (l.i = r'.i & r.i = r'.i) or
  (l.i <= r.i & r'.i < l'.i & r'.i <= l.i & r.i <= l'.i);

theorem :: CHAIN_1:46
 k < k' & k' <= d & cell(l,r) in cells(k,G) & cell(l',r') in cells(k',G) &
  cell(l,r) c= cell(l',r') implies
 ex i st (l.i = l'.i & r.i = l'.i) or (l.i = r'.i & r.i = r'.i);

theorem :: CHAIN_1:47
 for X,X' being Subset of Seg d st cell(l,r) c= cell(l',r') &
  (for i 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 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))
 holds X c= X' &
  (for i st i in X or not i in X' holds l.i = l'.i & r.i = r'.i) &
  (for i st not i in X & i in X' holds
    (l.i = l'.i & r.i = l'.i) or (l.i = r'.i & r.i = r'.i));

definition
 let d,G,k;
 mode Cell of k,G is Element of cells(k,G);
end;

definition
 let d,G,k;
 mode Chain of k,G is Subset of cells(k,G);
end;

definition
 let d,G,k;
 func 0_(k,G) -> Chain of k,G equals
:: CHAIN_1:def 9
  {};
end;

definition
 let d,G;
 func Omega(G) -> Chain of d,G equals
:: CHAIN_1:def 10
  cells(d,G);
end;

definition
 let d,G,k;
 let C1,C2 be Chain of k,G;
 redefine func C1 \+\ C2 -> Chain of k,G;
 synonym C1 + C2;
end;

definition
 let d,G;
 func infinite-cell(G) -> Cell of d,G means
:: CHAIN_1:def 11
  ex l,r st it = cell(l,r) & for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;
end;

theorem :: CHAIN_1:48
 cell(l,r) is Cell of d,G implies
  (cell(l,r) = infinite-cell(G) iff for i holds r.i < l.i);

theorem :: CHAIN_1:49
 cell(l,r) = infinite-cell(G) iff
  for i holds r.i < l.i & [l.i,r.i] is Gap of G.i;

scheme ChainInd
  { d()->non zero Nat, G()->Grating of d(), k()->Nat, C()->Chain of k(),G(),
    P[set] } : P[C()]
provided
 P[0_(k(),G())] and
 for A being Cell of k(),G() st A in C() holds P[{A}] and
 for C1,C2 being Chain of k(),G() st C1 c= C() & C2 c= C() &
  P[C1] & P[C2] holds P[C1 + C2];

:: the boundary operator

definition
 let d,G,k;
 let A be Cell of k,G;
 func star A -> Chain of (k + 1),G equals
:: CHAIN_1:def 12
  { B where B is Cell of (k + 1),G : A c= B };
end;

theorem :: CHAIN_1:50
 for A being Cell of k,G, B being Cell of (k + 1),G holds
  B in star A iff A c= B;

definition
 let d,G,k;
 let C be Chain of (k + 1),G;
 func del C -> Chain of k,G equals
:: CHAIN_1:def 13
  { A where A is Cell of k,G : k + 1 <= d & card(star A /\ C) is odd };
 synonym .C;  :: \cdot
end;

definition
 let d,G,k;
 let C be Chain of (k + 1),G, C' be Chain of k,G;
 pred C' bounds C means
:: CHAIN_1:def 14
    C' = del C;
end;

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

theorem :: CHAIN_1:52
 k + 1 > d implies for C being Chain of (k + 1),G holds del C = 0_(k,G);

theorem :: CHAIN_1:53
 k + 1 <= d implies
 for A being Cell of k,G, B being Cell of (k + 1),G holds
  A in del {B} iff A c= B;

:: lemmas

theorem :: CHAIN_1:54
 d = d' + 1 implies
 for A being Cell of d',G holds card(star A) = 2;

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

:: theorems

theorem :: CHAIN_1:56
   Omega(G) = 0_(d,G)` & 0_(d,G) = (Omega(G))`;

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

theorem :: CHAIN_1:58
 for C being Chain of k,G holds C + C = 0_(k,G);

theorem :: CHAIN_1:59
 for C being Chain of d,G holds C` = C + Omega(G);

theorem :: CHAIN_1:60
 del 0_(k + 1,G) = 0_(k,G);

theorem :: CHAIN_1:61
 for G being Grating of d' + 1 holds del Omega(G) = 0_(d',G);

theorem :: CHAIN_1:62
 for C1,C2 being Chain of (k + 1),G holds del(C1 + C2) = del C1 + del C2;

theorem :: CHAIN_1:63
 for G being Grating of d' + 1, C being Chain of (d' + 1),G holds
  del C` = del C;

theorem :: CHAIN_1:64
 for C being Chain of (k + 1 + 1),G holds
  del (del C) = 0_(k,G);

:: cycles

definition
 let d,G,k;
 mode Cycle of k,G -> Chain of k,G means
:: CHAIN_1:def 15
  (k = 0 & card it is even) or
  (ex k' st k = k' + 1 & ex C being Chain of (k' + 1),G st C = it &
    del C = 0_(k',G));
end;

theorem :: CHAIN_1:65
 for C being Chain of (k + 1),G holds
  C is Cycle of (k + 1),G iff del C = 0_(k,G);

theorem :: CHAIN_1:66
   k > d implies for C being Chain of k,G holds C is Cycle of k,G;

theorem :: CHAIN_1:67
 for C being Chain of 0,G holds
  C is Cycle of 0,G iff card C is even;

definition
 let d,G,k;
 let C be Cycle of (k + 1),G;
 redefine func del C equals
:: CHAIN_1:def 16
    0_(k,G);
end;

definition
 let d,G,k;
 redefine func 0_(k,G) -> Cycle of k,G;
end;

definition
 let d,G;
 redefine func Omega(G) -> Cycle of d,G;
end;

definition
 let d,G,k;
 let C1,C2 be Cycle of k,G;
 redefine func C1 \+\ C2 -> Cycle of k,G;
 synonym C1 + C2;
end;

theorem :: CHAIN_1:68
   for C being Cycle of d,G holds C` is Cycle of d,G;

definition
 let d,G,k;
 let C be Chain of (k + 1),G;
 redefine func del C -> Cycle of k,G;
end;

begin :: groups and homomorphisms

definition
 let d,G,k;
 func Chains(k,G) -> strict AbGroup means
:: CHAIN_1:def 17
  (the carrier of it = bool(cells(k,G))) &
  (0.it = 0_(k,G)) &
  (for A,B being Element of it, A',B' being Chain of k,G
    st A = A' & B = B' holds A + B = A' + B');
end;

definition let d,G,k;
 mode GrChain of k,G is Element of Chains(k,G);
end;

theorem :: CHAIN_1:69
  for x being set holds x is Chain of k,G iff x is GrChain of k,G;

definition
 let d,G,k;
 func del(k,G) -> Homomorphism of Chains(k + 1,G),Chains(k,G) means
:: CHAIN_1:def 18
    for A being Element of Chains(k + 1,G), A' being Chain of (k + 1),G
   st A = A' holds it.A = del A';
end;