:: On Powers of Cardinals
:: by Grzegorz Bancerek
::
:: Received August 24, 1992
:: Copyright (c) 1992-2016 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, SUBSET_1, ORDINAL1, CARD_1, FUNCT_1, ORDINAL2, TARSKI,
CARD_3, RELAT_1, FINSET_1, XBOOLE_0, ARYTM_3, WELLORD1, WELLORD2,
ORDINAL4, CARD_2, ORDINAL3, ZFMISC_1, FUNCT_2, FUNCOP_1, MCART_1, CARD_5,
MEMBERED, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, MEMBERED, RELAT_1, FUNCT_1, FINSET_1, FUNCT_2, WELLORD1,
WELLORD2, XTUPLE_0, MCART_1, FUNCOP_1, ORDINAL2, ORDINAL3, CARD_2,
CARD_3, ORDINAL4;
constructors WELLORD1, WELLORD2, FUNCOP_1, ORDINAL3, XXREAL_0, NAT_1,
FINSEQ_1, CARD_2, CARD_3, ORDINAL4, RELSET_1, MEMBERED, ORDERS_1,
XREAL_0, XTUPLE_0, NUMBERS;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, FUNCOP_1, ORDINAL2, ORDINAL3,
NAT_1, CARD_1, CARD_3, ORDINAL4, MEMBERED, FINSET_1, CARD_2, XTUPLE_0,
XCMPLX_0;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin :: Results of [(30),AXIOMS].
reserve k,n,m for Nat,
A,B,C for Ordinal,
X for set,
x,y,z for object;
begin :: Infinity, alephs and cofinality
reserve f,g,h,fx for Function,
K,M,N for Cardinal,
phi,psi for
Ordinal-Sequence;
theorem :: CARD_5:1
nextcard card X = nextcard X;
theorem :: CARD_5:2
y in Union f iff ex x st x in dom f & y in f.x;
theorem :: CARD_5:3
aleph A is infinite;
theorem :: CARD_5:4
M is infinite implies ex A st M = aleph A;
registration
let phi;
cluster Union phi -> ordinal;
end;
theorem :: CARD_5:5
X c= A implies ex phi st phi = canonical_isomorphism_of(RelIncl
order_type_of RelIncl X, RelIncl X) & phi is increasing & dom phi =
order_type_of RelIncl X & rng phi = X;
theorem :: CARD_5:6
X c= A implies sup X is_cofinal_with order_type_of RelIncl X;
theorem :: CARD_5:7
X c= A implies card X = card order_type_of RelIncl X;
theorem :: CARD_5:8
ex B st B c= card A & A is_cofinal_with B;
theorem :: CARD_5:9
ex M st M c= card A & A is_cofinal_with M & for B st A
is_cofinal_with B holds M c= B;
theorem :: CARD_5:10
rng phi = rng psi & phi is increasing & psi is increasing implies phi
= psi;
theorem :: CARD_5:11
phi is increasing implies phi is one-to-one;
theorem :: CARD_5:12
(phi^psi)|(dom phi) = phi;
theorem :: CARD_5:13
X <> {} implies card { Y where Y is Subset of X: card Y in M } c= M*`
exp(card X,M);
theorem :: CARD_5:14
M in exp(2,M);
registration
cluster infinite for Cardinal;
end;
registration
cluster infinite -> non empty for set;
end;
definition
mode Aleph is infinite Cardinal;
let M;
func cf M -> Cardinal means
:: CARD_5:def 1
M is_cofinal_with it & for N st M
is_cofinal_with N holds it c= N;
let N;
func N-powerfunc_of M -> Cardinal-Function means
:: CARD_5:def 2
(for x holds x in
dom it iff x in M & x is Cardinal) & for K st K in M holds it.K = exp(K,N);
end;
registration
let A;
cluster aleph A -> infinite;
end;
begin :: Arithmetics of alephs
reserve a,b for Aleph;
::$CT
theorem :: CARD_5:16
a <> 0 & a <> 1 & a <> 2 & a <> card n & card n in a & omega c= a;
theorem :: CARD_5:17
a c= M or a in M implies M is Aleph;
theorem :: CARD_5:18
a c= M or a in M implies a +` M = M & M +` a = M & a *` M = M &
M *` a = M;
theorem :: CARD_5:19
a +` a = a & a *` a = a;
theorem :: CARD_5:20
M c= exp(M,a);
theorem :: CARD_5:21
union a = a;
registration
let a,M;
cluster a +` M -> infinite;
end;
registration
let M,a;
cluster M +` a -> infinite;
end;
registration
let a,b;
cluster a *` b -> infinite;
cluster exp(a,b) -> infinite;
end;
begin :: Regular alephs
definition
let IT be Aleph;
attr IT is regular means
:: CARD_5:def 3
cf IT = IT;
end;
notation
let IT be Aleph;
antonym IT is irregular for IT is regular;
end;
registration
let a;
cluster nextcard a -> infinite;
end;
theorem :: CARD_5:22
cf omega = omega;
theorem :: CARD_5:23
cf nextcard a = nextcard a;
theorem :: CARD_5:24
omega c= cf a;
theorem :: CARD_5:25
cf 0 = 0 & cf card (n+1) = 1;
theorem :: CARD_5:26
X c= M & card X in cf M implies sup X in M & union X in M;
theorem :: CARD_5:27
dom phi = M & rng phi c= N & M in cf N implies sup phi in N &
Union phi in N;
registration
let a;
cluster cf a -> infinite;
end;
theorem :: CARD_5:28
cf a in a implies a is limit_cardinal;
theorem :: CARD_5:29
cf a in a implies ex xi being Ordinal-Sequence st dom xi = cf a
& rng xi c= a & xi is increasing & a = sup xi & xi is Cardinal-Function & not 0
in rng xi;
theorem :: CARD_5:30
omega is regular & nextcard a is regular;
begin :: Infinite powers
reserve a,b for Aleph;
theorem :: CARD_5:31
a c= b implies exp(a,b) = exp(2,b);
theorem :: CARD_5:32
exp(nextcard a,b) = exp(a,b) *` nextcard a;
theorem :: CARD_5:33
Sum (b-powerfunc_of a) c= exp(a,b);
theorem :: CARD_5:34
a is limit_cardinal & b in cf a implies exp(a,b) = Sum (b-powerfunc_of
a);
theorem :: CARD_5:35
cf a c= b & b in a implies exp(a,b) = exp(Sum (b-powerfunc_of a), cf a);
reserve O for Ordinal,
F for Subset of omega;
theorem :: CARD_5:36
for X being finite set st X c= O holds order_type_of RelIncl X =
card X;
theorem :: CARD_5:37
{x} c= O implies order_type_of RelIncl {x} = 1;
theorem :: CARD_5:38
{x} c= O implies canonical_isomorphism_of (RelIncl order_type_of
RelIncl {x}, RelIncl {x}) = 0 .--> x;
registration
let O be Ordinal, X be Subset of O, n be set;
cluster canonical_isomorphism_of (RelIncl order_type_of RelIncl X,RelIncl X)
.n -> ordinal;
end;
registration
let X be natural-membered set, n be set;
cluster canonical_isomorphism_of
(RelIncl order_type_of RelIncl X,RelIncl X).n -> natural;
end;
theorem :: CARD_5:39
card F c= order_type_of RelIncl F;