:: Series of Positive Real Numbers. Measure Theory
:: by J\'ozef Bia{\l}as
::
:: Received September 27, 1990
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem SUPINF_2:def 1 :
canceled;
theorem :: SUPINF_2:1
theorem :: SUPINF_2:2
canceled;
theorem :: SUPINF_2:3
theorem :: SUPINF_2:4
canceled;
theorem :: SUPINF_2:5
for
x,
y being
R_eal for
a,
b being
Real st
x = a &
y = b holds
x - y = a - b
theorem :: SUPINF_2:6
canceled;
theorem :: SUPINF_2:7
canceled;
theorem :: SUPINF_2:8
canceled;
theorem :: SUPINF_2:9
canceled;
theorem :: SUPINF_2:10
canceled;
theorem :: SUPINF_2:11
canceled;
theorem :: SUPINF_2:12
canceled;
theorem :: SUPINF_2:13
canceled;
theorem :: SUPINF_2:14
canceled;
theorem :: SUPINF_2:15
canceled;
theorem :: SUPINF_2:16
canceled;
theorem :: SUPINF_2:17
canceled;
theorem :: SUPINF_2:18
canceled;
theorem :: SUPINF_2:19
canceled;
theorem :: SUPINF_2:20
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 :: SUPINF_2:21
canceled;
theorem Th22: :: SUPINF_2:22
theorem Th23: :: SUPINF_2:23
theorem :: SUPINF_2:24
theorem :: SUPINF_2:25
theorem Th26: :: SUPINF_2:26
theorem Th27: :: SUPINF_2:27
theorem :: SUPINF_2:28
theorem :: SUPINF_2:29
theorem Th30: :: SUPINF_2:30
theorem Th31: :: SUPINF_2:31
theorem Th32: :: SUPINF_2:32
theorem Th33: :: SUPINF_2:33
:: deftheorem defines sup SUPINF_2:def 7 :
:: deftheorem defines inf SUPINF_2:def 8 :
:: deftheorem Def9 defines + SUPINF_2:def 9 :
theorem Th34: :: SUPINF_2:34
theorem Th35: :: SUPINF_2:35
theorem Th36: :: SUPINF_2:36
:: deftheorem Def10 defines - SUPINF_2:def 10 :
theorem Th37: :: SUPINF_2:37
theorem Th38: :: SUPINF_2:38
:: 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 :: SUPINF_2:39
theorem Th40: :: SUPINF_2:40
theorem Th41: :: SUPINF_2:41
theorem :: SUPINF_2:42
theorem :: SUPINF_2:43
theorem :: SUPINF_2:44
theorem Th45: :: SUPINF_2:45
theorem Th46: :: SUPINF_2:46
theorem Th47: :: SUPINF_2:47
theorem :: SUPINF_2:48
theorem Th49: :: SUPINF_2:49
theorem Th50: :: SUPINF_2:50
theorem :: SUPINF_2:51
theorem Th52: :: SUPINF_2:52
:: 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: :: SUPINF_2:53
:: deftheorem Def17 defines Ser SUPINF_2:def 17 :
theorem Th54: :: SUPINF_2:54
theorem Th55: :: SUPINF_2:55
theorem Th56: :: SUPINF_2:56
:: 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: :: SUPINF_2:57
:: 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: :: SUPINF_2:58
theorem Th59: :: SUPINF_2:59
theorem Th60: :: SUPINF_2:60
theorem Th61: :: SUPINF_2:61
theorem Th62: :: SUPINF_2:62
theorem Th63: :: SUPINF_2:63
theorem Th64: :: SUPINF_2:64
:: deftheorem Def24 defines summable SUPINF_2:def 24 :
theorem :: SUPINF_2:65
theorem :: SUPINF_2:66
theorem Th67: :: SUPINF_2:67
theorem Th68: :: SUPINF_2:68
theorem :: SUPINF_2:69
theorem :: SUPINF_2:70
theorem :: SUPINF_2:71