environ vocabulary SUPINF_1, ARYTM_1, ARYTM_3, RLVECT_1, BOOLE, ORDINAL2, SEQ_2, FUNCT_1, RELAT_1, LATTICES, CARD_4, FUNCT_4, FUNCOP_1, SUPINF_2; notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, REAL_1, SUPINF_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FUNCT_4, NAT_1, CARD_4; constructors REAL_1, SUPINF_1, NAT_1, CARD_4, FUNCOP_1, FUNCT_4, MEMBERED, XBOOLE_0; clusters SUPINF_1, RELSET_1, FUNCOP_1, FUNCT_1, ARYTM_3, FINSET_1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin :: operations " + "," - " in R_eal numbers definition func 0. -> R_eal equals :: SUPINF_2:def 1 0; end; definition let x,y be R_eal; func x + y -> R_eal means :: SUPINF_2:def 2 ex a,b being Real st x = a & y = b & it = a + b if x in REAL & y in REAL, it = +infty if x = +infty & y <> -infty or y = +infty & x <> -infty, it = -infty if x = -infty & y <> +infty or y = -infty & x <> +infty otherwise it = 0.; commutativity; end; theorem :: SUPINF_2:1 for x,y being R_eal holds for a,b being Real holds (x = a & y = b) implies (x + y = a + b); theorem :: SUPINF_2:2 for x being R_eal holds x in REAL or x = +infty or x = -infty; definition let x be R_eal; func - x -> R_eal means :: SUPINF_2:def 3 ex a being Real st x = a & it = - a if x in REAL, it = -infty if x = +infty otherwise it = +infty; involutiveness; end; definition let x,y be R_eal; func x - y -> R_eal equals :: SUPINF_2:def 4 x + -y; end; theorem :: SUPINF_2:3 for x being R_eal, a being Real st x = a holds - x = - a; theorem :: SUPINF_2:4 - -infty = +infty; theorem :: SUPINF_2:5 for x,y being R_eal holds for a,b being Real holds (x = a & y = b) implies (x - y = a - b); theorem :: SUPINF_2:6 for x being R_eal holds x <> +infty implies +infty - x = +infty & x - +infty = -infty; theorem :: SUPINF_2:7 for x being R_eal holds x <> -infty implies -infty - x = -infty & x - -infty = +infty; theorem :: SUPINF_2:8 for x,s being R_eal holds x + s = +infty implies x = +infty or s = +infty; theorem :: SUPINF_2:9 for x,s being R_eal holds x + s = -infty implies (x = -infty or s = -infty); theorem :: SUPINF_2:10 for x,s being R_eal holds x - s = +infty implies (x = +infty or s = -infty); theorem :: SUPINF_2:11 for x,s being R_eal holds x - s = -infty implies (x = -infty or s = +infty); theorem :: SUPINF_2:12 for x,s being R_eal holds (not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) & x + s in REAL) implies (x in REAL & s in REAL); theorem :: SUPINF_2:13 for x,s being R_eal holds (not ((x = +infty & s = +infty) or (x = -infty & s = -infty)) & x - s in REAL) implies (x in REAL & s in REAL); theorem :: SUPINF_2:14 for x,y,s,t being R_eal holds not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) & not ((y = +infty & t = -infty) or (y = -infty & t = +infty )) & x <=' y & s <=' t implies x + s <=' y + t; theorem :: SUPINF_2:15 for x,y,s,t being R_eal holds not ((x = +infty & t = +infty) or (x = -infty & t = -infty)) & not ((y = +infty & s = +infty) or (y = -infty & s = -infty )) & x <=' y & s <=' t implies x - t <=' y - s; theorem :: SUPINF_2:16 for x,y being R_eal holds x <=' y iff - y <=' - x; theorem :: SUPINF_2:17 for x,y being R_eal holds x <' y iff - y <' - x; theorem :: SUPINF_2:18 for x being R_eal holds x + 0. = x & 0. + x = x; theorem :: SUPINF_2:19 -infty <'0. & 0. <'+infty; theorem :: SUPINF_2:20 for x,y,z being R_eal holds 0. <=' z & 0. <=' x & y = x + z implies x <=' y; theorem :: SUPINF_2:21 for x being R_eal holds x in NAT implies 0. <=' x; :: :: operations " + "," - " in SUBDOMAIN of ExtREAL :: definition let X,Y be non empty Subset of ExtREAL; func X + Y -> Subset of ExtREAL means :: SUPINF_2:def 5 for z being R_eal holds z in it iff ex x,y being R_eal st (x in X & y in Y & z = x + y); end; definition let X,Y be non empty Subset of ExtREAL; cluster X + Y -> non empty; end; definition let X be non empty Subset of ExtREAL; func - X -> Subset of ExtREAL means :: SUPINF_2:def 6 for z being R_eal holds z in it iff ex x being R_eal st (x in X & z = - x); end; definition let X be non empty Subset of ExtREAL; cluster - X -> non empty; end; theorem :: SUPINF_2:22 for X being non empty Subset of ExtREAL holds - (- X) = X; theorem :: SUPINF_2:23 for X being non empty Subset of ExtREAL holds for z being R_eal holds z in X iff - z in - X; theorem :: SUPINF_2:24 for X,Y being non empty Subset of ExtREAL holds X c= Y iff - X c= - Y; theorem :: SUPINF_2:25 for z being R_eal holds z in REAL iff - z in REAL; theorem :: SUPINF_2:26 for X,Y being non empty Subset of ExtREAL holds (not(-infty in X & +infty in Y or +infty in X & -infty in Y) & not(sup X = +infty & sup Y = -infty or sup X = -infty & sup Y = +infty )) implies sup (X + Y) <=' sup X + sup Y; theorem :: SUPINF_2:27 for X,Y being non empty Subset of ExtREAL holds (not(-infty in X & +infty in Y or +infty in X & -infty in Y) & not(inf X = +infty & inf Y = -infty or inf X = -infty & inf Y = +infty )) implies inf X + inf Y <=' inf (X + Y); theorem :: SUPINF_2:28 for X,Y being non empty Subset of ExtREAL holds X is bounded_above & Y is bounded_above implies sup (X + Y) <=' sup X + sup Y; theorem :: SUPINF_2:29 for X,Y being non empty Subset of ExtREAL holds X is bounded_below & Y is bounded_below implies inf X + inf Y <=' inf (X + Y); theorem :: SUPINF_2:30 for X being non empty Subset of ExtREAL holds for a being R_eal holds a is majorant of X iff - a is minorant of - X; theorem :: SUPINF_2:31 for X being non empty Subset of ExtREAL holds for a being R_eal holds a is minorant of X iff - a is majorant of - X; theorem :: SUPINF_2:32 for X being non empty Subset of ExtREAL holds inf(- X) = - sup X; theorem :: SUPINF_2:33 for X be non empty Subset of ExtREAL holds sup(- X) = - inf X; definition let X be non empty set; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; redefine func rng F -> non empty Subset of ExtREAL; end; :: :: sup F and inf F for Function of X,ExtREAL :: definition let X be non empty set; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; func sup F -> R_eal equals :: SUPINF_2:def 7 sup(rng F); end; definition let X be non empty set; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; func inf F -> R_eal equals :: SUPINF_2:def 8 inf(rng F); end; definition let X be non empty set; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; let x be Element of X; redefine func F.x -> R_eal; end; scheme FunctR_ealEx{X()->non empty set,Y()->set,F(set)->set}: ex f being Function of X(),Y() st for x being Element of X() holds f.x = F(x) provided for x being Element of X() holds F(x) in Y(); definition let X be non empty set; let Y,Z be non empty Subset of ExtREAL; let F be Function of X,Y; let G be Function of X,Z; func F + G -> Function of X,Y + Z means :: SUPINF_2:def 9 for x being Element of X holds it.x = F.x + G.x; end; theorem :: SUPINF_2:34 for X being non empty set holds for Y,Z being non empty Subset of ExtREAL holds for F being Function of X,Y for G being Function of X,Z holds rng(F + G) c= rng F + rng G; theorem :: SUPINF_2:35 for X being non empty set holds for Y,Z being non empty Subset of ExtREAL st not(-infty in Y & +infty in Z or +infty in Y & -infty in Z) holds for F being Function of X,Y for G being Function of X,Z st not(sup F = +infty & sup G = -infty or sup F = -infty & sup G = +infty ) holds sup(F + G) <=' sup F + sup G; theorem :: SUPINF_2:36 for X being non empty set holds for Y,Z being non empty Subset of ExtREAL st not(-infty in Y & +infty in Z or +infty in Y & -infty in Z) holds for F being Function of X,Y for G being Function of X,Z st not(inf F = +infty & inf G = -infty or inf F = -infty & inf G = +infty ) holds inf F + inf G <=' inf(F + G); definition let X be non empty set; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; func - F -> Function of X,- Y means :: SUPINF_2:def 10 for x being Element of X holds it.x = - F.x; end; theorem :: SUPINF_2:37 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds rng(- F) = - rng F; theorem :: SUPINF_2:38 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds inf(- F) = - sup F & sup(- F) = - inf F; :: :: Bounded Function of X,ExtREAL :: definition let X be non empty set; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; attr F is bounded_above means :: SUPINF_2:def 11 sup F <'+infty; end; definition let X be non empty set; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; attr F is bounded_below means :: SUPINF_2:def 12 -infty <'inf F; end; definition let X be non empty set; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; attr F is bounded means :: SUPINF_2:def 13 F is bounded_above & F is bounded_below; end; definition let X be non empty set; let Y be non empty Subset of ExtREAL; cluster bounded -> bounded_above bounded_below Function of X, Y; cluster bounded_above bounded_below -> bounded Function of X, Y; end; theorem :: SUPINF_2:39 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds F is bounded iff sup F <'+infty & -infty <'inf F; theorem :: SUPINF_2:40 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds F is bounded_above iff - F is bounded_below; theorem :: SUPINF_2:41 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds F is bounded_below iff - F is bounded_above; theorem :: SUPINF_2:42 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds F is bounded iff - F is bounded; theorem :: SUPINF_2:43 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds for x being Element of X holds -infty <=' F.x & F.x <=' +infty; theorem :: SUPINF_2:44 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds for x being Element of X holds Y c= REAL implies -infty <'F.x & F.x <'+infty; theorem :: SUPINF_2:45 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds for x being Element of X holds inf F <=' F.x & F.x <=' sup F; theorem :: SUPINF_2:46 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds Y c= REAL implies (F is bounded_above iff sup F in REAL); theorem :: SUPINF_2:47 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds Y c= REAL implies (F is bounded_below iff inf F in REAL); theorem :: SUPINF_2:48 for X being non empty set holds for Y being non empty Subset of ExtREAL holds for F being Function of X,Y holds Y c= REAL implies (F is bounded iff inf F in REAL & sup F in REAL); theorem :: SUPINF_2:49 for X being non empty set holds for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds for F1 being Function of X,Y holds for F2 being Function of X,Z holds F1 is bounded_above & F2 is bounded_above implies F1 + F2 is bounded_above; theorem :: SUPINF_2:50 for X being non empty set holds for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds for F1 being Function of X,Y holds for F2 being Function of X,Z holds F1 is bounded_below & F2 is bounded_below implies F1 + F2 is bounded_below; theorem :: SUPINF_2:51 for X being non empty set holds for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds for F1 being Function of X,Y holds for F2 being Function of X,Z holds F1 is bounded & F2 is bounded implies F1 + F2 is bounded; theorem :: SUPINF_2:52 ex F being Function of NAT,ExtREAL st (F is one-to-one & NAT = rng F & rng F is non empty Subset of ExtREAL); :: :: Series of Elements of ExtREAL numbers :: definition let D be non empty set; let IT be Subset of D; redefine attr IT is countable means :: SUPINF_2:def 14 IT is empty or ex F being Function of NAT,D st IT = rng F; synonym IT is denumerable; end; definition cluster denumerable (non empty Subset of ExtREAL); end; definition mode Denum_Set_of_R_EAL is denumerable non empty Subset of ExtREAL; end; definition let IT be set; attr IT is nonnegative means :: SUPINF_2:def 15 for x being R_eal holds x in IT implies 0. <=' x; end; definition cluster nonnegative Denum_Set_of_R_EAL; end; definition mode Pos_Denum_Set_of_R_EAL is nonnegative Denum_Set_of_R_EAL; end; definition let D be Denum_Set_of_R_EAL; mode Num of D -> Function of NAT,ExtREAL means :: SUPINF_2:def 16 D = rng it; end; definition let N be Function of NAT,ExtREAL; let n be Nat; redefine func N.n -> R_eal; end; theorem :: SUPINF_2:53 for D being Denum_Set_of_R_EAL holds for N being Num of D holds ex F being Function of NAT,ExtREAL st F.0 = N.0 & for n being Nat, y being R_eal st y = F.n holds F.(n + 1) = y + N.(n+1); definition let D be Denum_Set_of_R_EAL; let N be Num of D; func Ser(D,N) -> Function of NAT,ExtREAL means :: SUPINF_2:def 17 it.0 = N.0 & for n being Nat holds for y being R_eal st y = it.n holds it.(n + 1) = y + N.(n + 1); end; theorem :: SUPINF_2:54 for D being Pos_Denum_Set_of_R_EAL holds for N being Num of D holds for n being Nat holds 0. <=' N.n; theorem :: SUPINF_2:55 for D being Pos_Denum_Set_of_R_EAL holds for N being Num of D holds for n being Nat holds Ser(D,N).n <=' Ser(D,N).(n + 1) & 0. <=' Ser(D,N).n; theorem :: SUPINF_2:56 for D being Pos_Denum_Set_of_R_EAL holds for N being Num of D holds for n,m being Nat holds Ser(D,N).n <=' Ser(D,N).(n + m); definition let D be Denum_Set_of_R_EAL; mode Set_of_Series of D -> non empty Subset of ExtREAL means :: SUPINF_2:def 18 ex N being Num of D st it = rng Ser(D,N); end; definition let F be Function of NAT,ExtREAL; redefine func rng F -> non empty Subset of ExtREAL; end; definition let D be Pos_Denum_Set_of_R_EAL; let N be Num of D; func SUM(D,N) -> R_eal equals :: SUPINF_2:def 19 sup(rng Ser(D,N)); end; definition let D be Pos_Denum_Set_of_R_EAL; let N be Num of D; pred D is_sumable N means :: SUPINF_2:def 20 SUM(D,N) in REAL; end; theorem :: SUPINF_2:57 for F being Function of NAT,ExtREAL holds rng F is Denum_Set_of_R_EAL; definition let F be Function of NAT,ExtREAL; redefine func rng F -> Denum_Set_of_R_EAL; end; definition let F be Function of NAT,ExtREAL; func Ser(F) -> Function of NAT,ExtREAL means :: SUPINF_2:def 21 for N being Num of rng F st N = F holds it = Ser(rng F,N); end; definition let X be set; let F be Function of X,ExtREAL; attr F is nonnegative means :: SUPINF_2:def 22 rng F is nonnegative; end; definition let F be Function of NAT,ExtREAL; func SUM(F) -> R_eal equals :: SUPINF_2:def 23 sup(rng Ser(F)); end; theorem :: SUPINF_2:58 for X being non empty set for F being Function of X,ExtREAL holds F is nonnegative iff for n being Element of X holds 0. <=' F.n; theorem :: SUPINF_2:59 for F being Function of NAT,ExtREAL holds for n being Nat holds F is nonnegative implies (Ser(F)).n <=' (Ser(F)).(n + 1) & 0. <=' (Ser(F)).n ; theorem :: SUPINF_2:60 for F being Function of NAT,ExtREAL holds F is nonnegative implies for n,m being Nat holds Ser(F).n <=' Ser(F).(n + m); theorem :: SUPINF_2:61 for F1,F2 being Function of NAT,ExtREAL st F1 is nonnegative holds ((for n being Nat holds F1.n <=' F2.n) implies (for n being Nat holds Ser(F1).n <=' Ser(F2).n)); theorem :: SUPINF_2:62 for F1,F2 being Function of NAT,ExtREAL st F1 is nonnegative holds ((for n being Nat holds F1.n <=' F2.n) implies (SUM(F1) <=' SUM(F2))); theorem :: SUPINF_2:63 for F being Function of NAT,ExtREAL holds Ser(F).0 = F.0 & for n being Nat holds for y being R_eal st y = Ser(F).n holds Ser(F).(n + 1) = y + F.(n + 1); theorem :: SUPINF_2:64 for F being Function of NAT,ExtREAL st F is nonnegative holds (ex n being Nat st F.n = +infty) implies SUM(F) = +infty; definition let F be Function of NAT,ExtREAL; attr F is summable means :: SUPINF_2:def 24 SUM(F) in REAL; end; theorem :: SUPINF_2:65 for F being Function of NAT,ExtREAL st F is nonnegative holds ((ex n being Nat st F.n = +infty) implies F is not summable); theorem :: SUPINF_2:66 for F1,F2 being Function of NAT,ExtREAL st F1 is nonnegative holds ((for n being Nat holds F1.n <=' F2.n) implies (F2 is summable implies F1 is summable)); theorem :: SUPINF_2:67 for F being Function of NAT,ExtREAL st F is nonnegative holds for n being Nat st (for r being Nat holds (n <= r implies F.r = 0.)) holds SUM(F) = Ser(F).n; theorem :: SUPINF_2:68 for F being Function of NAT,ExtREAL st (for n being Nat holds F.n in REAL ) holds (for n being Nat holds Ser(F).n in REAL); theorem :: SUPINF_2:69 for F being Function of NAT,ExtREAL st F is nonnegative holds (ex n being Nat st (for k being Nat holds (n <= k implies F.k = 0.)) & (for k being Nat holds (k <= n implies not F.k = +infty))) implies F is summable;