begin
theorem
theorem Th2:
:: deftheorem Def1 defines Filter CARD_FIL:def 1 :
theorem
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem
theorem Th9:
:: deftheorem Def2 defines Ideal CARD_FIL:def 2 :
theorem Th10:
theorem Th11:
:: deftheorem Def3 defines is_multiplicative_with CARD_FIL:def 3 :
:: deftheorem Def4 defines is_additive_with CARD_FIL:def 4 :
theorem Th12:
:: deftheorem Def5 defines uniform CARD_FIL:def 5 :
:: deftheorem Def6 defines principal CARD_FIL:def 6 :
:: deftheorem Def7 defines being_ultrafilter CARD_FIL:def 7 :
:: deftheorem defines Extend_Filter CARD_FIL:def 8 :
theorem Th13:
theorem Th14:
:: deftheorem defines Filters CARD_FIL:def 9 :
theorem Th15:
theorem Th16:
theorem Th17:
:: deftheorem defines Frechet_Filter CARD_FIL:def 10 :
:: deftheorem defines Frechet_Ideal CARD_FIL:def 11 :
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem Th22:
theorem Th23:
begin
theorem Th24:
:: deftheorem Def12 defines GCH CARD_FIL:def 12 :
:: deftheorem Def13 defines inaccessible CARD_FIL:def 13 :
theorem
:: deftheorem Def14 defines strong_limit CARD_FIL:def 14 :
theorem Th26:
theorem Th27:
theorem Th28:
:: deftheorem Def15 defines strongly_inaccessible CARD_FIL:def 15 :
theorem
theorem Th30:
theorem
:: deftheorem Def16 defines measurable CARD_FIL:def 16 :
theorem Th32:
theorem Th33:
:: deftheorem Def17 defines predecessor CARD_FIL:def 17 :
definition
let M be non
limit_cardinal Aleph;
let T be
Inf_Matrix of
(predecessor M),
M,
(bool M);
pred T is_Ulam_Matrix_of M means :
Def18:
( ( for
N1 being
Element of
predecessor M for
K1,
K2 being
Element of
M st
K1 <> K2 holds
(T . N1,K1) /\ (T . N1,K2) is
empty ) & ( for
K1 being
Element of
M for
N1,
N2 being
Element of
predecessor M st
N1 <> N2 holds
(T . N1,K1) /\ (T . N2,K1) is
empty ) & ( for
N1 being
Element of
predecessor M holds
card (M \ (union { (T . N1,K1) where K1 is Element of M : K1 in M } )) c= predecessor M ) & ( for
K1 being
Element of
M holds
card (M \ (union { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M ) );
end;
:: deftheorem Def18 defines is_Ulam_Matrix_of CARD_FIL:def 18 :
for
M being non
limit_cardinal Aleph for
T being
Inf_Matrix of
(predecessor M),
M,
(bool M) holds
(
T is_Ulam_Matrix_of M iff ( ( for
N1 being
Element of
predecessor M for
K1,
K2 being
Element of
M st
K1 <> K2 holds
(T . N1,K1) /\ (T . N1,K2) is
empty ) & ( for
K1 being
Element of
M for
N1,
N2 being
Element of
predecessor M st
N1 <> N2 holds
(T . N1,K1) /\ (T . N2,K1) is
empty ) & ( for
N1 being
Element of
predecessor M holds
card (M \ (union { (T . N1,K1) where K1 is Element of M : K1 in M } )) c= predecessor M ) & ( for
K1 being
Element of
M holds
card (M \ (union { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } )) c= predecessor M ) ) );
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem Th40:
theorem