ORDINAL5: Epsilon Numbers and Cantor Normal Form

:: Epsilon Numbers and Cantor Normal Form
:: by Grzegorz Bancerek
::
:: Received October 20, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users

begin

theorem Th1: :: ORDINAL5:1

for a, b being ordinal number holds
( not a c= succ b or a c= b or a = succ b )

proof end;

registration

cluster NAT -> limit_ordinal ;

coherence ;

cluster empty -> empty Ordinal-yielding for set ;

coherence

proof end;

end;

registration

cluster Relation-like Function-like non empty T-Sequence-like finite for set ;

existence

proof end;

end;

registration

let f be T-Sequence;
let g be non empty T-Sequence;

cluster f ^ g -> non empty ;

coherence

proof end;

cluster g ^ f -> non empty ;

coherence

proof end;

end;

theorem Th2: :: ORDINAL5:2

for a, b being ordinal number
for S being T-Sequence st dom S = a +^ b holds
ex S1, S2 being T-Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b )

proof end;

theorem Th3: :: ORDINAL5:3

for S1, S2 being T-Sequence holds
( rng S1 c= rng (S1 ^ S2) & rng S2 c= rng (S1 ^ S2) )

proof end;

theorem Th4: :: ORDINAL5:4

for S1, S2 being T-Sequence st S1 ^ S2 is Ordinal-yielding holds
( S1 is Ordinal-yielding & S2 is Ordinal-yielding )

proof end;

definition

let f be T-Sequence;

attr f is decreasing means :: ORDINAL5:def 1
for a, b being ordinal number st a in b & b in dom f holds
f . b in f . a;

attr f is non-decreasing means :Def2: :: ORDINAL5:def 2
for a, b being ordinal number st a in b & b in dom f holds
f . a c= f . b;

attr f is non-increasing means :: ORDINAL5:def 3
for a, b being ordinal number st a in b & b in dom f holds
f . b c= f . a;

end;

:: deftheorem defines decreasing ORDINAL5:def 1 :

:: deftheorem Def2 defines non-decreasing ORDINAL5:def 2 :

:: deftheorem defines non-increasing ORDINAL5:def 3 :

registration

cluster Relation-like Function-like T-Sequence-like Ordinal-yielding increasing -> non-decreasing for set ;

coherence

proof end;

cluster Relation-like Function-like T-Sequence-like Ordinal-yielding decreasing -> non-increasing for set ;

coherence

proof end;

end;

theorem Th5: :: ORDINAL5:5

for f being T-Sequence holds
( f is infinite iff omega c= dom f )

proof end;

registration

cluster Relation-like Function-like T-Sequence-like decreasing -> finite for set ;

coherence

proof end;

cluster empty -> empty increasing decreasing for set ;

coherence

proof end;

end;

registration

let a be ordinal number ;

cluster <%a%> -> Ordinal-yielding ;

coherence

proof end;

end;

registration

let a be ordinal number ;

cluster <%a%> -> increasing decreasing ;

coherence

proof end;

end;

registration

cluster Relation-like Function-like non empty T-Sequence-like finite Ordinal-yielding increasing decreasing non-decreasing non-increasing for set ;

existence

proof end;

end;

theorem Th6: :: ORDINAL5:6

for f being non-decreasing Ordinal-Sequence st not dom f is empty holds
Union f is_limes_of f

proof end;

theorem :: ORDINAL5:7

for a, b being ordinal number
for n being Nat st a in b holds
n *^ (exp (omega,a)) in exp (omega,b)

proof end;

theorem Th8: :: ORDINAL5:8

for a being ordinal number
for f being Ordinal-Sequence st 0 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) holds
f is non-decreasing

proof end;

theorem Th9: :: ORDINAL5:9

for a, b being ordinal number st a is limit_ordinal & 0 in b holds
exp (a,b) is limit_ordinal

proof end;

theorem :: ORDINAL5:10

for a being ordinal number
for f being Ordinal-Sequence st 1 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) holds
f is increasing

proof end;

theorem Th11: :: ORDINAL5:11

for a, b being ordinal number
for x being set st 0 in a & not b is empty & b is limit_ordinal holds
( x in exp (a,b) iff ex c being ordinal number st
( c in b & x in exp (a,c) ) )

proof end;

theorem Th12: :: ORDINAL5:12

for a, b, c being ordinal number st 0 in a & exp (a,b) in exp (a,c) holds
b in c

proof end;

begin

definition

let a, b be Ordinal;

func a |^|^ b -> Ordinal means :Def4: :: ORDINAL5:def 4
ex phi being Ordinal-Sequence st
( it = 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) ) );

correctness

proof end;

