begin
:: deftheorem Def1 defines is_unbounded_in CARD_LAR:def 1 :
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_unbounded_in A iff ( X c= A & sup X = A ) );
:: deftheorem Def2 defines is_closed_in CARD_LAR:def 2 :
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_closed_in A iff ( X c= A & ( for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X ) ) );
:: deftheorem Def3 defines is_club_in CARD_LAR:def 3 :
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_club_in A iff ( X is_closed_in A & X is_unbounded_in A ) );
:: deftheorem Def4 defines unbounded CARD_LAR:def 4 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is unbounded iff sup X = A );
:: deftheorem Def5 defines closed CARD_LAR:def 5 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is closed iff for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X );
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
:: deftheorem Def6 defines LBound CARD_LAR:def 6 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A
for B1 being Ordinal st X is unbounded & B1 in A holds
LBound (B1,X) = inf { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } ;
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
:: deftheorem Def7 defines stationary CARD_LAR:def 7 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds
( X is stationary iff for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty );
theorem Th14:
:: deftheorem Def8 defines is_stationary_in CARD_LAR:def 8 :
for A being limit_ordinal infinite Ordinal
for X being set holds
( X is_stationary_in A iff ( X c= A & ( for Y being Subset of A st Y is closed & Y is unbounded holds
not X /\ Y is empty ) ) );
theorem
theorem
:: deftheorem defines limpoints CARD_LAR:def 9 :
for A being limit_ordinal infinite Ordinal
for X being Subset of A holds limpoints X = { B1 where B1 is Element of A : ( not B1 is finite & B1 is limit_ordinal & sup (X /\ B1) = B1 ) } ;
theorem Th17:
theorem
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem
:: deftheorem Def10 defines Mahlo CARD_LAR:def 10 :
for M being non countable Aleph holds
( M is Mahlo iff { N where N is infinite cardinal Element of M : N is regular } is_stationary_in M );
:: deftheorem Def11 defines strongly_Mahlo CARD_LAR:def 11 :
for M being non countable Aleph holds
( M is strongly_Mahlo iff { N where N is infinite cardinal Element of M : N is strongly_inaccessible } is_stationary_in M );
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem
begin
theorem Th33:
theorem Th34:
deffunc H1( Ordinal) -> set = Rank $1;
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem