begin
theorem
theorem
begin
:: deftheorem Def3 defines lim_inf KURATO_0:def 1 :
for X being set
for F being SetSequence of X
for b3 being Subset of X holds
( b3 = lim_inf F iff ex f being SetSequence of X st
( b3 = Union f & ( for n being Element of NAT holds f . n = meet (F ^\ n) ) ) );
:: deftheorem Def4 defines lim_sup KURATO_0:def 2 :
for X being set
for F being SetSequence of X
for b3 being Subset of X holds
( b3 = lim_sup F iff ex f being SetSequence of X st
( b3 = meet f & ( for n being Element of NAT holds f . n = Union (F ^\ n) ) ) );
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem Th10:
theorem Th11:
theorem
theorem
theorem
theorem
theorem
theorem Th17:
theorem Th18:
theorem
theorem
begin
theorem Th21:
:: deftheorem Def5 defines non-ascending KURATO_0:def 3 :
for T being set
for S being SetSequence of T holds
( S is non-ascending iff for i being Element of NAT holds S . (i + 1) c= S . i );
:: deftheorem Def6 defines non-descending KURATO_0:def 4 :
for T being set
for S being SetSequence of T holds
( S is non-descending iff for i being Element of NAT holds S . i c= S . (i + 1) );
theorem Th24:
theorem
theorem
begin
:: deftheorem Def7 defines convergent KURATO_0:def 5 :
for T being set
for S being SetSequence of T holds
( S is convergent iff lim_sup S = lim_inf S );
theorem
theorem