begin
:: deftheorem SUPINF_2:def 1 :
canceled;
theorem
theorem
canceled;
theorem
theorem
canceled;
theorem
for
x,
y being
R_eal for
a,
b being
Real st
x = a &
y = b holds
x - y = a - b
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem SUPINF_2:def 2 :
canceled;
:: deftheorem SUPINF_2:def 3 :
canceled;
:: deftheorem SUPINF_2:def 4 :
canceled;
:: deftheorem Def5 defines + SUPINF_2:def 5 :
:: deftheorem Def6 defines - SUPINF_2:def 6 :
theorem
canceled;
theorem Th22:
theorem Th23:
theorem
theorem
theorem Th26:
theorem Th27:
theorem
theorem
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
:: deftheorem defines sup SUPINF_2:def 7 :
:: deftheorem defines inf SUPINF_2:def 8 :
:: deftheorem Def9 defines + SUPINF_2:def 9 :
theorem Th34:
theorem Th35:
theorem Th36:
:: deftheorem Def10 defines - SUPINF_2:def 10 :
theorem Th37:
theorem Th38:
:: deftheorem Def11 defines bounded_above SUPINF_2:def 11 :
:: deftheorem Def12 defines bounded_below SUPINF_2:def 12 :
:: deftheorem Def13 defines bounded SUPINF_2:def 13 :
theorem
theorem Th40:
theorem Th41:
theorem
theorem
theorem
theorem Th45:
theorem Th46:
theorem Th47:
theorem
theorem Th49:
theorem Th50:
theorem
theorem Th52:
:: deftheorem Def14 defines countable SUPINF_2:def 14 :
:: deftheorem Def15 defines nonnegative SUPINF_2:def 15 :
:: deftheorem Def16 defines Num SUPINF_2:def 16 :
theorem Th53:
:: deftheorem Def17 defines Ser SUPINF_2:def 17 :
theorem Th54:
theorem Th55:
theorem Th56:
:: deftheorem defines Set_of_Series SUPINF_2:def 18 :
Lm1:
for F being Function of NAT ,ExtREAL holds rng F is non empty Subset of ExtREAL
;
:: deftheorem defines SUM SUPINF_2:def 19 :
:: deftheorem defines is_sumable SUPINF_2:def 20 :
theorem Th57:
:: deftheorem Def21 defines Ser SUPINF_2:def 21 :
:: deftheorem Def22 defines nonnegative SUPINF_2:def 22 :
:: deftheorem defines SUM SUPINF_2:def 23 :
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
:: deftheorem Def24 defines summable SUPINF_2:def 24 :
theorem
theorem
theorem Th67:
theorem Th68:
theorem
theorem
theorem