:: Sequences of Ordinal Numbers. Beginnings of Ordinal Arithmetics :: by Grzegorz Bancerek :: :: Received July 18, 1989 :: Copyright (c) 1990-2021 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 ORDINAL1, FUNCT_1, XBOOLE_0, TARSKI, ZFMISC_1, RELAT_1, SETFAM_1, SUBSET_1, FUNCOP_1, ORDINAL2, NAT_1, CARD_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1, FUNCOP_1; constructors SETFAM_1, ORDINAL1, FUNCOP_1; registrations SUBSET_1, FUNCT_1, ORDINAL1, FUNCOP_1; requirements SUBSET, BOOLE, NUMERALS; begin reserve A,A1,A2,B,C,D for Ordinal, X,Y for set, x,y,a,b,c for object, L,L1,L2,L3 for Sequence, f for Function; scheme :: ORDINAL2:sch 1 OrdinalInd { P[Ordinal] } : for A holds P[A] provided P[0] and for A st P[A] holds P[succ A] and for A st A <> 0 & A is limit_ordinal & for B st B in A holds P[B] holds P[A]; theorem :: ORDINAL2:1 A c= B iff succ A c= succ B; theorem :: ORDINAL2:2 union succ A = A; theorem :: ORDINAL2:3 succ A c= bool A; theorem :: ORDINAL2:4 0 is limit_ordinal; theorem :: ORDINAL2:5 union A c= A; definition let L; func last L -> set equals :: ORDINAL2:def 1 L.(union dom L); end; theorem :: ORDINAL2:6 dom L = succ A implies last L = L.A; theorem :: ORDINAL2:7 On X c= X; theorem :: ORDINAL2:8 On A = A; theorem :: ORDINAL2:9 X c= Y implies On X c= On Y; theorem :: ORDINAL2:10 Lim X c= X; theorem :: ORDINAL2:11 X c= Y implies Lim X c= Lim Y; theorem :: ORDINAL2:12 Lim X c= On X; theorem :: ORDINAL2:13 (for x st x in X holds x is Ordinal) implies meet X is Ordinal; registration cluster limit_ordinal for Ordinal; end; definition let X; func inf X -> Ordinal equals :: ORDINAL2:def 2 meet On X; func sup X -> Ordinal means :: ORDINAL2:def 3 On X c= it & for A st On X c= A holds it c= A; end; theorem :: ORDINAL2:14 A in X implies inf X c= A; theorem :: ORDINAL2:15 On X <> 0 & (for A st A in X holds D c= A) implies D c= inf X; theorem :: ORDINAL2:16 A in X & X c= Y implies inf Y c= inf X; theorem :: ORDINAL2:17 A in X implies inf X in X; theorem :: ORDINAL2:18 sup A = A; theorem :: ORDINAL2:19 A in X implies A in sup X; theorem :: ORDINAL2:20 (for A st A in X holds A in D) implies sup X c= D; theorem :: ORDINAL2:21 A in sup X implies ex B st B in X & A c= B; theorem :: ORDINAL2:22 X c= Y implies sup X c= sup Y; theorem :: ORDINAL2:23 sup { A } = succ A; theorem :: ORDINAL2:24 inf X c= sup X; scheme :: ORDINAL2:sch 2 TSLambda { A()->Ordinal, F(Ordinal)->set } : ex L st dom L = A() & for A st A in A() holds L.A = F(A); definition let f; attr f is Ordinal-yielding means :: ORDINAL2:def 4 ex A st rng f c= A; end; registration cluster Ordinal-yielding for Sequence; end; definition mode Ordinal-Sequence is Ordinal-yielding Sequence; end; registration let A; cluster -> Ordinal-yielding for Sequence of A; end; registration let L be Ordinal-Sequence; let A; cluster L|A -> Ordinal-yielding; end; reserve fi,psi for Ordinal-Sequence; theorem :: ORDINAL2:25 A in dom fi implies fi.A is Ordinal; registration let f be Ordinal-Sequence, a be object; cluster f.a -> ordinal; end; scheme :: ORDINAL2:sch 3 OSLambda { A()->Ordinal, F(Ordinal)->Ordinal } : ex fi st dom fi = A() & for A st A in A() holds fi.A = F(A); scheme :: ORDINAL2:sch 4 TSUniq1 { A()->Ordinal, B()->object, C(Ordinal,set)->object, D(Ordinal,Sequence)->object, L1()->Sequence, L2()->Sequence } : L1() = L2() provided dom L1() = A() and 0 in A() implies L1().0 = B() and for A st succ A in A() holds L1().(succ A) = C(A,L1().A) and for A st A in A() & A <> 0 & A is limit_ordinal holds L1().A = D(A, L1()|A) and dom L2() = A() and 0 in A() implies L2().0 = B() and for A st succ A in A() holds L2().(succ A) = C(A,L2().A) and for A st A in A() & A <> 0 & A is limit_ordinal holds L2().A = D(A, L2()|A); scheme :: ORDINAL2:sch 5 TSExist1 { A()->Ordinal, B()->object, C(Ordinal,set)->object, D(Ordinal,Sequence)->object } : ex L st dom L = A() & (0 in A() implies L.0 = B() ) & (for A st succ A in A() holds L.(succ A) = C(A,L.A) ) & for A st A in A() & A <> 0 & A is limit_ordinal holds L.A = D(A,L|A); scheme :: ORDINAL2:sch 6 TSResult { L()->Sequence, F(Ordinal)->set, A()->Ordinal, B()->set, C( Ordinal,set)->set, D(Ordinal,Sequence)->set } : for A st A in dom L() holds L ().A = F(A) provided for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L. 0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) and dom L() = A() and 0 in A() implies L().0 = B() and for A st succ A in A() holds L().(succ A) = C(A,L().A) and for A st A in A() & A <> 0 & A is limit_ordinal holds L().A = D(A,L ()|A); scheme :: ORDINAL2:sch 7 TSDef { A()->Ordinal, B()->set, C(Ordinal,set)->set, D(Ordinal,Sequence)-> set } : (ex x,L st x = last L & dom L = succ A() & L.0 = B() & (for C st succ C in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A() & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) ) & for x1,x2 being set st (ex L st x1 = last L & dom L = succ A() & L.0 = B() & (for C st succ C in succ A() holds L. succ C = C(C,L.C)) & for C st C in succ A() & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) ) & (ex L st x2 = last L & dom L = succ A() & L.0 = B() & (for C st succ C in succ A() holds L.succ C = C(C,L.C)) & for C st C in succ A( ) & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) ) holds x1 = x2; scheme :: ORDINAL2:sch 8 TSResult0 { F(Ordinal)->set, B()->set, C(Ordinal,set)->set, D(Ordinal, Sequence)->set } : F(0) = B() provided for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L. 0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C); scheme :: ORDINAL2:sch 9 TSResultS { B()->set, C(Ordinal,set)->set, D(Ordinal,Sequence)->set, F( Ordinal)->set } : for A holds F(succ A) = C(A,F(A)) provided for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L. 0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C); scheme :: ORDINAL2:sch 10 TSResultL { L()->Sequence, A()->Ordinal, F(Ordinal)->set, B()->set, C( Ordinal,set)->set, D(Ordinal,Sequence)->set } : F(A()) = D(A(),L()) provided for A,x holds x = F(A) iff ex L st x = last L & dom L = succ A & L. 0 = B() & (for C st succ C in succ A holds L.succ C = C(C,L.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds L.C = D(C,L|C) and A() <> 0 & A() is limit_ordinal and dom L() = A() and for A st A in A() holds L().A = F(A); scheme :: ORDINAL2:sch 11 OSExist { A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal ,Sequence)->Ordinal } : ex fi st dom fi = A() & (0 in A() implies fi.0 = B( ) ) & (for A st succ A in A() holds fi.(succ A) = C(A,fi.A) ) & for A st A in A () & A <> 0 & A is limit_ordinal holds fi.A = D(A,fi|A); scheme :: ORDINAL2:sch 12 OSResult { fi()->Ordinal-Sequence, F(Ordinal)->Ordinal, A()->Ordinal, B()-> Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence)->Ordinal } : for A st A in dom fi() holds fi().A = F(A) provided for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) and dom fi() = A() and 0 in A() implies fi().0 = B() and for A st succ A in A() holds fi().(succ A) = C(A,fi().A) and for A st A in A() & A <> 0 & A is limit_ordinal holds fi().A = D(A, fi()|A); scheme :: ORDINAL2:sch 13 OSDef { A()->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal, Sequence)->Ordinal } : (ex A,fi st A = last fi & dom fi = succ A() & fi.0 = B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & for A1,A2 st (ex fi st A1 = last fi & dom fi = succ A() & fi.0 = B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) & (ex fi st A2 = last fi & dom fi = succ A() & fi.0 = B() & (for C st succ C in succ A() holds fi.succ C = C(C,fi.C)) & for C st C in succ A() & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) ) holds A1 = A2; scheme :: ORDINAL2:sch 14 OSResult0 { F(Ordinal)->Ordinal, B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence)->Ordinal } : F(0) = B() provided for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C); scheme :: ORDINAL2:sch 15 OSResultS { B()->Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence) ->Ordinal, F(Ordinal)->Ordinal } : for A holds F(succ A) = C(A,F(A)) provided for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C); scheme :: ORDINAL2:sch 16 OSResultL { fi()->Ordinal-Sequence, A()->Ordinal, F(Ordinal)->Ordinal, B()-> Ordinal, C(Ordinal,Ordinal)->Ordinal, D(Ordinal,Sequence)->Ordinal } : F(A()) = D(A(),fi()) provided for A,B holds B = F(A) iff ex fi st B = last fi & dom fi = succ A & fi.0 = B() & (for C st succ C in succ A holds fi.succ C = C(C,fi.C)) & for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = D(C,fi|C) and A() <> 0 & A() is limit_ordinal and dom fi() = A() and for A st A in A() holds fi().A = F(A); definition let L; func sup L -> Ordinal equals :: ORDINAL2:def 5 sup rng L; func inf L -> Ordinal equals :: ORDINAL2:def 6 inf rng L; end; theorem :: ORDINAL2:26 sup L = sup rng L & inf L = inf rng L; definition let L; func lim_sup L -> Ordinal means :: ORDINAL2:def 7 ex fi st it = inf fi & dom fi = dom L & for A st A in dom L holds fi.A = sup rng (L|(dom L \ A)); func lim_inf L -> Ordinal means :: ORDINAL2:def 8 ex fi st it = sup fi & dom fi = dom L & for A st A in dom L holds fi.A = inf rng (L|(dom L \ A)); end; definition let A,fi; pred A is_limes_of fi means :: ORDINAL2:def 9 ex B st B in dom fi & for C st B c= C & C in dom fi holds fi.C = 0 if A = 0 otherwise for B,C st B in A & A in C ex D st D in dom fi & for E being Ordinal st D c= E & E in dom fi holds B in fi.E & fi.E in C; end; definition let fi; given A such that A is_limes_of fi; func lim fi -> Ordinal means :: ORDINAL2:def 10 it is_limes_of fi; end; definition let A,fi; func lim(A,fi) -> Ordinal equals :: ORDINAL2:def 11 lim(fi|A); end; definition let L be Ordinal-Sequence; attr L is increasing means :: ORDINAL2:def 12 for A,B st A in B & B in dom L holds L.A in L.B; attr L is continuous means :: ORDINAL2:def 13 for A,B st A in dom L & A <> 0 & A is limit_ordinal & B = L.A holds B is_limes_of L|A; end; definition let A,B be Ordinal; func A +^ B -> Ordinal means :: ORDINAL2:def 14 ex fi st it = last fi & dom fi = succ B & fi.0 = A & (for C st succ C in succ B holds fi.succ C = succ(fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = sup(fi|C); end; definition let A,B; func A *^ B -> Ordinal means :: ORDINAL2:def 15 ex fi st it = last fi & dom fi = succ A & fi.0 = 0 & (for C st succ C in succ A holds fi.succ C = (fi.C)+^B) & for C st C in succ A & C <> 0 & C is limit_ordinal holds fi.C = union sup(fi|C); end; registration let O be Ordinal; cluster -> ordinal for Element of O; end; definition let A,B; func exp(A,B) -> Ordinal means :: ORDINAL2:def 16 ex fi st it = last fi & dom fi = succ B & fi.0 = 1 & (for C st succ C in succ B holds fi.succ C = A*^(fi.C)) & for C st C in succ B & C <> 0 & C is limit_ordinal holds fi.C = lim(fi|C); end; theorem :: ORDINAL2:27 A+^0 = A; theorem :: ORDINAL2:28 A+^succ B = succ(A+^B); theorem :: ORDINAL2:29 B <> 0 & B is limit_ordinal implies for fi st dom fi = B & for C st C in B holds fi.C = A+^C holds A+^B = sup fi; theorem :: ORDINAL2:30 0+^A = A; theorem :: ORDINAL2:31 A+^1 = succ A; theorem :: ORDINAL2:32 A in B implies C +^ A in C +^ B; theorem :: ORDINAL2:33 A c= B implies C +^ A c= C +^ B; theorem :: ORDINAL2:34 A c= B implies A +^ C c= B +^ C; theorem :: ORDINAL2:35 0*^A = 0; theorem :: ORDINAL2:36 (succ B)*^A = B*^A +^ A; theorem :: ORDINAL2:37 B <> 0 & B is limit_ordinal implies for fi st dom fi = B & for C st C in B holds fi.C = C*^A holds B*^A = union sup fi; theorem :: ORDINAL2:38 A*^0 = 0; theorem :: ORDINAL2:39 1*^A = A & A*^1 = A; theorem :: ORDINAL2:40 C <> 0 & A in B implies A*^C in B*^C; theorem :: ORDINAL2:41 A c= B implies A*^C c= B*^C; theorem :: ORDINAL2:42 A c= B implies C*^A c= C*^B; theorem :: ORDINAL2:43 exp(A,0) = 1; theorem :: ORDINAL2:44 exp(A,succ B) = A*^exp(A,B); theorem :: ORDINAL2:45 B <> 0 & B is limit_ordinal implies for fi st dom fi = B & for C st C in B holds fi.C = exp(A,C) holds exp(A,B) = lim fi; theorem :: ORDINAL2:46 exp(A,1) = A & exp(1,A) = 1; theorem :: ORDINAL2:47 for A ex B,C st B is limit_ordinal & C is natural & A = B +^ C; :: 2005.05.04, A.T. registration let X be set, o be Ordinal; cluster X --> o -> Ordinal-yielding; end; registration let O be Ordinal, x be object; cluster O --> x -> Sequence-like; end; :: from ZFREFLE1, 2007.03.14, A.T. definition let A,B be Ordinal; pred A is_cofinal_with B means :: ORDINAL2:def 17 ex xi being Ordinal-Sequence st dom xi = B & rng xi c= A & xi is increasing & A = sup xi; reflexivity; end; reserve e,u for set; theorem :: ORDINAL2:48 e in rng psi implies e is Ordinal; theorem :: ORDINAL2:49 rng psi c= sup psi; theorem :: ORDINAL2:50 A is_cofinal_with 0 implies A = 0; :: from ARYTM_3, 2007.10.23, A.T. scheme :: ORDINAL2:sch 17 OmegaInd {a()-> Nat, P[object]}: P[a()] provided P[0] and for a being Nat st P[a] holds P[succ a]; registration let a, b be Nat; cluster a +^ b -> natural; end; :: from AMI_2, 2008.02.14, A.T. registration let x,y be set, a,b be Nat; cluster IFEQ(x,y,a,b) -> natural; end; :: 2010.03.16, A.T. scheme :: ORDINAL2:sch 18 LambdaRecEx{A() -> set,G(set,set) -> set}: ex f being Function st dom f = omega & f.0 = A() & for n being Nat holds f.succ n = G(n,f.n); reserve n for Nat; scheme :: ORDINAL2:sch 19 RecUn{A() -> set, F, G() -> Function, P[set,set,set]}: F() = G() provided dom F() = omega and F().0 = A() and for n holds P[n,F().n,F().(succ n)] and dom G() = omega and G().0 = A() and for n holds P[n,G().n,G().(succ n)] and for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2; scheme :: ORDINAL2:sch 20 LambdaRecUn{A() -> set, F(set,set) -> set, F, G() -> Function}: F() = G() provided dom F() = omega and F().0 = A() and for n holds F().(succ n) = F(n,F().n) and dom G() = omega and G().0 = A() and for n holds G().(succ n) = F(n,G().n);