end;

:: deftheorem Def4 defines |^|^ ORDINAL5:def 4 :

theorem Th13: :: ORDINAL5:13

for a being ordinal number holds a |^|^ 0 = 1

proof end;

theorem Th14: :: ORDINAL5:14

for a, b being ordinal number holds a |^|^ (succ b) = exp (a,(a |^|^ b))

proof end;

theorem Th15: :: ORDINAL5:15

for b, a being ordinal number st b <> {} & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = a |^|^ c ) holds
a |^|^ b = lim phi

proof end;

theorem Th16: :: ORDINAL5:16

for a being ordinal number holds a |^|^ 1 = a

proof end;

theorem Th17: :: ORDINAL5:17

for a being ordinal number holds 1 |^|^ a = 1

proof end;

theorem Th18: :: ORDINAL5:18

for a being ordinal number holds a |^|^ 2 = exp (a,a)

proof end;

theorem :: ORDINAL5:19

for a being ordinal number holds a |^|^ 3 = exp (a,(exp (a,a)))

proof end;

theorem :: ORDINAL5:20

for n being Nat holds
( 0 |^|^ (2 * n) = 1 & 0 |^|^ ((2 * n) + 1) = 0 )

proof end;

theorem Th21: :: ORDINAL5:21

for a, b, c being ordinal number st a c= b & 0 in c holds
c |^|^ a c= c |^|^ b

proof end;

theorem :: ORDINAL5:22

for a being ordinal number
for f being Ordinal-Sequence st 0 in a & ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) holds
f is non-decreasing

proof end;

theorem Th23: :: ORDINAL5:23

for a, b being ordinal number st 0 in a & 0 in b holds
a c= a |^|^ b

proof end;

theorem Th24: :: ORDINAL5:24

for a being ordinal number
for m, n being Nat st 1 in a & m < n holds
a |^|^ m in a |^|^ n

proof end;

:: theorem :: false a |^|^ succ omega = a |^|^ omega for a > 0
:: 1 in c & a in b implies c |^|^ a in c |^|^ b

theorem Th25: :: ORDINAL5:25

for a being ordinal number
for f being Ordinal-Sequence st 1 in a & dom f c= omega & ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) holds
f is increasing

proof end;

theorem Th26: :: ORDINAL5:26

for a, b being ordinal number st 1 in a & 1 in b holds
a in a |^|^ b

proof end;

theorem Th27: :: ORDINAL5:27

for n, k being Nat holds exp (n,k) = n |^ k

proof end;

registration

let n, k be Nat;

cluster exp (n,k) -> natural ;

coherence

proof end;

end;

registration

let n, k be Nat;

cluster n |^|^ k -> natural ;

coherence

proof end;

end;

theorem Th28: :: ORDINAL5:28

for n, k being Nat st n > 1 holds
n |^|^ k > k

proof end;

theorem :: ORDINAL5:29

for n being Nat st n > 1 holds
n |^|^ omega = omega

proof end;

theorem Th30: :: ORDINAL5:30

for a being ordinal number st 1 in a holds
a |^|^ omega is limit_ordinal

proof end;

theorem Th31: :: ORDINAL5:31

for a being ordinal number st 0 in a holds
exp (a,(a |^|^ omega)) = a |^|^ omega

proof end;

theorem :: ORDINAL5:32

for a, b being ordinal number st 0 in a & omega c= b holds
a |^|^ b = a |^|^ omega

proof end;

begin

Lm1: {} in omega
by ORDINAL1:def 11;

scheme :: ORDINAL5:sch 1
CriticalNumber2{ F₁() -> Ordinal, F₂() -> Ordinal-Sequence, F₃( Ordinal) -> Ordinal } :

( F₁() c= Union F₂() & F₃((Union F₂())) = Union F₂() & ( for b being ordinal number st F₁() c= b & F₃(b) = b holds
Union F₂() c= b ) )

provided

A1: for a, b being ordinal number st a in b holds
F₃(a) in F₃(b) and
A2: for a being ordinal number st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = F₃(b) ) holds
F₃(a) is_limes_of phi and
A3: ( dom F₂() = omega & F₂() . 0 = F₁() ) and
A4: for a being ordinal number st a in omega holds
F₂() . (succ a) = F₃((F₂() . a))

proof end;

scheme :: ORDINAL5:sch 2
CriticalNumber3{ F₁() -> Ordinal, F₂( Ordinal) -> Ordinal } :

ex a being ordinal number st
( F₁() in a & F₂(a) = a )

provided

A1: for a, b being ordinal number st a in b holds
F₂(a) in F₂(b) and
A2: for a being ordinal number st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = F₂(b) ) holds
F₂(a) is_limes_of phi

