begin
Lm1:
for r1, r2, s being real number st 0 < s & r1 <= r2 holds
( r1 < r2 + s & r1 - s < r2 )
theorem Th1:
:: deftheorem defines upper_bound RINFSUP1:def 1 :
for seq being Real_Sequence holds upper_bound seq = upper_bound (rng seq);
:: deftheorem defines lower_bound RINFSUP1:def 2 :
for seq being Real_Sequence holds lower_bound seq = lower_bound (rng seq);
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
theorem
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
:: deftheorem Def3 defines nonnegative RINFSUP1:def 3 :
for f being Real_Sequence holds
( f is nonnegative iff for n being Element of NAT holds f . n >= 0 );
theorem Th17:
theorem Th18:
theorem
theorem Th20:
theorem Th21:
theorem
theorem
theorem Th24:
theorem Th25:
theorem
theorem
theorem
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
:: deftheorem Def4 defines inferior_realsequence RINFSUP1:def 4 :
for seq, b2 being Real_Sequence holds
( b2 = inferior_realsequence seq iff for n being Element of NAT
for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds
b2 . n = lower_bound Y );
:: deftheorem Def5 defines superior_realsequence RINFSUP1:def 5 :
for seq, b2 being Real_Sequence holds
( b2 = superior_realsequence seq iff for n being Element of NAT
for Y being Subset of REAL st Y = { (seq . k) where k is Element of NAT : n <= k } holds
b2 . n = upper_bound Y );
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem
Lm2:
for n being Element of NAT
for seq being Real_Sequence st seq is non-decreasing holds
(inferior_realsequence seq) . n = seq . n
theorem
theorem Th67:
theorem Th68:
theorem Th69:
theorem
theorem
Lm3:
for n being Element of NAT
for seq being Real_Sequence st seq is non-increasing holds
(superior_realsequence seq) . n = seq . n
theorem
theorem Th73:
theorem Th74:
theorem Th75:
theorem
theorem Th77:
theorem
theorem
theorem
theorem Th81:
theorem Th82:
:: deftheorem defines lim_sup RINFSUP1:def 6 :
for seq being Real_Sequence holds lim_sup seq = lower_bound (superior_realsequence seq);
:: deftheorem defines lim_inf RINFSUP1:def 7 :
for seq being Real_Sequence holds lim_inf seq = upper_bound (inferior_realsequence seq);
theorem Th83:
theorem Th84:
theorem
theorem Th86:
theorem Th87:
theorem
theorem
theorem Th90:
theorem
theorem Th92:
theorem
theorem
theorem