:: Epsilon Numbers and Cantor Normal Form
:: by Grzegorz Bancerek
::
:: Received October 20, 2009
:: Copyright (c) 2009-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 NUMBERS, ORDINAL1, ORDINAL2, TARSKI, MATROID0, XBOOLE_0, CARD_1,
FINSET_1, AFINSQ_1, ORDINAL4, RELAT_1, FUNCT_1, VALUED_0, CARD_3,
SUBSET_1, ARYTM_3, NAT_1, XXREAL_0, NEWTON, ORDINAL3, FINSEQ_1, ORDINAL5;
notations XBOOLE_0, TARSKI, RELAT_1, FUNCT_1, SUBSET_1, FINSET_1, ORDINAL1,
XCMPLX_0, NAT_1, XXREAL_0, NEWTON, ORDINAL2, AFINSQ_1, ORDINAL3,
ORDINAL4, CARD_1, CARD_3, NUMBERS;
constructors NEWTON, NAT_1, AFINSQ_1, ORDINAL3, CARD_3, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, NAT_1, XREAL_0, ORDINAL2,
ORDINAL4, CARD_1, CARD_5, CARD_LAR, NEWTON, AFINSQ_1, FINSET_1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
begin :: Preliminaries
reserve a,b,c,d,e for Ordinal, m,n for Nat,
f for Ordinal-Sequence,
x for object;
theorem :: ORDINAL5:1
a c= succ b implies a c= b or a = succ b;
registration
cluster omega -> limit_ordinal;
cluster -> Ordinal-yielding for empty set;
end;
registration
cluster non empty finite for Sequence;
end;
registration
let f be Sequence;
let g be non empty Sequence;
cluster f^g -> non empty;
cluster g^f -> non empty;
end;
reserve S,S1,S2 for Sequence;
theorem :: ORDINAL5:2
dom S = a+^b implies ex S1,S2 st S = S1^S2 & dom S1 = a & dom S2 = b;
theorem :: ORDINAL5:3
rng S1 c= rng(S1^S2) & rng S2 c= rng(S1^S2);
theorem :: ORDINAL5:4
S1^S2 is Ordinal-yielding implies
S1 is Ordinal-yielding & S2 is Ordinal-yielding;
definition
let f be Sequence;
attr f is decreasing means
:: ORDINAL5:def 1
for a,b st a in b & b in dom f holds f.b in f.a;
attr f is non-decreasing means
:: ORDINAL5:def 2
for a,b 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 st a in b & b in dom f holds f.b c= f.a;
end;
registration
cluster increasing -> non-decreasing for Ordinal-Sequence;
cluster decreasing -> non-increasing for Ordinal-Sequence;
end;
theorem :: ORDINAL5:5
for f being Sequence holds f is infinite iff omega c= dom f;
registration
cluster decreasing -> finite for Sequence;
cluster -> decreasing increasing for empty set;
end;
registration
let a;
cluster <%a%> -> Ordinal-yielding;
end;
registration
let a;
cluster <%a%> -> decreasing increasing;
end;
registration
cluster decreasing increasing non-decreasing non-increasing finite
non empty for Ordinal-Sequence;
end;
theorem :: ORDINAL5:6
for f being non-decreasing Ordinal-Sequence
st dom f is non empty holds Union f is_limes_of f;
theorem :: ORDINAL5:7
a in b implies n*^exp(omega, a) in exp(omega, b);
theorem :: ORDINAL5:8
0 in a & (for b st b in dom f holds f.b = exp(a,b)) implies
f is non-decreasing;
theorem :: ORDINAL5:9
a is limit_ordinal & 0 in b implies exp(a,b) is limit_ordinal;
theorem :: ORDINAL5:10
1 in a & (for b st b in dom f holds f.b = exp(a,b)) implies f is increasing;
theorem :: ORDINAL5:11
0 in a & b is non empty limit_ordinal implies
(x in exp(a,b) iff ex c st c in b & x in exp(a,c));
theorem :: ORDINAL5:12
0 in a & exp(a,b) in exp(a,c) implies b in c;
begin :: Tetration (Knuth's arrow notation) of ordinals
definition
let a,b be Ordinal;
func a|^|^b -> Ordinal means
:: 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);
end;
theorem :: ORDINAL5:13
a |^|^ 0 = 1;
theorem :: ORDINAL5:14
a |^|^ succ b = exp(a, a|^|^b);
theorem :: ORDINAL5:15
b <> 0 & b is limit_ordinal implies
for phi being Ordinal-Sequence st dom phi = b &
for c st c in b holds phi.c = a |^|^ c
holds a |^|^ b = lim phi;
theorem :: ORDINAL5:16
a |^|^ 1 = a;
theorem :: ORDINAL5:17
1 |^|^ a = 1;
theorem :: ORDINAL5:18
a |^|^ 2 = exp(a, a);
theorem :: ORDINAL5:19
a |^|^ 3 = exp(a,exp(a, a));
theorem :: ORDINAL5:20
for n being Nat holds 0 |^|^ (2*n) = 1 & 0 |^|^ (2*n+1) = 0;
theorem :: ORDINAL5:21
a c= b & 0 in c implies c |^|^ a c= c |^|^ b;
theorem :: ORDINAL5:22
0 in a & (for b st b in dom f holds f.b = a|^|^b) implies f is non-decreasing
;
theorem :: ORDINAL5:23
0 in a & 0 in b implies a c= a |^|^ b;
theorem :: ORDINAL5:24
1 in a & m < n implies a |^|^ m in a |^|^ n;
:: theorem :: false a |^|^ succ omega = a |^|^ omega for a > 0
:: 1 in c & a in b implies c |^|^ a in c |^|^ b
theorem :: ORDINAL5:25
1 in a & dom f c= omega & (for b st b in dom f holds f.b = a|^|^b)
implies f is increasing;
theorem :: ORDINAL5:26
1 in a & 1 in b implies a in a |^|^ b;
theorem :: ORDINAL5:27
for n,k being Nat holds exp(n,k) = n|^k;
registration
let n,k be Nat;
cluster exp(n,k) -> natural;
end;
registration
let n,k be Nat;
cluster n |^|^ k -> natural;
end;
theorem :: ORDINAL5:28
for n,k being Nat st n > 1 holds n |^|^ k > k;
theorem :: ORDINAL5:29
for n being Nat st n > 1 holds n |^|^ omega = omega;
theorem :: ORDINAL5:30
1 in a implies a |^|^ omega is limit_ordinal;
theorem :: ORDINAL5:31
0 in a implies exp(a, a |^|^ omega) = a |^|^ omega;
theorem :: ORDINAL5:32
0 in a & omega c= b implies a |^|^ b = a |^|^ omega;
begin
scheme :: ORDINAL5:sch 1
CriticalNumber2
{a() -> Ordinal, f() -> Ordinal-Sequence, phi(Ordinal) -> Ordinal}:
a() c= Union f() & phi(Union f()) = Union f() &
for b st a() c= b & phi(b) = b holds Union f() c= b
provided
for a,b st a in b holds phi(a) in phi(b) and
for a st a is non empty limit_ordinal for phi being Ordinal-Sequence
st dom phi = a & for b st b in a holds phi.b = phi(b)
holds phi(a) is_limes_of phi
and
dom f() = omega & f().0 = a() and
for a st a in omega holds f().(succ a) = phi(f().a);
scheme :: ORDINAL5:sch 2
CriticalNumber3{a() -> Ordinal, phi(Ordinal) -> Ordinal}:
ex a st a() in a & phi(a) = a
provided
for a,b st a in b holds phi(a) in phi(b) and
for a st a is non empty limit_ordinal for phi being Ordinal-Sequence
st dom phi = a & for b st b in a holds phi.b = phi(b)
holds phi(a) is_limes_of phi;
begin :: Epsilon numbers
definition
let a be Ordinal;
attr a is epsilon means
:: ORDINAL5:def 5
exp(omega,a) = a;
end;
theorem :: ORDINAL5:33
ex b st a in b & b is epsilon;
registration
cluster epsilon for Ordinal;
end;
definition
let a be Ordinal;
func first_epsilon_greater_than a -> epsilon Ordinal means
:: ORDINAL5:def 6
a in it & for b being epsilon Ordinal st a in b holds it c= b;
end;
theorem :: ORDINAL5:34
a c= b implies first_epsilon_greater_than a c= first_epsilon_greater_than b;
theorem :: ORDINAL5:35
a in b & b in first_epsilon_greater_than a implies
first_epsilon_greater_than b = first_epsilon_greater_than a;
theorem :: ORDINAL5:36
first_epsilon_greater_than 0 = omega |^|^ omega;
theorem :: ORDINAL5:37
for e being epsilon Ordinal holds omega in e;
registration
cluster epsilon -> non empty limit_ordinal for Ordinal;
end;
theorem :: ORDINAL5:38
for e being epsilon Ordinal holds
exp(omega, exp(e, omega)) = exp(e, exp(e, omega));
theorem :: ORDINAL5:39
for e being epsilon Ordinal st 0 in n holds
e |^|^ (n+2) = exp(omega, e |^|^ (n+1));
theorem :: ORDINAL5:40
for e being epsilon Ordinal holds first_epsilon_greater_than e = e |^|^ omega
;
definition
let a be Ordinal;
func epsilon_a -> Ordinal means
:: ORDINAL5:def 7
:: equals omega |^|^ exp(omega, 1+^a); :: wg wikipedii, ale to nie prawda
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);
end;
theorem :: ORDINAL5:41
epsilon_0 = omega |^|^ omega;
theorem :: ORDINAL5:42
epsilon_(succ a) = epsilon_a |^|^ omega;
theorem :: ORDINAL5:43
b <> 0 & b is limit_ordinal implies
for phi being Ordinal-Sequence st dom phi = b &
for c st c in b holds phi.c = epsilon_c
holds epsilon_b = lim phi;
theorem :: ORDINAL5:44
a in b implies epsilon_a in epsilon_b;
theorem :: ORDINAL5:45
for phi being Ordinal-Sequence st
for c st c in dom phi holds phi.c = epsilon_c
holds phi is increasing;
theorem :: ORDINAL5:46
b <> {} & b is limit_ordinal implies
for phi being Ordinal-Sequence st dom phi = b &
for c st c in b holds phi.c = epsilon_c
holds epsilon_b = Union phi;
theorem :: ORDINAL5:47
b is non empty limit_ordinal implies
(x in epsilon_b iff ex c st c in b & x in epsilon_c);
theorem :: ORDINAL5:48
a c= epsilon_a;
theorem :: ORDINAL5:49
for X being non empty set st for x 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;
theorem :: ORDINAL5:50
for X being non empty set st (for x st x in X holds x is epsilon Ordinal) &
for a st a in X holds first_epsilon_greater_than a in X
holds union X is epsilon Ordinal;
registration
let a;
cluster epsilon_a -> epsilon;
end;
::$N The ordinal indexing of epsilon numbers
theorem :: ORDINAL5:51
a is epsilon implies ex b st a = epsilon_b;
begin :: Cantor Normal Form
definition
let A be finite Ordinal-Sequence; :: why finite?
func Sum^ A -> Ordinal means
:: 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;
end;
theorem :: ORDINAL5:52
Sum^ {} = 0;
theorem :: ORDINAL5:53
Sum^ <%a%> = a;
theorem :: ORDINAL5:54
for A being finite Ordinal-Sequence holds Sum^ (A^<%a%>) = (Sum^ A) +^ a;
theorem :: ORDINAL5:55
for A being finite Ordinal-Sequence holds Sum^ (<%a%>^A) = a +^ Sum^ A;
theorem :: ORDINAL5:56
for A being finite Ordinal-Sequence holds A.0 c= Sum^ A;
definition
let a;
attr a is Cantor-component means
:: ORDINAL5:def 9
ex b,n st 0 in Segm n & a = n*^exp(omega,b);
end;
registration
cluster Cantor-component -> non empty for Ordinal;
end;
registration
cluster Cantor-component for Ordinal;
end;
definition
let a,b;
func b-exponent(a) -> Ordinal means
:: ORDINAL5:def 10
exp(b,it) c= a & for c st exp(b,c) c= a holds c c= it if 1 in b & 0 in a
otherwise it = 0;
end;
theorem :: ORDINAL5:57
1 in b implies a in exp(b, succ(b-exponent(a)));
registration
let a, b be Ordinal;
cluster <% a,b %> -> Ordinal-yielding;
let c be Ordinal;
cluster <% a,b,c %> -> Ordinal-yielding;
end;
::: into ORDINAL3 ?
registration
let a be non empty Ordinal, b be Ordinal;
cluster a +^ b -> non empty;
cluster b +^ a -> non empty;
end;
::: into ORDINAL3 ?
registration
let a, b be non empty Ordinal;
cluster b *^ a -> non empty;
end;
::: into ORDINAL4 ?
registration
let A be empty Ordinal, B be non empty Ordinal;
cluster exp(A,B) -> empty;
end;
::: into ORDINAL4 ?
registration
let A be Ordinal, B be empty Ordinal;
cluster exp(A,B) -> non empty;
end;
::: into ORDINAL4 ?
registration
let A be non empty Ordinal, B be Ordinal;
cluster exp(A,B) -> non empty;
end;
theorem :: ORDINAL5:58
for a, b, c being Ordinal
holds 0 in c & c in b implies b -exponent(c*^exp(b,a)) = a;
theorem :: ORDINAL5:59
0 in a & 1 in b & c = b-exponent a implies a div^ exp(b, c) in b;
theorem :: ORDINAL5:60
0 in a & 1 in b & c = b-exponent a implies 0 in a div^ exp(b, c);
theorem :: ORDINAL5:61
b <> 0 implies a mod^ exp(b, c) in exp(b, c);
theorem :: ORDINAL5:62
0 in a implies
ex n,c st a = n*^exp(omega, omega-exponent(a))+^c & 0 in Segm n &
c in exp(omega, omega-exponent(a));
theorem :: ORDINAL5:63
1 in c & c-exponent b in c-exponent a implies b in a;
definition
let A be Ordinal-Sequence;
attr A is Cantor-normal-form means
:: ORDINAL5:def 11
(for a st a in dom A holds A.a is Cantor-component) &
for a,b st a in b & b in dom A holds
omega-exponent(A.b) in omega-exponent(A.a);
end;
registration
cluster empty -> Cantor-normal-form for Ordinal-Sequence;
cluster Cantor-normal-form -> non-empty for Ordinal-Sequence;
cluster Cantor-normal-form -> decreasing for Ordinal-Sequence;
end;
reserve A,B for Cantor-normal-form Ordinal-Sequence;
theorem :: ORDINAL5:64
Sum^ A = 0 implies A = {};
theorem :: ORDINAL5:65
0 in Segm n implies <%n*^exp(omega,b)%> is Cantor-normal-form;
registration
cluster non empty Cantor-normal-form for Ordinal-Sequence;
end;
theorem :: 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;
theorem :: ORDINAL5:67
A <> {} implies ex c being Cantor-component Ordinal, B st A = <%c%>^B;
theorem :: 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;
::$N Existence of Cantor Normal Form for ordinal numbers
theorem :: ORDINAL5:69
ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A;