proof end;

begin

definition

let a be ordinal number ;

attr a is epsilon means :Def5: :: ORDINAL5:def 5
exp (omega,a) = a;

end;

:: deftheorem Def5 defines epsilon ORDINAL5:def 5 :

theorem Th33: :: ORDINAL5:33

for a being ordinal number ex b being ordinal number st
( a in b & b is epsilon )

proof end;

registration

cluster epsilon-transitive epsilon-connected ordinal epsilon for set ;

existence

proof end;

end;

definition

let a be Ordinal;

func first_epsilon_greater_than a -> epsilon Ordinal means :Def6: :: ORDINAL5:def 6
( a in it & ( for b being epsilon Ordinal st a in b holds
it c= b ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines first_epsilon_greater_than ORDINAL5:def 6 :

theorem :: ORDINAL5:34

for a, b being ordinal number st a c= b holds
first_epsilon_greater_than a c= first_epsilon_greater_than b

proof end;

theorem :: ORDINAL5:35

for a, b being ordinal number st a in b & b in first_epsilon_greater_than a holds
first_epsilon_greater_than b = first_epsilon_greater_than a

proof end;

theorem Th36: :: ORDINAL5:36

first_epsilon_greater_than 0 = omega |^|^ omega

proof end;

theorem Th37: :: ORDINAL5:37

for e being epsilon Ordinal holds omega in e

proof end;

registration

cluster ordinal epsilon -> non empty limit_ordinal for set ;

coherence

proof end;

end;

theorem Th38: :: ORDINAL5:38

for e being epsilon Ordinal holds exp (omega,(exp (e,omega))) = exp (e,(exp (e,omega)))

proof end;

theorem Th39: :: ORDINAL5:39

for n being Nat
for e being epsilon Ordinal st 0 in n holds
e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1)))

proof end;

theorem Th40: :: ORDINAL5:40

for e being epsilon Ordinal holds first_epsilon_greater_than e = e |^|^ omega

proof end;

definition

let a be Ordinal;

:: equals omega |^|^ exp(omega, 1+^a); :: wg wikipedii, ale to nie prawda

func epsilon_ a -> Ordinal means :Def7: :: ORDINAL5:def 7
ex phi being Ordinal-Sequence st
( it = 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) ) );

correctness

proof end;

end;

:: deftheorem Def7 defines epsilon_ ORDINAL5:def 7 :

theorem Th41: :: ORDINAL5:41

epsilon_ 0 = omega |^|^ omega

proof end;

theorem Th42: :: ORDINAL5:42

for a being ordinal number holds epsilon_ (succ a) = (epsilon_ a) |^|^ omega

proof end;

theorem Th43: :: ORDINAL5:43

for b being ordinal number st b <> {} & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = lim phi

proof end;

theorem Th44: :: ORDINAL5:44

for a, b being ordinal number st a in b holds
epsilon_ a in epsilon_ b

proof end;

theorem Th45: :: ORDINAL5:45

for phi being Ordinal-Sequence st ( for c being ordinal number st c in dom phi holds
phi . c = epsilon_ c ) holds
phi is increasing

proof end;

theorem Th46: :: ORDINAL5:46

proof end;

theorem Th47: :: ORDINAL5:47

for b being ordinal number
for x being set st not b is empty & b is limit_ordinal holds
( x in epsilon_ b iff ex c being ordinal number st
( c in b & x in epsilon_ c ) )

proof end;

theorem Th48: :: ORDINAL5:48

for a being ordinal number holds a c= epsilon_ a

proof end;

theorem Th49: :: ORDINAL5:49

for X being non empty set st ( for x being set st x in X holds
( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) ) ) holds
union X is epsilon Ordinal

proof end;

theorem Th50: :: ORDINAL5:50

for X being non empty set st ( for x being set st x in X holds
x is epsilon Ordinal ) & ( for a being ordinal number st a in X holds
first_epsilon_greater_than a in X ) holds
union X is epsilon Ordinal

proof end;

registration

let a be ordinal number ;

cluster epsilon_ a -> epsilon ;

coherence

proof end;

end;

The ordinal indexing of epsilon numbers

theorem :: ORDINAL5:51

for a being ordinal number st a is epsilon holds
ex b being ordinal number st a = epsilon_ b

proof end;

begin

definition

let A be finite Ordinal-Sequence;

func Sum^ A -> Ordinal means :Def8: :: ORDINAL5:def 8
ex f being Ordinal-Sequence st
( it = 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) ) );

correctness

proof end;

end;

:: deftheorem Def8 defines Sum^ ORDINAL5:def 8 :

