:: Chains on a Grating in Euclidean Space
:: by Freek Wiedijk
::
:: Received January 27, 2003
:: Copyright (c) 2003-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XREAL_0, ARYTM_3, REAL_1, XXREAL_0, CARD_1,
XBOOLE_0, TARSKI, ZFMISC_1, SETFAM_1, XCMPLX_0, FINSEQ_1, FINSET_1,
ABIAN, FUNCT_1, FINSEQ_2, FUNCT_2, RELAT_1, CARD_3, GOBOARD5, MCART_1,
ARYTM_1, TREES_2, POLYNOM1, WAYBEL25, GRAPH_1, NAT_1, ORDERS_2, STRUCT_0,
VECTSP_1, SUPINF_2, BINOP_1, ALGSTR_0, RLVECT_1, GROUP_6, CHAIN_1,
MSSUBFAM;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1,
XCMPLX_0, XXREAL_0, XREAL_0, FUNCT_1, REAL_1, EUCLID, FUNCT_2, ABIAN,
CARD_1, DOMAIN_1, MOD_4, CARD_3, BINOP_1, VECTSP_1, NAT_1, NUMBERS,
FINSET_1, STRUCT_0, ALGSTR_0, FINSEQ_1, FINSEQ_2, RLVECT_1;
constructors REAL_1, CARD_3, REALSET1, ABIAN, EUCLID, RELSET_1, MOD_4,
BINOP_1;
registrations XBOOLE_0, SUBSET_1, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1,
MEMBERED, FINSEQ_1, ABIAN, STRUCT_0, VECTSP_1, CARD_1, VALUED_0, RELAT_1,
EUCLID, CARD_2, RELSET_1, ORDINAL1;
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,k9,d9 for Nat;
theorem :: CHAIN_1:1
for x,y being Real st x < y
ex z being Element of REAL st x < z & z < y;
theorem :: CHAIN_1:2
for x,y being Real ex z being Element of REAL st x < z & y < z;
scheme :: CHAIN_1:sch 1
FrSet12 { 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-Family of B;
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;
end;
definition
let d be Nat;
redefine attr d is zero means
:: CHAIN_1:def 2
not d >= 1;
end;
reserve d for non zero Nat;
reserve i,i0,i1 for Element of Seg d;
:: non trivial sets
theorem :: CHAIN_1:3
for x,y being object holds {x,y} is trivial iff x = y;
registration
cluster non trivial finite for set;
end;
registration
let X be non trivial set;
let Y be set;
cluster X \/ Y -> non trivial;
cluster Y \/ X -> non trivial;
end;
registration
let X be non trivial set;
cluster non trivial finite for Subset of X;
end;
theorem :: CHAIN_1:4
X is trivial & X \/ {y} is non trivial implies
ex x being object st X = {x};
scheme :: CHAIN_1:sch 2
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 :: CHAIN_1:sch 3
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:5
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;
::$CT
theorem :: 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;
theorem :: 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;
:: elements of REAL d as functions to REAL
definition
let n;
redefine func REAL n means
:: CHAIN_1:def 3
for x being object holds x in it iff x is Function of Seg n,REAL;
end;
reserve l,r,l9,r9,l99,r99,x,x9,l1,r1,l2,r2 for Element of REAL d;
reserve Gi for non trivial finite Subset of REAL;
reserve li,ri,li9,ri9,xi,xi9 for Real;
begin :: gratings, cells, chains, cycles
:: gratings
definition
let d;
mode Grating of d -> Function of Seg d,bool REAL means
:: CHAIN_1:def 4
for i holds it.i is non trivial finite;
end;
reserve G for Grating of d;
registration
let d;
cluster -> finite-yielding for Grating of d;
end;
definition
let d,G,i;
redefine func G.i -> non trivial finite Subset of REAL;
end;
theorem :: CHAIN_1:9
x in product G iff for i holds x.i in G.i;
:: gaps
::$CT
theorem :: CHAIN_1:11
for X being non empty finite Subset of REAL holds
ex ri being Element of REAL st ri in X & for xi st xi in X holds ri >= xi;
theorem :: CHAIN_1:12
for X being non empty finite Subset of REAL holds
ex li being Element of REAL st li in X & for xi st xi in X holds li <= xi;
theorem :: CHAIN_1:13
ex li,ri st li in Gi & ri in Gi &
li < ri & for xi st xi in Gi holds not (li < xi & xi < ri);
::$CT
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 5
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
([li9,ri9] is Gap of Gi iff li9 = li & ri9 = ri or li9 = ri & ri9 = li);
theorem :: CHAIN_1:18
xi in Gi implies ex ri being Element of REAL st [xi,ri] is Gap of Gi;
theorem :: CHAIN_1:19
xi in Gi implies ex li being Element of REAL st [li,xi] is Gap of Gi;
theorem :: CHAIN_1:20
[li,ri] is Gap of Gi & [li,ri9] is Gap of Gi implies ri = ri9;
theorem :: CHAIN_1:21
[li,ri] is Gap of Gi & [li9,ri] is Gap of Gi implies li = li9;
theorem :: CHAIN_1:22
ri < li & [li,ri] is Gap of Gi & ri9 < li9 & [li9,ri9] is Gap of Gi implies
li = li9 & ri = ri9;
:: cells, chains
definition
let d,l,r;
func cell(l,r) -> non empty Subset of REAL d equals
:: CHAIN_1:def 6
{ 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 l9.i <= r9.i) implies (cell(l,r) c= cell(l9,r9) iff
for i holds l9.i <= l.i & l.i <= r.i & r.i <= r9.i);
theorem :: CHAIN_1:29
(for i holds r.i < l.i) implies (cell(l,r) c= cell(l9,r9) iff
for i holds r.i <= r9.i & r9.i < l9.i & l9.i <= l.i);
theorem :: CHAIN_1:30
(for i holds l.i <= r.i) & (for i holds r9.i < l9.i) implies
(cell(l,r) c= cell(l9,r9) iff ex i st r.i <= r9.i or l9.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(l9,r9) iff l = l9 & r = r9);
definition
let d,G,k;
assume
k <= d;
func cells(k,G) -> finite non empty Subset-Family of REAL d equals
:: CHAIN_1:def 7
{ 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 = d9 + 1 implies for A being Subset of REAL d holds A in cells(d9,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 = d9 + 1 implies (cell(l,r) in cells(d9,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 & k9 <= d & cell(l,r) in cells(k,G) & cell(l9,r9) in cells(k9,G) &
cell(l,r) c= cell(l9,r9) implies for i 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;
theorem :: CHAIN_1:46
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) implies
ex i st l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.i;
theorem :: CHAIN_1:47
for X,X9 being Subset of Seg d st cell(l,r) c= cell(l9,r9) &
(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 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 st i in X or not i in X9 holds l.i = l9.i & r.i = r9.i) &
for i st not i in X & i in X9 holds
l.i = l9.i & r.i = l9.i or l.i = r9.i & r.i = r9.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 8
{};
end;
definition
let d,G;
func Omega(G) -> Chain of d,G equals
:: CHAIN_1:def 9
cells(d,G);
end;
notation
let d,G,k;
let C1,C2 be Chain of k,G;
synonym C1 + C2 for C1 \+\ C2;
end;
definition
let d,G,k;
let C1,C2 be Chain of k,G;
redefine func C1 + C2 -> Chain of k,G;
end;
definition
let d,G;
func infinite-cell(G) -> Cell of d,G means
:: CHAIN_1:def 10
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 :: CHAIN_1:sch 4
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 11
{ 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 12
{ A where A is Cell of k,G : k + 1 <= d & card(star A /\ C) is odd };
end;
notation
let d,G,k;
let C be Chain of (k + 1),G;
synonym .C for del C;
end;
definition
let d,G,k;
let C be Chain of (k + 1),G, C9 be Chain of k,G;
pred C9 bounds C means
:: CHAIN_1:def 13
C9 = 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 = d9 + 1 implies for A being Cell of d9,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 d,G holds C` = C + Omega(G);
theorem :: CHAIN_1:59
del 0_(k + 1,G) = 0_(k,G);
theorem :: CHAIN_1:60
for G being Grating of d9 + 1 holds del Omega(G) = 0_(d9,G);
theorem :: CHAIN_1:61
for C1,C2 being Chain of (k + 1),G holds del(C1 + C2) = del C1 + del C2;
theorem :: CHAIN_1:62
for G being Grating of d9 + 1, C being Chain of (d9 + 1),G holds
del C` = del C;
theorem :: CHAIN_1:63
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 14
k = 0 & card it is even or
ex k9 st k = k9 + 1 & ex C being Chain of (k9 + 1),G st C = it &
del C = 0_(k9,G);
end;
theorem :: CHAIN_1:64
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:65
k > d implies for C being Chain of k,G holds C is Cycle of k,G;
theorem :: CHAIN_1:66
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 15
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;
end;
theorem :: CHAIN_1:67
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 16
the carrier of it = bool(cells(k,G)) & 0.it = 0_(k,G) &
for A,B being Element of it, A9,B9 being Chain of k,G
st A = A9 & B = B9 holds A + B = A9 + B9;
end;
definition
let d,G,k;
mode GrChain of k,G is Element of Chains(k,G);
end;
theorem :: CHAIN_1:68
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 17
for A being Element of Chains(k + 1,G), A9 being Chain of (k + 1),G
st A = A9 holds it.A = del A9;
end;