Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

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

Back to top