theorem Th52: :: ORDINAL5:52

Sum^ {} = 0

proof end;

theorem Th53: :: ORDINAL5:53

for a being ordinal number holds Sum^ <%a%> = a

proof end;

theorem Th54: :: ORDINAL5:54

for a being ordinal number
for A being finite Ordinal-Sequence holds Sum^ (A ^ <%a%>) = (Sum^ A) +^ a

proof end;

theorem Th55: :: ORDINAL5:55

for a being ordinal number
for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A)

proof end;

theorem Th56: :: ORDINAL5:56

for A being finite Ordinal-Sequence holds A . 0 c= Sum^ A

proof end;

definition

let a be ordinal number ;

attr a is Cantor-component means :Def9: :: ORDINAL5:def 9
ex b being ordinal number ex n being Nat st
( 0 in n & a = n *^ (exp (omega,b)) );

end;

:: deftheorem Def9 defines Cantor-component ORDINAL5:def 9 :

registration

cluster ordinal Cantor-component -> non empty for set ;

coherence

proof end;

end;

registration

cluster epsilon-transitive epsilon-connected ordinal Cantor-component for set ;

existence

proof end;

end;

definition

let a, b be ordinal number ;

func b -exponent a -> Ordinal means :Def10: :: ORDINAL5:def 10
( 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

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def10 defines -exponent ORDINAL5:def 10 :

Lm2: 0 in 1
by NAT_1:44;

theorem Th57: :: ORDINAL5:57

for b, a being ordinal number st 1 in b holds
a in exp (b,(succ (b -exponent a)))

proof end;

theorem Th58: :: ORDINAL5:58

for b, a being ordinal number
for n being Nat st 0 in n & n in b holds
b -exponent (n *^ (exp (b,a))) = a

proof end;

theorem Th59: :: ORDINAL5:59

for a, b, c being ordinal number st 0 in a & 1 in b & c = b -exponent a holds
a div^ (exp (b,c)) in b

proof end;

theorem Th60: :: ORDINAL5:60

for a, b, c being ordinal number st 0 in a & 1 in b & c = b -exponent a holds
0 in a div^ (exp (b,c))

proof end;

theorem Th61: :: ORDINAL5:61

for b, a, c being ordinal number st b <> 0 holds
a mod^ (exp (b,c)) in exp (b,c)

proof end;

theorem Th62: :: ORDINAL5:62

for a being ordinal number st 0 in a holds
ex n being Nat ex c being ordinal number st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in n & c in exp (omega,(omega -exponent a)) )

proof end;

theorem Th63: :: ORDINAL5:63

for c, b, a being ordinal number st 1 in c & c -exponent b in c -exponent a holds
b in a

proof end;

definition

let A be Ordinal-Sequence;

attr A is Cantor-normal-form means :Def11: :: ORDINAL5:def 11
( ( 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) ) );

end;

:: deftheorem Def11 defines Cantor-normal-form ORDINAL5:def 11 :

registration

cluster Relation-like Function-like empty T-Sequence-like Ordinal-yielding -> Cantor-normal-form for set ;

coherence

proof end;

cluster Relation-like Function-like T-Sequence-like Ordinal-yielding Cantor-normal-form -> decreasing for set ;

coherence

proof end;

end;

theorem :: ORDINAL5:64

for A being Cantor-normal-form Ordinal-Sequence st Sum^ A = 0 holds
A = {}

proof end;

theorem Th65: :: ORDINAL5:65

for b being ordinal number
for n being Nat st 0 in n holds
<%(n *^ (exp (omega,b)))%> is Cantor-normal-form

proof end;

registration

cluster Relation-like Function-like non empty T-Sequence-like Ordinal-yielding Cantor-normal-form for set ;

existence

proof end;

end;

theorem Th66: :: ORDINAL5:66

for A, B being Ordinal-Sequence st A ^ B is Cantor-normal-form holds
( A is Cantor-normal-form & B is Cantor-normal-form )

proof end;

theorem :: ORDINAL5:67

for A being Cantor-normal-form Ordinal-Sequence st A <> {} holds
ex c being Cantor-component Ordinal ex B being Cantor-normal-form Ordinal-Sequence st A = <%c%> ^ B

proof end;

theorem Th68: :: ORDINAL5:68

for A being non empty Cantor-normal-form Ordinal-Sequence
for c being Cantor-component Ordinal st omega -exponent (A . 0) in omega -exponent c holds
<%c%> ^ A is Cantor-normal-form

proof end;

Existence of Cantor Normal Form for ordinal numbers

theorem :: ORDINAL5:69

for a being ordinal number ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A

proof end;