begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
:: deftheorem defines decreasing ORDINAL5:def 1 :
for f being T-Sequence holds
( f is decreasing iff for a, b being ordinal number st a in b & b in dom f holds
f . b in f . a );
:: deftheorem Def2 defines non-decreasing ORDINAL5:def 2 :
for f being T-Sequence holds
( f is non-decreasing iff for a, b being ordinal number st a in b & b in dom f holds
f . a c= f . b );
:: deftheorem defines non-increasing ORDINAL5:def 3 :
for f being T-Sequence holds
( f is non-increasing iff for a, b being ordinal number st a in b & b in dom f holds
f . b c= f . a );
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem Th12:
begin
:: deftheorem Def4 defines |^|^ ORDINAL5:def 4 :
for a, b, b3 being Ordinal holds
( b3 = a |^|^ b iff ex phi being Ordinal-Sequence st
( b3 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) );
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem
theorem
theorem Th21:
theorem
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
for
n,
k being
Nat st
n > 1 holds
n |^|^ k > k
theorem
theorem Th30:
theorem Th31:
theorem
begin
Lm1:
{} in omega
by ORDINAL1:def 12;
begin
:: deftheorem Def5 defines epsilon ORDINAL5:def 5 :
for a being ordinal number holds
( a is epsilon iff exp (omega,a) = a );
theorem Th33:
:: deftheorem Def6 defines first_epsilon_greater_than ORDINAL5:def 6 :
for a being Ordinal
for b2 being epsilon Ordinal holds
( b2 = first_epsilon_greater_than a iff ( a in b2 & ( for b being epsilon Ordinal st a in b holds
b2 c= b ) ) );
theorem
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
:: deftheorem Def7 defines epsilon_ ORDINAL5:def 7 :
for a, b2 being Ordinal holds
( b2 = epsilon_ a iff ex phi being Ordinal-Sequence st
( b2 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) );
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem
begin
:: deftheorem Def8 defines Sum^ ORDINAL5:def 8 :
for A being finite Ordinal-Sequence
for b2 being Ordinal holds
( b2 = Sum^ A iff ex f being Ordinal-Sequence st
( b2 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) );
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
:: deftheorem Def9 defines Cantor-component ORDINAL5:def 9 :
for a being ordinal number holds
( a is Cantor-component iff ex b being ordinal number ex n being natural number st
( 0 in n & a = n *^ (exp (omega,b)) ) );
definition
let a,
b be
ordinal number ;
func b -exponent a -> Ordinal means :
Def10:
(
exp (
b,
it)
c= a & ( for
c being
ordinal number st
exp (
b,
c)
c= a holds
c c= it ) )
if ( 1
in b &
0 in a )
otherwise it = 0 ;
existence
( ( 1 in b & 0 in a implies ex b1 being Ordinal st
( exp (b,b1) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b1 ) ) ) & ( ( not 1 in b or not 0 in a ) implies ex b1 being Ordinal st b1 = 0 ) )
uniqueness
for b1, b2 being Ordinal holds
( ( 1 in b & 0 in a & exp (b,b1) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b1 ) & exp (b,b2) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b2 ) implies b1 = b2 ) & ( ( not 1 in b or not 0 in a ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
consistency
for b1 being Ordinal holds verum
;
end;
:: deftheorem Def10 defines -exponent ORDINAL5:def 10 :
for a, b being ordinal number
for b3 being Ordinal holds
( ( 1 in b & 0 in a implies ( b3 = b -exponent a iff ( exp (b,b3) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b3 ) ) ) ) & ( ( not 1 in b or not 0 in a ) implies ( b3 = b -exponent a iff b3 = 0 ) ) );
Lm2:
0 in 1
by NAT_1:45;
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
:: deftheorem Def11 defines Cantor-normal-form ORDINAL5:def 11 :
for A being Ordinal-Sequence holds
( A is Cantor-normal-form iff ( ( for a being ordinal number st a in dom A holds
A . a is Cantor-component ) & ( for a, b being ordinal number st a in b & b in dom A holds
omega -exponent (A . b) in omega -exponent (A . a) ) ) );
theorem
theorem Th65:
theorem Th66:
theorem
theorem Th68:
theorem