:: Sequences of Ordinal Numbers. Beginnings of Ordinal Arithmetics
:: by Grzegorz Bancerek
::
:: Received July 18, 1989
:: Copyright (c) 1990-2018 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);