Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Ordinal Arithmetics

**by****Grzegorz Bancerek**- Received March 1, 1990
- MML identifier: ORDINAL3

- [ Mizar article, MML identifier index ]

environ vocabulary ORDINAL2, ORDINAL1, BOOLE, TARSKI, SETFAM_1, FUNCT_1, RELAT_1, ORDINAL3; notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1, ORDINAL2; constructors SETFAM_1, ORDINAL2, XBOOLE_0; clusters ORDINAL1, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements SUBSET, BOOLE; begin reserve fi,psi for Ordinal-Sequence, A,B,C,D for Ordinal, X,Y for set, x,y for set; theorem :: ORDINAL3:1 X c= succ X; theorem :: ORDINAL3:2 succ X c= Y implies X c= Y; canceled 2; theorem :: ORDINAL3:5 A in B iff succ A in succ B; theorem :: ORDINAL3:6 X c= A implies union X is Ordinal; theorem :: ORDINAL3:7 union On X is Ordinal; theorem :: ORDINAL3:8 X c= A implies On X = X; theorem :: ORDINAL3:9 On {A} = {A}; theorem :: ORDINAL3:10 A <> {} implies {} in A; theorem :: ORDINAL3:11 inf A = {}; theorem :: ORDINAL3:12 inf {A} = A; theorem :: ORDINAL3:13 X c= A implies meet X is Ordinal; definition let A,B; cluster A \/ B -> ordinal; cluster A /\ B -> ordinal; end; canceled; theorem :: ORDINAL3:15 A \/ B = A or A \/ B = B; theorem :: ORDINAL3:16 A /\ B = A or A /\ B = B; theorem :: ORDINAL3:17 A in one implies A = {}; theorem :: ORDINAL3:18 one = {{}}; theorem :: ORDINAL3:19 A c= one implies A = {} or A = one; theorem :: ORDINAL3:20 (A c= B or A in B) & C in D implies A+^C in B+^D; theorem :: ORDINAL3:21 A c= B & C c= D implies A+^C c= B+^D; theorem :: ORDINAL3:22 A in B & (C c= D & D <> {} or C in D) implies A*^C in B*^D; theorem :: ORDINAL3:23 A c= B & C c= D implies A*^C c= B*^D; theorem :: ORDINAL3:24 B+^C = B+^D implies C = D; theorem :: ORDINAL3:25 B+^C in B+^D implies C in D; theorem :: ORDINAL3:26 B+^C c= B+^D implies C c= D; theorem :: ORDINAL3:27 A c= A+^B & B c= A+^B; theorem :: ORDINAL3:28 A in B implies A in B+^C & A in C+^B; theorem :: ORDINAL3:29 A+^B = {} implies A = {} & B = {}; theorem :: ORDINAL3:30 A c= B implies ex C st B = A+^C; theorem :: ORDINAL3:31 A in B implies ex C st B = A+^C & C <> {}; theorem :: ORDINAL3:32 A <> {} & A is_limit_ordinal implies B+^A is_limit_ordinal; theorem :: ORDINAL3:33 A+^B+^C = A+^(B+^C); theorem :: ORDINAL3:34 A*^B = {} implies A = {} or B = {}; theorem :: ORDINAL3:35 A in B & C <> {} implies A in B*^C & A in C*^B; theorem :: ORDINAL3:36 B*^A = C*^A & A <> {} implies B = C; theorem :: ORDINAL3:37 B*^A in C*^A implies B in C; theorem :: ORDINAL3:38 B*^A c= C*^A & A <> {} implies B c= C; theorem :: ORDINAL3:39 B <> {} implies A c= A*^B & A c= B*^A; canceled; theorem :: ORDINAL3:41 A*^B = one implies A = one & B = one; theorem :: ORDINAL3:42 A in B+^C implies A in B or ex D st D in C & A = B+^D; definition let C,fi; canceled; func C+^fi -> Ordinal-Sequence means :: ORDINAL3:def 2 dom it = dom fi & for A st A in dom fi holds it.A = C+^(fi.A); func fi+^C -> Ordinal-Sequence means :: ORDINAL3:def 3 dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)+^C; func C*^fi -> Ordinal-Sequence means :: ORDINAL3:def 4 dom it = dom fi & for A st A in dom fi holds it.A = C*^(fi.A); func fi*^C -> Ordinal-Sequence means :: ORDINAL3:def 5 dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)*^C; end; canceled 4; theorem :: ORDINAL3:47 {} <> dom fi & dom fi = dom psi & (for A,B st A in dom fi & B = fi.A holds psi.A = C+^B) implies sup psi = C+^sup fi; theorem :: ORDINAL3:48 A is_limit_ordinal implies A*^B is_limit_ordinal; theorem :: ORDINAL3:49 A in B*^C & B is_limit_ordinal implies ex D st D in B & A in D*^C; theorem :: ORDINAL3:50 {} <> dom fi & dom fi = dom psi & C <> {} & sup fi is_limit_ordinal & (for A,B st A in dom fi & B = fi.A holds psi.A = B*^C) implies sup psi = (sup fi)*^C; theorem :: ORDINAL3:51 {} <> dom fi implies sup (C+^fi) = C+^sup fi; theorem :: ORDINAL3:52 {} <> dom fi & C <> {} & sup fi is_limit_ordinal implies sup (fi*^C) = (sup fi)*^C; theorem :: ORDINAL3:53 B <> {} implies union(A+^B) = A+^union B; theorem :: ORDINAL3:54 (A+^B)*^C = A*^C +^ B*^C; theorem :: ORDINAL3:55 A <> {} implies ex C,D st B = C*^A+^D & D in A; theorem :: ORDINAL3:56 for C1,D1,C2,D2 being Ordinal st C1*^A+^D1 = C2*^A+^D2 & D1 in A & D2 in A holds C1 = C2 & D1 = D2; theorem :: ORDINAL3:57 one in B & A <> {} & A is_limit_ordinal implies for fi st dom fi = A & for C st C in A holds fi.C = C*^B holds A*^B = sup fi ; theorem :: ORDINAL3:58 (A*^B)*^C = A*^(B*^C); definition let A,B; func A -^ B -> Ordinal means :: ORDINAL3:def 6 A = B+^it if B c= A otherwise it = {}; func A div^ B -> Ordinal means :: ORDINAL3:def 7 ex C st A = it*^B+^C & C in B if B <> {} otherwise it = {}; end; definition let A,B; func A mod^ B -> Ordinal equals :: ORDINAL3:def 8 A-^(A div^ B)*^B; end; canceled; theorem :: ORDINAL3:60 A in B implies B = A+^(B-^A); canceled 4; theorem :: ORDINAL3:65 A+^B-^A = B; theorem :: ORDINAL3:66 A in B & (C c= A or C in A) implies A-^C in B-^C; theorem :: ORDINAL3:67 A-^A = {}; theorem :: ORDINAL3:68 A in B implies B-^A <> {} & {} in B-^A; theorem :: ORDINAL3:69 A-^{} = A & {}-^A = {}; theorem :: ORDINAL3:70 A-^(B+^C) = (A-^B)-^C; theorem :: ORDINAL3:71 A c= B implies C-^B c= C-^A; theorem :: ORDINAL3:72 A c= B implies A-^C c= B-^C; theorem :: ORDINAL3:73 C <> {} & A in B+^C implies A-^B in C; theorem :: ORDINAL3:74 A+^B in C implies B in C-^A; theorem :: ORDINAL3:75 A c= B+^(A-^B); theorem :: ORDINAL3:76 A*^C -^ B*^C = (A-^B)*^C; theorem :: ORDINAL3:77 (A div^ B)*^B c= A; theorem :: ORDINAL3:78 A = (A div^ B)*^B+^(A mod^ B); theorem :: ORDINAL3:79 A = B*^C+^D & D in C implies B = A div^ C & D = A mod^ C; theorem :: ORDINAL3:80 A in B*^C implies A div^ C in B & A mod^ C in C; theorem :: ORDINAL3:81 B <> {} implies A*^B div^ B = A; theorem :: ORDINAL3:82 A*^B mod^ B = {}; theorem :: ORDINAL3:83 {} div^ A = {} & {} mod^ A = {} & A mod^ {} = A; theorem :: ORDINAL3:84 A div^ one = A & A mod^ one = {};

Back to top