:: Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received March 1, 1990
:: Copyright (c) 1990-2017 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 ORDINAL2, ORDINAL1, TARSKI, XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1,
SUBSET_1, ORDINAL3, CARD_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1,
ORDINAL2;
constructors SETFAM_1, ORDINAL2, XTUPLE_0;
registrations XBOOLE_0, ORDINAL1, ORDINAL2;
requirements SUBSET, BOOLE, NUMERALS;
begin
reserve fi,psi for Ordinal-Sequence,
A,B,C,D for Ordinal,
X,Y for set,
x,y for object;
theorem :: ORDINAL3:1
X c= succ X;
theorem :: ORDINAL3:2
succ X c= Y implies X c= Y;
theorem :: ORDINAL3:3
A in B iff succ A in succ B;
theorem :: ORDINAL3:4
X c= A implies union X is epsilon-transitive epsilon-connected set;
theorem :: ORDINAL3:5
union On X is epsilon-transitive epsilon-connected set;
theorem :: ORDINAL3:6
X c= A implies On X = X;
theorem :: ORDINAL3:7
On {A} = {A};
theorem :: ORDINAL3:8
A <> {} implies {} in A;
theorem :: ORDINAL3:9
inf A = {};
theorem :: ORDINAL3:10
inf {A} = A;
theorem :: ORDINAL3:11
X c= A implies meet X is Ordinal;
registration
let A,B;
cluster A \/ B -> ordinal;
cluster A /\ B -> ordinal;
end;
theorem :: ORDINAL3:12
A \/ B = A or A \/ B = B;
theorem :: ORDINAL3:13
A /\ B = A or A /\ B = B;
theorem :: ORDINAL3:14
A in 1 implies A = {};
theorem :: ORDINAL3:15
1 = {{}};
theorem :: ORDINAL3:16
A c= 1 implies A = {} or A = 1;
theorem :: ORDINAL3:17
(A c= B or A in B) & C in D implies A+^C in B+^D;
theorem :: ORDINAL3:18
A c= B & C c= D implies A+^C c= B+^D;
theorem :: ORDINAL3:19
A in B & (C c= D & D <> {} or C in D) implies A*^C in B*^D;
theorem :: ORDINAL3:20
A c= B & C c= D implies A*^C c= B*^D;
theorem :: ORDINAL3:21
B+^C = B+^D implies C = D;
theorem :: ORDINAL3:22
B+^C in B+^D implies C in D;
theorem :: ORDINAL3:23
B+^C c= B+^D implies C c= D;
theorem :: ORDINAL3:24
A c= A+^B & B c= A+^B;
theorem :: ORDINAL3:25
A in B implies A in B+^C & A in C+^B;
theorem :: ORDINAL3:26
A+^B = {} implies A = {} & B = {};
theorem :: ORDINAL3:27
A c= B implies ex C st B = A+^C;
theorem :: ORDINAL3:28
A in B implies ex C st B = A+^C & C <> {};
theorem :: ORDINAL3:29
A <> {} & A is limit_ordinal implies B+^A is limit_ordinal;
theorem :: ORDINAL3:30
A+^B+^C = A+^(B+^C);
theorem :: ORDINAL3:31
A*^B = {} implies A = {} or B = {};
theorem :: ORDINAL3:32
A in B & C <> {} implies A in B*^C & A in C*^B;
theorem :: ORDINAL3:33
B*^A = C*^A & A <> {} implies B = C;
theorem :: ORDINAL3:34
B*^A in C*^A implies B in C;
theorem :: ORDINAL3:35
B*^A c= C*^A & A <> {} implies B c= C;
theorem :: ORDINAL3:36
B <> {} implies A c= A*^B & A c= B*^A;
theorem :: ORDINAL3:37
A*^B = 1 implies A = 1 & B = 1;
theorem :: ORDINAL3:38
A in B+^C implies A in B or ex D st D in C & A = B+^D;
definition
let C,fi;
func C+^fi -> Ordinal-Sequence means
:: ORDINAL3:def 1
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 2
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 3
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 4
dom it = dom fi & for A st A in dom fi holds it.A = (fi.A)*^C;
end;
theorem :: ORDINAL3:39
{} <> 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:40
A is limit_ordinal implies A*^B is limit_ordinal;
theorem :: ORDINAL3:41
A in B*^C & B is limit_ordinal implies ex D st D in B & A in D*^ C;
theorem :: ORDINAL3:42
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:43
{} <> dom fi implies sup (C+^fi) = C+^sup fi;
theorem :: ORDINAL3:44
{} <> dom fi & C <> {} & sup fi is limit_ordinal implies sup (fi
*^C) = (sup fi)*^C;
theorem :: ORDINAL3:45
B <> {} implies union(A+^B) = A+^union B;
theorem :: ORDINAL3:46
(A+^B)*^C = A*^C +^ B*^C;
theorem :: ORDINAL3:47
A <> {} implies ex C,D st B = C*^A+^D & D in A;
theorem :: ORDINAL3:48
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:49
1 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:50
(A*^B)*^C = A*^(B*^C);
definition
let A,B;
func A -^ B -> Ordinal means
:: ORDINAL3:def 5
A = B+^it if B c= A otherwise it = {};
func A div^ B -> Ordinal means
:: ORDINAL3:def 6
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 7
A-^(A div^ B)*^B;
end;
theorem :: ORDINAL3:51
A in B implies B = A+^(B-^A);
theorem :: ORDINAL3:52
A+^B-^A = B;
theorem :: ORDINAL3:53
A in B & (C c= A or C in A) implies A-^C in B-^C;
theorem :: ORDINAL3:54
A-^A = {};
theorem :: ORDINAL3:55
A in B implies B-^A <> {} & {} in B-^A;
theorem :: ORDINAL3:56
A-^{} = A & {}-^A = {};
theorem :: ORDINAL3:57
A-^(B+^C) = (A-^B)-^C;
theorem :: ORDINAL3:58
A c= B implies C-^B c= C-^A;
theorem :: ORDINAL3:59
A c= B implies A-^C c= B-^C;
theorem :: ORDINAL3:60
C <> {} & A in B+^C implies A-^B in C;
theorem :: ORDINAL3:61
A+^B in C implies B in C-^A;
theorem :: ORDINAL3:62
A c= B+^(A-^B);
theorem :: ORDINAL3:63
A*^C -^ B*^C = (A-^B)*^C;
theorem :: ORDINAL3:64
(A div^ B)*^B c= A;
theorem :: ORDINAL3:65
A = (A div^ B)*^B+^(A mod^ B);
theorem :: ORDINAL3:66
A = B*^C+^D & D in C implies B = A div^ C & D = A mod^ C;
theorem :: ORDINAL3:67
A in B*^C implies A div^ C in B & A mod^ C in C;
theorem :: ORDINAL3:68
B <> {} implies A*^B div^ B = A;
theorem :: ORDINAL3:69
A*^B mod^ B = {};
theorem :: ORDINAL3:70
{} div^ A = {} & {} mod^ A = {} & A mod^ {} = A;
theorem :: ORDINAL3:71
A div^ 1 = A & A mod^ 1 = {};
begin :: Addenda
:: from ZF_REFLE, 2007.03.13, A.T.
theorem :: ORDINAL3:72
sup X c= succ union On X;
:: from ZFREFLE1, 2007.03.14, A.T.
reserve e,u for set;
theorem :: ORDINAL3:73
succ A is_cofinal_with 1;
:: from ARYTM_3, 2007.10.23, A.T.
theorem :: ORDINAL3:74
for a,b being Ordinal st a+^b is natural holds a in omega & b in omega;
registration
let a, b be natural Ordinal;
cluster a -^ b -> natural;
cluster a *^ b -> natural;
end;
theorem :: ORDINAL3:75
for a,b being Ordinal st a*^b is natural non empty holds a in omega &
b in omega;
definition
let a,b be natural Ordinal;
redefine func a+^b;
commutativity;
end;
definition
let a,b be natural Ordinal;
redefine func a*^b;
commutativity;
end;