:: SUPINF_2 semantic presentation begin notation synonym 0. for 0 ; end; definition :: original: 0. redefine func 0. -> R_eal; coherence 0. is R_eal by XXREAL_0:def_1; let x be R_eal; :: original: - redefine func - x -> R_eal; coherence - x is R_eal by XXREAL_0:def_1; let y be R_eal; :: original: + redefine funcx + y -> R_eal; coherence x + y is R_eal by XXREAL_0:def_1; :: original: - redefine funcx - y -> R_eal; coherence x - y is R_eal by XXREAL_0:def_1; end; theorem :: SUPINF_2:1 for x, y being R_eal for a, b being Real st x = a & y = b holds x + y = a + b by XXREAL_3:def_2; theorem :: SUPINF_2:2 for x being R_eal for a being Real st x = a holds - x = - a by XXREAL_3:def_3; theorem :: SUPINF_2:3 for x, y being R_eal for a, b being Real st x = a & y = b holds x - y = a - b proof let x, y be R_eal; ::_thesis: for a, b being Real st x = a & y = b holds x - y = a - b let a, b be Real; ::_thesis: ( x = a & y = b implies x - y = a - b ) assume A1: x = a ; ::_thesis: ( not y = b or x - y = a - b ) assume y = b ; ::_thesis: x - y = a - b then - y = - b by XXREAL_3:def_3; hence x - y = a - b by A1, XXREAL_3:def_2; ::_thesis: verum end; notation let X, Y be Subset of ExtREAL; synonym X + Y for X ++ Y; end; definition let X, Y be Subset of ExtREAL; :: original: + redefine funcX + Y -> Subset of ExtREAL; coherence X + Y is Subset of ExtREAL by MEMBERED:2; end; notation let X be Subset of ExtREAL; synonym - X for -- X; end; definition let X be Subset of ExtREAL; :: original: - redefine func - X -> Subset of ExtREAL; coherence - X is Subset of ExtREAL by MEMBERED:2; end; theorem :: SUPINF_2:4 canceled; theorem :: SUPINF_2:5 for X being non empty Subset of ExtREAL for z being R_eal holds ( z in X iff - z in - X ) by MEMBER_1:1; theorem :: SUPINF_2:6 for X, Y being non empty Subset of ExtREAL holds ( X c= Y iff - X c= - Y ) by MEMBER_1:3; theorem :: SUPINF_2:7 for z being R_eal holds ( z in REAL iff - z in REAL ) proof let z be R_eal; ::_thesis: ( z in REAL iff - z in REAL ) A1: for z being R_eal st z in REAL holds - z in REAL proof let z be R_eal; ::_thesis: ( z in REAL implies - z in REAL ) A2: ( - z in REAL or - z in {-infty,+infty} ) by XBOOLE_0:def_3; assume z in REAL ; ::_thesis: - z in REAL hence - z in REAL by A2, TARSKI:def_2; ::_thesis: verum end; ( - z in REAL implies z in REAL ) proof assume - z in REAL ; ::_thesis: z in REAL then - (- z) in REAL by A1; hence z in REAL ; ::_thesis: verum end; hence ( z in REAL iff - z in REAL ) by A1; ::_thesis: verum end; definition let X be ext-real-membered set ; :: original: inf redefine func inf X -> R_eal; coherence inf X is R_eal by XXREAL_0:def_1; :: original: sup redefine func sup X -> R_eal; coherence sup X is R_eal by XXREAL_0:def_1; end; theorem Th8: :: SUPINF_2:8 for X, Y being non empty Subset of ExtREAL holds sup (X + Y) <= (sup X) + (sup Y) proof let X, Y be non empty Subset of ExtREAL; ::_thesis: sup (X + Y) <= (sup X) + (sup Y) for z being ext-real number st z in X + Y holds z <= (sup X) + (sup Y) proof let z be ext-real number ; ::_thesis: ( z in X + Y implies z <= (sup X) + (sup Y) ) assume z in X + Y ; ::_thesis: z <= (sup X) + (sup Y) then consider x, y being R_eal such that A1: z = x + y and A2: x in X and A3: y in Y ; A4: y <= sup Y by A3, XXREAL_2:4; x <= sup X by A2, XXREAL_2:4; hence z <= (sup X) + (sup Y) by A1, A4, XXREAL_3:36; ::_thesis: verum end; then (sup X) + (sup Y) is UpperBound of X + Y by XXREAL_2:def_1; hence sup (X + Y) <= (sup X) + (sup Y) by XXREAL_2:def_3; ::_thesis: verum end; theorem Th9: :: SUPINF_2:9 for X, Y being non empty Subset of ExtREAL holds (inf X) + (inf Y) <= inf (X + Y) proof let X, Y be non empty Subset of ExtREAL; ::_thesis: (inf X) + (inf Y) <= inf (X + Y) for z being ext-real number st z in X + Y holds (inf X) + (inf Y) <= z proof let z be ext-real number ; ::_thesis: ( z in X + Y implies (inf X) + (inf Y) <= z ) assume z in X + Y ; ::_thesis: (inf X) + (inf Y) <= z then consider x, y being R_eal such that A1: z = x + y and A2: x in X and A3: y in Y ; A4: inf Y <= y by A3, XXREAL_2:3; inf X <= x by A2, XXREAL_2:3; hence (inf X) + (inf Y) <= z by A1, A4, XXREAL_3:36; ::_thesis: verum end; then (inf X) + (inf Y) is LowerBound of X + Y by XXREAL_2:def_2; hence (inf X) + (inf Y) <= inf (X + Y) by XXREAL_2:def_4; ::_thesis: verum end; theorem :: SUPINF_2:10 for X, Y being non empty Subset of ExtREAL st X is bounded_above & Y is bounded_above holds sup (X + Y) <= (sup X) + (sup Y) by Th8; theorem :: SUPINF_2:11 for X, Y being non empty Subset of ExtREAL st X is bounded_below & Y is bounded_below holds (inf X) + (inf Y) <= inf (X + Y) by Th9; theorem Th12: :: SUPINF_2:12 for X being non empty Subset of ExtREAL for a being R_eal holds ( a is UpperBound of X iff - a is LowerBound of - X ) proof let X be non empty Subset of ExtREAL; ::_thesis: for a being R_eal holds ( a is UpperBound of X iff - a is LowerBound of - X ) let a be R_eal; ::_thesis: ( a is UpperBound of X iff - a is LowerBound of - X ) hereby ::_thesis: ( - a is LowerBound of - X implies a is UpperBound of X ) assume A1: a is UpperBound of X ; ::_thesis: - a is LowerBound of - X for x being ext-real number st x in - X holds - a <= x proof let x be ext-real number ; ::_thesis: ( x in - X implies - a <= x ) assume A2: x in - X ; ::_thesis: - a <= x reconsider x = x as Element of ExtREAL by XXREAL_0:def_1; - x in - (- X) by A2; then - x <= a by A1, XXREAL_2:def_1; then - a <= - (- x) by XXREAL_3:38; hence - a <= x ; ::_thesis: verum end; hence - a is LowerBound of - X by XXREAL_2:def_2; ::_thesis: verum end; assume A3: - a is LowerBound of - X ; ::_thesis: a is UpperBound of X for x being ext-real number st x in X holds x <= a proof let x be ext-real number ; ::_thesis: ( x in X implies x <= a ) assume A4: x in X ; ::_thesis: x <= a reconsider x = x as Element of ExtREAL by XXREAL_0:def_1; - x in - X by A4; then - a <= - x by A3, XXREAL_2:def_2; hence x <= a by XXREAL_3:38; ::_thesis: verum end; hence a is UpperBound of X by XXREAL_2:def_1; ::_thesis: verum end; theorem Th13: :: SUPINF_2:13 for X being non empty Subset of ExtREAL for a being R_eal holds ( a is LowerBound of X iff - a is UpperBound of - X ) proof let X be non empty Subset of ExtREAL; ::_thesis: for a being R_eal holds ( a is LowerBound of X iff - a is UpperBound of - X ) let a be R_eal; ::_thesis: ( a is LowerBound of X iff - a is UpperBound of - X ) hereby ::_thesis: ( - a is UpperBound of - X implies a is LowerBound of X ) assume A1: a is LowerBound of X ; ::_thesis: - a is UpperBound of - X for x being ext-real number st x in - X holds x <= - a proof let x be ext-real number ; ::_thesis: ( x in - X implies x <= - a ) assume A2: x in - X ; ::_thesis: x <= - a reconsider x = x as Element of ExtREAL by XXREAL_0:def_1; - x in - (- X) by A2; then a <= - x by A1, XXREAL_2:def_2; then - (- x) <= - a by XXREAL_3:38; hence x <= - a ; ::_thesis: verum end; hence - a is UpperBound of - X by XXREAL_2:def_1; ::_thesis: verum end; assume A3: - a is UpperBound of - X ; ::_thesis: a is LowerBound of X for x being ext-real number st x in X holds a <= x proof let x be ext-real number ; ::_thesis: ( x in X implies a <= x ) assume A4: x in X ; ::_thesis: a <= x reconsider x = x as Element of ExtREAL by XXREAL_0:def_1; - x in - X by A4; then - x <= - a by A3, XXREAL_2:def_1; hence a <= x by XXREAL_3:38; ::_thesis: verum end; hence a is LowerBound of X by XXREAL_2:def_2; ::_thesis: verum end; theorem Th14: :: SUPINF_2:14 for X being non empty Subset of ExtREAL holds inf (- X) = - (sup X) proof let X be non empty Subset of ExtREAL; ::_thesis: inf (- X) = - (sup X) set a = inf (- X); set b = sup X; inf (- X) is LowerBound of - X by XXREAL_2:def_4; then - (inf (- X)) is UpperBound of - (- X) by Th13; then sup X <= - (inf (- X)) by XXREAL_2:def_3; then A1: - (- (inf (- X))) <= - (sup X) by XXREAL_3:38; sup X is UpperBound of X by XXREAL_2:def_3; then - (sup X) is LowerBound of - X by Th12; then - (sup X) <= inf (- X) by XXREAL_2:def_4; hence inf (- X) = - (sup X) by A1, XXREAL_0:1; ::_thesis: verum end; theorem Th15: :: SUPINF_2:15 for X being non empty Subset of ExtREAL holds sup (- X) = - (inf X) proof let X be non empty Subset of ExtREAL; ::_thesis: sup (- X) = - (inf X) set a = sup (- X); set b = inf X; sup (- X) is UpperBound of - X by XXREAL_2:def_3; then - (sup (- X)) is LowerBound of - (- X) by Th12; then - (sup (- X)) <= inf X by XXREAL_2:def_4; then A1: - (inf X) <= - (- (sup (- X))) by XXREAL_3:38; inf X is LowerBound of X by XXREAL_2:def_4; then - (inf X) is UpperBound of - X by Th13; then sup (- X) <= - (inf X) by XXREAL_2:def_3; hence sup (- X) = - (inf X) by A1, XXREAL_0:1; ::_thesis: verum end; definition let X be non empty set ; let Y be non empty Subset of ExtREAL; let F be Function of X,Y; :: original: rng redefine func rng F -> non empty Subset of ExtREAL; coherence rng F is non empty Subset of ExtREAL proof set x = the Element of X; F . the Element of X in rng F by FUNCT_2:4; hence rng F is non empty Subset of ExtREAL by XBOOLE_1:1; ::_thesis: verum end; end; definition let D be ext-real-membered set ; let X be set ; let Y be Subset of D; let F be PartFunc of X,Y; func sup F -> Element of ExtREAL equals :: SUPINF_2:def 1 sup (rng F); coherence sup (rng F) is Element of ExtREAL ; func inf F -> Element of ExtREAL equals :: SUPINF_2:def 2 inf (rng F); coherence inf (rng F) is Element of ExtREAL ; end; :: deftheorem defines sup SUPINF_2:def_1_:_ for D being ext-real-membered set for X being set for Y being Subset of D for F being PartFunc of X,Y holds sup F = sup (rng F); :: deftheorem defines inf SUPINF_2:def_2_:_ for D being ext-real-membered set for X being set for Y being Subset of D for F being PartFunc of X,Y holds inf F = inf (rng F); definition let F be ext-real-valued Function; let x be set ; :: original: . redefine funcF . x -> R_eal; coherence F . x is R_eal by XXREAL_0:def_1; end; 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; funcF + G -> Function of X,(Y + Z) means :Def3: :: SUPINF_2:def 3 for x being Element of X holds it . x = (F . x) + (G . x); existence ex b1 being Function of X,(Y + Z) st for x being Element of X holds b1 . x = (F . x) + (G . x) proof deffunc H1( Element of X) -> R_eal = (F . \$1) + (G . \$1); A1: for x being Element of X holds H1(x) in Y + Z proof let x be Element of X; ::_thesis: H1(x) in Y + Z A2: G . x in Z by FUNCT_2:5; F . x in Y by FUNCT_2:5; hence H1(x) in Y + Z by A2; ::_thesis: verum end; ex H being Function of X,(Y + Z) st for x being Element of X holds H . x = H1(x) from FUNCT_2:sch_8(A1); then consider H being Function of X,(Y + Z) such that A3: for x being Element of X holds H . x = (F . x) + (G . x) ; take H ; ::_thesis: for x being Element of X holds H . x = (F . x) + (G . x) thus for x being Element of X holds H . x = (F . x) + (G . x) by A3; ::_thesis: verum end; uniqueness for b1, b2 being Function of X,(Y + Z) st ( for x being Element of X holds b1 . x = (F . x) + (G . x) ) & ( for x being Element of X holds b2 . x = (F . x) + (G . x) ) holds b1 = b2 proof let H1, H2 be Function of X,(Y + Z); ::_thesis: ( ( for x being Element of X holds H1 . x = (F . x) + (G . x) ) & ( for x being Element of X holds H2 . x = (F . x) + (G . x) ) implies H1 = H2 ) assume that A4: for x being Element of X holds H1 . x = (F . x) + (G . x) and A5: for x being Element of X holds H2 . x = (F . x) + (G . x) ; ::_thesis: H1 = H2 for x being set st x in X holds H1 . x = H2 . x proof let x be set ; ::_thesis: ( x in X implies H1 . x = H2 . x ) assume x in X ; ::_thesis: H1 . x = H2 . x then reconsider x = x as Element of X ; H1 . x = (F . x) + (G . x) by A4 .= H2 . x by A5 ; hence H1 . x = H2 . x ; ::_thesis: verum end; hence H1 = H2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def3 defines + SUPINF_2:def_3_:_ for X being non empty set for Y, Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z for b6 being Function of X,(Y + Z) holds ( b6 = F + G iff for x being Element of X holds b6 . x = (F . x) + (G . x) ); theorem Th16: :: SUPINF_2:16 for X being non empty set for Y, Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G) proof let X be non empty set ; ::_thesis: for Y, Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G) let Y, Z be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G) let F be Function of X,Y; ::_thesis: for G being Function of X,Z holds rng (F + G) c= (rng F) + (rng G) let G be Function of X,Z; ::_thesis: rng (F + G) c= (rng F) + (rng G) A1: for x being set st x in X holds (F + G) . x in (rng F) + (rng G) proof let x be set ; ::_thesis: ( x in X implies (F + G) . x in (rng F) + (rng G) ) assume x in X ; ::_thesis: (F + G) . x in (rng F) + (rng G) then reconsider x = x as Element of X ; reconsider a = F . x, b = G . x as R_eal ; A2: a in rng F by FUNCT_2:4; A3: b in rng G by FUNCT_2:4; (F + G) . x = a + b by Def3; hence (F + G) . x in (rng F) + (rng G) by A2, A3; ::_thesis: verum end; dom (F + G) = X by FUNCT_2:def_1; then F + G is Function of X,((rng F) + (rng G)) by A1, FUNCT_2:3; hence rng (F + G) c= (rng F) + (rng G) by RELAT_1:def_19; ::_thesis: verum end; theorem Th17: :: SUPINF_2:17 for X being non empty set for Y, Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z holds sup (F + G) <= (sup F) + (sup G) proof let X be non empty set ; ::_thesis: for Y, Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z holds sup (F + G) <= (sup F) + (sup G) let Y, Z be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y for G being Function of X,Z holds sup (F + G) <= (sup F) + (sup G) let F be Function of X,Y; ::_thesis: for G being Function of X,Z holds sup (F + G) <= (sup F) + (sup G) let G be Function of X,Z; ::_thesis: sup (F + G) <= (sup F) + (sup G) A1: sup ((rng F) + (rng G)) <= (sup (rng F)) + (sup (rng G)) by Th8; sup (F + G) <= sup ((rng F) + (rng G)) by Th16, XXREAL_2:59; hence sup (F + G) <= (sup F) + (sup G) by A1, XXREAL_0:2; ::_thesis: verum end; theorem Th18: :: SUPINF_2:18 for X being non empty set for Y, Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z holds (inf F) + (inf G) <= inf (F + G) proof let X be non empty set ; ::_thesis: for Y, Z being non empty Subset of ExtREAL for F being Function of X,Y for G being Function of X,Z holds (inf F) + (inf G) <= inf (F + G) let Y, Z be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y for G being Function of X,Z holds (inf F) + (inf G) <= inf (F + G) let F be Function of X,Y; ::_thesis: for G being Function of X,Z holds (inf F) + (inf G) <= inf (F + G) let G be Function of X,Z; ::_thesis: (inf F) + (inf G) <= inf (F + G) A1: (inf (rng F)) + (inf (rng G)) <= inf ((rng F) + (rng G)) by Th9; inf ((rng F) + (rng G)) <= inf (F + G) by Th16, XXREAL_2:60; hence (inf F) + (inf G) <= inf (F + G) by A1, XXREAL_0:2; ::_thesis: verum end; 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 :Def4: :: SUPINF_2:def 4 for x being Element of X holds it . x = - (F . x); existence ex b1 being Function of X,(- Y) st for x being Element of X holds b1 . x = - (F . x) proof deffunc H1( Element of X) -> R_eal = - (F . \$1); A1: for x being Element of X holds H1(x) in - Y proof let x be Element of X; ::_thesis: H1(x) in - Y F . x in Y by FUNCT_2:5; hence H1(x) in - Y ; ::_thesis: verum end; ex H being Function of X,(- Y) st for x being Element of X holds H . x = H1(x) from FUNCT_2:sch_8(A1); then consider H being Function of X,(- Y) such that A2: for x being Element of X holds H . x = - (F . x) ; take H ; ::_thesis: for x being Element of X holds H . x = - (F . x) thus for x being Element of X holds H . x = - (F . x) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of X,(- Y) st ( for x being Element of X holds b1 . x = - (F . x) ) & ( for x being Element of X holds b2 . x = - (F . x) ) holds b1 = b2 proof let H1, H2 be Function of X,(- Y); ::_thesis: ( ( for x being Element of X holds H1 . x = - (F . x) ) & ( for x being Element of X holds H2 . x = - (F . x) ) implies H1 = H2 ) assume that A3: for x being Element of X holds H1 . x = - (F . x) and A4: for x being Element of X holds H2 . x = - (F . x) ; ::_thesis: H1 = H2 for x being set st x in X holds H1 . x = H2 . x proof let x be set ; ::_thesis: ( x in X implies H1 . x = H2 . x ) assume x in X ; ::_thesis: H1 . x = H2 . x then reconsider x = x as Element of X ; H1 . x = - (F . x) by A3 .= H2 . x by A4 ; hence H1 . x = H2 . x ; ::_thesis: verum end; hence H1 = H2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def4 defines - SUPINF_2:def_4_:_ for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y for b4 being Function of X,(- Y) holds ( b4 = - F iff for x being Element of X holds b4 . x = - (F . x) ); theorem Th19: :: SUPINF_2:19 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds rng (- F) = - (rng F) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y holds rng (- F) = - (rng F) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y holds rng (- F) = - (rng F) let F be Function of X,Y; ::_thesis: rng (- F) = - (rng F) thus rng (- F) c= - (rng F) :: according to XBOOLE_0:def_10 ::_thesis: - (rng F) c= rng (- F) proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (- F) or y in - (rng F) ) A1: dom F = X by FUNCT_2:def_1; assume A2: y in rng (- F) ; ::_thesis: y in - (rng F) then reconsider y = y as R_eal ; dom (- F) = X by FUNCT_2:def_1; then consider a being set such that A3: a in X and A4: y = (- F) . a by A2, FUNCT_1:def_3; reconsider a = a as Element of X by A3; y = - (F . a) by A4, Def4; then - y in rng F by A1, FUNCT_1:def_3; then - (- y) in - (rng F) ; hence y in - (rng F) ; ::_thesis: verum end; thus - (rng F) c= rng (- F) ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in - (rng F) or y in rng (- F) ) assume A5: y in - (rng F) ; ::_thesis: y in rng (- F) then reconsider y = y as R_eal ; A6: - y in - (- (rng F)) by A5; dom F = X by FUNCT_2:def_1; then consider a being set such that A7: a in X and A8: - y = F . a by A6, FUNCT_1:def_3; reconsider a = a as Element of X by A7; y = - (F . a) by A8; then A9: y = (- F) . a by Def4; dom (- F) = X by FUNCT_2:def_1; hence y in rng (- F) by A9, FUNCT_1:def_3; ::_thesis: verum end; end; theorem Th20: :: SUPINF_2:20 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( inf (- F) = - (sup F) & sup (- F) = - (inf F) ) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( inf (- F) = - (sup F) & sup (- F) = - (inf F) ) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y holds ( inf (- F) = - (sup F) & sup (- F) = - (inf F) ) let F be Function of X,Y; ::_thesis: ( inf (- F) = - (sup F) & sup (- F) = - (inf F) ) thus inf (- F) = inf (- (rng F)) by Th19 .= - (sup F) by Th14 ; ::_thesis: sup (- F) = - (inf F) thus sup (- F) = sup (- (rng F)) by Th19 .= - (inf F) by Th15 ; ::_thesis: verum end; definition let X be set ; let Y be Subset of ExtREAL; let F be Function of X,Y; attrF is bounded_above means :Def5: :: SUPINF_2:def 5 sup F < +infty ; attrF is bounded_below means :Def6: :: SUPINF_2:def 6 -infty < inf F; end; :: deftheorem Def5 defines bounded_above SUPINF_2:def_5_:_ for X being set for Y being Subset of ExtREAL for F being Function of X,Y holds ( F is bounded_above iff sup F < +infty ); :: deftheorem Def6 defines bounded_below SUPINF_2:def_6_:_ for X being set for Y being Subset of ExtREAL for F being Function of X,Y holds ( F is bounded_below iff -infty < inf F ); definition let X be set ; let Y be Subset of ExtREAL; let F be Function of X,Y; attrF is bounded means :Def7: :: SUPINF_2:def 7 ( F is bounded_above & F is bounded_below ); end; :: deftheorem Def7 defines bounded SUPINF_2:def_7_:_ for X being set for Y being Subset of ExtREAL for F being Function of X,Y holds ( F is bounded iff ( F is bounded_above & F is bounded_below ) ); registration let X be set ; let Y be Subset of ExtREAL; cluster Function-like V18(X,Y) bounded -> bounded_above bounded_below for Element of K19(K20(X,Y)); coherence for b1 being Function of X,Y st b1 is bounded holds ( b1 is bounded_above & b1 is bounded_below ) by Def7; cluster Function-like V18(X,Y) bounded_above bounded_below -> bounded for Element of K19(K20(X,Y)); coherence for b1 being Function of X,Y st b1 is bounded_above & b1 is bounded_below holds b1 is bounded by Def7; end; theorem :: SUPINF_2:21 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded iff ( sup F < +infty & -infty < inf F ) ) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded iff ( sup F < +infty & -infty < inf F ) ) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y holds ( F is bounded iff ( sup F < +infty & -infty < inf F ) ) let F be Function of X,Y; ::_thesis: ( F is bounded iff ( sup F < +infty & -infty < inf F ) ) thus ( F is bounded implies ( sup F < +infty & -infty < inf F ) ) by Def5, Def6; ::_thesis: ( sup F < +infty & -infty < inf F implies F is bounded ) assume that A1: sup F < +infty and A2: -infty < inf F ; ::_thesis: F is bounded A3: F is bounded_below by A2, Def6; F is bounded_above by A1, Def5; hence F is bounded by A3; ::_thesis: verum end; theorem Th22: :: SUPINF_2:22 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded_above iff - F is bounded_below ) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded_above iff - F is bounded_below ) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y holds ( F is bounded_above iff - F is bounded_below ) let F be Function of X,Y; ::_thesis: ( F is bounded_above iff - F is bounded_below ) hereby ::_thesis: ( - F is bounded_below implies F is bounded_above ) assume F is bounded_above ; ::_thesis: - F is bounded_below then sup F < +infty by Def5; then A1: - +infty < - (sup F) by XXREAL_3:38; - +infty = -infty by XXREAL_3:def_3; then -infty < inf (- F) by A1, Th20; hence - F is bounded_below by Def6; ::_thesis: verum end; assume - F is bounded_below ; ::_thesis: F is bounded_above then -infty < inf (- F) by Def6; then - (inf (- F)) < - -infty by XXREAL_3:38; then - (- (sup F)) < - -infty by Th20; hence F is bounded_above by Def5, XXREAL_3:5; ::_thesis: verum end; theorem Th23: :: SUPINF_2:23 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded_below iff - F is bounded_above ) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded_below iff - F is bounded_above ) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y holds ( F is bounded_below iff - F is bounded_above ) let F be Function of X,Y; ::_thesis: ( F is bounded_below iff - F is bounded_above ) hereby ::_thesis: ( - F is bounded_above implies F is bounded_below ) assume F is bounded_below ; ::_thesis: - F is bounded_above then -infty < inf F by Def6; then - (inf F) < - -infty by XXREAL_3:38; then sup (- F) < +infty by Th20, XXREAL_3:5; hence - F is bounded_above by Def5; ::_thesis: verum end; assume - F is bounded_above ; ::_thesis: F is bounded_below then sup (- F) < +infty by Def5; then - (inf F) < +infty by Th20; then A1: - +infty < - (- (inf F)) by XXREAL_3:38; - +infty = -infty by XXREAL_3:def_3; hence F is bounded_below by A1, Def6; ::_thesis: verum end; theorem :: SUPINF_2:24 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded iff - F is bounded ) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y holds ( F is bounded iff - F is bounded ) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y holds ( F is bounded iff - F is bounded ) let F be Function of X,Y; ::_thesis: ( F is bounded iff - F is bounded ) hereby ::_thesis: ( - F is bounded implies F is bounded ) assume A1: F is bounded ; ::_thesis: - F is bounded then A2: - F is bounded_below by Th22; - F is bounded_above by A1, Th23; hence - F is bounded by A2; ::_thesis: verum end; assume A3: - F is bounded ; ::_thesis: F is bounded then A4: F is bounded_below by Th23; F is bounded_above by A3, Th22; hence F is bounded by A4; ::_thesis: verum end; theorem :: SUPINF_2:25 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y for x being Element of X holds ( -infty <= F . x & F . x <= +infty ) by XXREAL_0:4, XXREAL_0:5; theorem :: SUPINF_2:26 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y for x being Element of X st Y c= REAL holds ( -infty < F . x & F . x < +infty ) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y for x being Element of X st Y c= REAL holds ( -infty < F . x & F . x < +infty ) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y for x being Element of X st Y c= REAL holds ( -infty < F . x & F . x < +infty ) let F be Function of X,Y; ::_thesis: for x being Element of X st Y c= REAL holds ( -infty < F . x & F . x < +infty ) let x be Element of X; ::_thesis: ( Y c= REAL implies ( -infty < F . x & F . x < +infty ) ) A1: -infty <= F . x by XXREAL_0:5; assume Y c= REAL ; ::_thesis: ( -infty < F . x & F . x < +infty ) hence ( -infty < F . x & F . x < +infty ) by A1, XXREAL_0:1, XXREAL_0:4; ::_thesis: verum end; theorem Th27: :: SUPINF_2:27 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y for x being Element of X holds ( inf F <= F . x & F . x <= sup F ) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y for x being Element of X holds ( inf F <= F . x & F . x <= sup F ) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y for x being Element of X holds ( inf F <= F . x & F . x <= sup F ) let F be Function of X,Y; ::_thesis: for x being Element of X holds ( inf F <= F . x & F . x <= sup F ) let x be Element of X; ::_thesis: ( inf F <= F . x & F . x <= sup F ) X = dom F by FUNCT_2:def_1; then F . x in rng F by FUNCT_1:def_3; hence ( inf F <= F . x & F . x <= sup F ) by XXREAL_2:3, XXREAL_2:4; ::_thesis: verum end; theorem Th28: :: SUPINF_2:28 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y st Y c= REAL holds ( F is bounded_above iff sup F in REAL ) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y st Y c= REAL holds ( F is bounded_above iff sup F in REAL ) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y st Y c= REAL holds ( F is bounded_above iff sup F in REAL ) let F be Function of X,Y; ::_thesis: ( Y c= REAL implies ( F is bounded_above iff sup F in REAL ) ) assume A1: Y c= REAL ; ::_thesis: ( F is bounded_above iff sup F in REAL ) hereby ::_thesis: ( sup F in REAL implies F is bounded_above ) set x = the Element of X; X = dom F by FUNCT_2:def_1; then A2: F . the Element of X in rng F by FUNCT_1:def_3; rng F c= Y by RELAT_1:def_19; then F . the Element of X in Y by A2; then A3: not sup F = -infty by A1, Th27, XXREAL_0:12; assume F is bounded_above ; ::_thesis: sup F in REAL then A4: sup F < +infty by Def5; ( sup F in REAL or sup F in {-infty,+infty} ) by XBOOLE_0:def_3; hence sup F in REAL by A4, A3, TARSKI:def_2; ::_thesis: verum end; assume sup F in REAL ; ::_thesis: F is bounded_above then sup F < +infty by XXREAL_0:9; hence F is bounded_above by Def5; ::_thesis: verum end; theorem Th29: :: SUPINF_2:29 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y st Y c= REAL holds ( F is bounded_below iff inf F in REAL ) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y st Y c= REAL holds ( F is bounded_below iff inf F in REAL ) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y st Y c= REAL holds ( F is bounded_below iff inf F in REAL ) let F be Function of X,Y; ::_thesis: ( Y c= REAL implies ( F is bounded_below iff inf F in REAL ) ) assume A1: Y c= REAL ; ::_thesis: ( F is bounded_below iff inf F in REAL ) thus ( F is bounded_below implies inf F in REAL ) ::_thesis: ( inf F in REAL implies F is bounded_below ) proof set x = the Element of X; X = dom F by FUNCT_2:def_1; then A2: F . the Element of X in rng F by FUNCT_1:def_3; rng F c= Y by RELAT_1:def_19; then F . the Element of X in Y by A2; then A3: not inf F = +infty by A1, Th27, XXREAL_0:9; assume F is bounded_below ; ::_thesis: inf F in REAL then A4: -infty < inf F by Def6; ( inf F in REAL or inf F in {-infty,+infty} ) by XBOOLE_0:def_3; hence inf F in REAL by A4, A3, TARSKI:def_2; ::_thesis: verum end; assume inf F in REAL ; ::_thesis: F is bounded_below then -infty < inf F by XXREAL_0:12; hence F is bounded_below by Def6; ::_thesis: verum end; theorem :: SUPINF_2:30 for X being non empty set for Y being non empty Subset of ExtREAL for F being Function of X,Y st Y c= REAL holds ( F is bounded iff ( inf F in REAL & sup F in REAL ) ) proof let X be non empty set ; ::_thesis: for Y being non empty Subset of ExtREAL for F being Function of X,Y st Y c= REAL holds ( F is bounded iff ( inf F in REAL & sup F in REAL ) ) let Y be non empty Subset of ExtREAL; ::_thesis: for F being Function of X,Y st Y c= REAL holds ( F is bounded iff ( inf F in REAL & sup F in REAL ) ) let F be Function of X,Y; ::_thesis: ( Y c= REAL implies ( F is bounded iff ( inf F in REAL & sup F in REAL ) ) ) assume A1: Y c= REAL ; ::_thesis: ( F is bounded iff ( inf F in REAL & sup F in REAL ) ) hence ( F is bounded implies ( inf F in REAL & sup F in REAL ) ) by Th28, Th29; ::_thesis: ( inf F in REAL & sup F in REAL implies F is bounded ) assume that A2: inf F in REAL and A3: sup F in REAL ; ::_thesis: F is bounded A4: F is bounded_below by A1, A2, Th29; F is bounded_above by A1, A3, Th28; hence F is bounded by A4; ::_thesis: verum end; theorem Th31: :: SUPINF_2:31 for X being non empty set for Y, Z being non empty Subset of ExtREAL for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded_above & F2 is bounded_above holds F1 + F2 is bounded_above proof let X be non empty set ; ::_thesis: for Y, Z being non empty Subset of ExtREAL for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded_above & F2 is bounded_above holds F1 + F2 is bounded_above let Y, Z be non empty Subset of ExtREAL; ::_thesis: for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded_above & F2 is bounded_above holds F1 + F2 is bounded_above let F1 be Function of X,Y; ::_thesis: for F2 being Function of X,Z st F1 is bounded_above & F2 is bounded_above holds F1 + F2 is bounded_above let F2 be Function of X,Z; ::_thesis: ( F1 is bounded_above & F2 is bounded_above implies F1 + F2 is bounded_above ) assume that A1: F1 is bounded_above and A2: F2 is bounded_above ; ::_thesis: F1 + F2 is bounded_above A3: not sup F2 = +infty by A2, Def5; A4: ( sup F1 in REAL & sup F2 in REAL implies (sup F1) + (sup F2) < +infty ) proof reconsider a = sup F1, b = sup F2 as R_eal ; assume that A5: sup F1 in REAL and A6: sup F2 in REAL ; ::_thesis: (sup F1) + (sup F2) < +infty reconsider a = a, b = b as Real by A5, A6; (sup F1) + (sup F2) = a + b by XXREAL_3:def_2; hence (sup F1) + (sup F2) < +infty by XXREAL_0:9; ::_thesis: verum end; A7: ( sup F1 in REAL & sup F2 = -infty implies (sup F1) + (sup F2) < +infty ) by XXREAL_0:7, XXREAL_3:def_2; A8: ( sup F1 = -infty & sup F2 = -infty implies (sup F1) + (sup F2) < +infty ) by XXREAL_0:7, XXREAL_3:def_2; A9: ( sup F1 = -infty & sup F2 in REAL implies (sup F1) + (sup F2) < +infty ) by XXREAL_0:7, XXREAL_3:def_2; A10: not sup F1 = +infty by A1, Def5; sup (F1 + F2) < +infty proof assume not sup (F1 + F2) < +infty ; ::_thesis: contradiction then ( not sup (F1 + F2) <= +infty or sup (F1 + F2) = +infty ) by XXREAL_0:1; hence contradiction by A10, A3, A4, A7, A9, A8, Th17, XXREAL_0:4, XXREAL_3:def_1; ::_thesis: verum end; hence F1 + F2 is bounded_above by Def5; ::_thesis: verum end; theorem Th32: :: SUPINF_2:32 for X being non empty set for Y, Z being non empty Subset of ExtREAL for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded_below & F2 is bounded_below holds F1 + F2 is bounded_below proof let X be non empty set ; ::_thesis: for Y, Z being non empty Subset of ExtREAL for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded_below & F2 is bounded_below holds F1 + F2 is bounded_below let Y, Z be non empty Subset of ExtREAL; ::_thesis: for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded_below & F2 is bounded_below holds F1 + F2 is bounded_below let F1 be Function of X,Y; ::_thesis: for F2 being Function of X,Z st F1 is bounded_below & F2 is bounded_below holds F1 + F2 is bounded_below let F2 be Function of X,Z; ::_thesis: ( F1 is bounded_below & F2 is bounded_below implies F1 + F2 is bounded_below ) assume that A1: F1 is bounded_below and A2: F2 is bounded_below ; ::_thesis: F1 + F2 is bounded_below A3: not inf F2 = -infty by A2, Def6; A4: ( inf F1 in REAL & inf F2 in REAL implies -infty < (inf F1) + (inf F2) ) proof reconsider a = inf F1, b = inf F2 as R_eal ; assume that A5: inf F1 in REAL and A6: inf F2 in REAL ; ::_thesis: -infty < (inf F1) + (inf F2) reconsider a = a, b = b as Real by A5, A6; (inf F1) + (inf F2) = a + b by XXREAL_3:def_2; hence -infty < (inf F1) + (inf F2) by XXREAL_0:12; ::_thesis: verum end; A7: ( inf F1 in REAL & inf F2 = +infty implies -infty < (inf F1) + (inf F2) ) by XXREAL_0:7, XXREAL_3:def_2; A8: ( inf F1 = +infty & inf F2 = +infty implies -infty < (inf F1) + (inf F2) ) by XXREAL_0:7, XXREAL_3:def_2; A9: ( inf F1 = +infty & inf F2 in REAL implies -infty < (inf F1) + (inf F2) ) by XXREAL_0:7, XXREAL_3:def_2; A10: not inf F1 = -infty by A1, Def6; -infty < inf (F1 + F2) proof assume inf (F1 + F2) <= -infty ; ::_thesis: contradiction then ( not -infty <= inf (F1 + F2) or inf (F1 + F2) = -infty ) by XXREAL_0:1; hence contradiction by A10, A3, A4, A7, A9, A8, Th18, XXREAL_0:6, XXREAL_3:def_1; ::_thesis: verum end; hence F1 + F2 is bounded_below by Def6; ::_thesis: verum end; theorem :: SUPINF_2:33 for X being non empty set for Y, Z being non empty Subset of ExtREAL for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds F1 + F2 is bounded proof let X be non empty set ; ::_thesis: for Y, Z being non empty Subset of ExtREAL for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds F1 + F2 is bounded let Y, Z be non empty Subset of ExtREAL; ::_thesis: for F1 being Function of X,Y for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds F1 + F2 is bounded let F1 be Function of X,Y; ::_thesis: for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds F1 + F2 is bounded let F2 be Function of X,Z; ::_thesis: ( F1 is bounded & F2 is bounded implies F1 + F2 is bounded ) assume that A1: F1 is bounded and A2: F2 is bounded ; ::_thesis: F1 + F2 is bounded A3: F1 + F2 is bounded_below by A1, A2, Th32; F1 + F2 is bounded_above by A1, A2, Th31; hence F1 + F2 is bounded by A3; ::_thesis: verum end; theorem Th34: :: SUPINF_2:34 ( incl NAT is Function of NAT,ExtREAL & incl NAT is one-to-one & NAT = rng (incl NAT) & rng (incl NAT) is non empty Subset of ExtREAL ) proof reconsider F = incl NAT as Function of NAT,ExtREAL by FUNCT_2:7, NUMBERS:31; rng F c= ExtREAL ; hence ( incl NAT is Function of NAT,ExtREAL & incl NAT is one-to-one & NAT = rng (incl NAT) & rng (incl NAT) is non empty Subset of ExtREAL ) ; ::_thesis: verum end; definition let D be non empty set ; let IT be Subset of D; :: original: countable redefine attrIT is countable means :Def8: :: SUPINF_2:def 8 ( IT is empty or ex F being Function of NAT,D st IT = rng F ); compatibility ( IT is countable iff ( IT is empty or ex F being Function of NAT,D st IT = rng F ) ) proof thus ( not IT is countable or IT is empty or ex F being Function of NAT,D st IT = rng F ) ::_thesis: ( ( IT is empty or ex F being Function of NAT,D st IT = rng F ) implies IT is countable ) proof assume that A1: IT is countable and A2: not IT is empty ; ::_thesis: ex F being Function of NAT,D st IT = rng F consider f being Function such that A3: dom f = NAT and A4: IT c= rng f by A1, CARD_3:93; consider x being Element of D such that A5: x in IT by A2, SUBSET_1:4; set F = (f | (f " IT)) +* ((NAT \ (f " IT)) --> x); A6: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT ) proof A7: f " IT c= NAT by A3, RELAT_1:132; A8: dom (f | (f " IT)) = NAT /\ (f " IT) by A3, RELAT_1:61; percases ( NAT = f " IT or NAT <> f " IT ) ; supposeA9: NAT = f " IT ; ::_thesis: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT ) then A10: NAT \ (f " IT) = {} by XBOOLE_1:37; then dom ((NAT \ (f " IT)) --> x) = {} ; then (dom (f | (f " IT))) /\ (dom ((NAT \ (f " IT)) --> x)) = {} ; then dom (f | (f " IT)) misses dom ((NAT \ (f " IT)) --> x) by XBOOLE_0:def_7; then (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by FUNCT_4:31; hence rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:12 .= (rng (f | (f " IT))) \/ {} by A10 .= f .: (f " IT) by RELAT_1:115 .= IT by A4, FUNCT_1:77 ; ::_thesis: dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT thus dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (dom (f | (f " IT))) \/ (dom ((NAT \ (f " IT)) --> x)) by FUNCT_4:def_1 .= (dom (f | (f " IT))) \/ {} by A10 .= NAT by A8, A9 ; ::_thesis: verum end; supposeA11: NAT <> f " IT ; ::_thesis: ( rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = IT & dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT ) A12: now__::_thesis:_not_NAT_\_(f_"_IT)_is_empty assume NAT \ (f " IT) is empty ; ::_thesis: contradiction then NAT c= f " IT by XBOOLE_1:37; hence contradiction by A7, A11, XBOOLE_0:def_10; ::_thesis: verum end; dom ((NAT \ (f " IT)) --> x) = NAT \ (f " IT) by FUNCOP_1:13; then (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) = (f | (f " IT)) \/ ((NAT \ (f " IT)) --> x) by A8, FUNCT_4:31, XBOOLE_1:89; hence rng ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (rng (f | (f " IT))) \/ (rng ((NAT \ (f " IT)) --> x)) by RELAT_1:12 .= (rng (f | (f " IT))) \/ {x} by A12, FUNCOP_1:8 .= (f .: (f " IT)) \/ {x} by RELAT_1:115 .= IT \/ {x} by A4, FUNCT_1:77 .= IT by A5, ZFMISC_1:40 ; ::_thesis: dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = NAT thus dom ((f | (f " IT)) +* ((NAT \ (f " IT)) --> x)) = (dom (f | (f " IT))) \/ (dom ((NAT \ (f " IT)) --> x)) by FUNCT_4:def_1 .= (NAT /\ (f " IT)) \/ (NAT \ (f " IT)) by A8, FUNCOP_1:13 .= NAT by XBOOLE_1:51 ; ::_thesis: verum end; end; end; then reconsider F = (f | (f " IT)) +* ((NAT \ (f " IT)) --> x) as Function of NAT,D by FUNCT_2:def_1, RELSET_1:4; take F ; ::_thesis: IT = rng F thus IT = rng F by A6; ::_thesis: verum end; assume A13: ( IT is empty or ex F being Function of NAT,D st IT = rng F ) ; ::_thesis: IT is countable percases ( IT is empty or not IT is empty ) ; suppose IT is empty ; ::_thesis: IT is countable hence IT is countable by CARD_4:1; ::_thesis: verum end; suppose not IT is empty ; ::_thesis: IT is countable then consider F being Function of NAT,D such that A14: IT = rng F by A13; dom F = NAT by FUNCT_2:def_1; hence IT is countable by A14, CARD_3:93; ::_thesis: verum end; end; end; end; :: deftheorem Def8 defines countable SUPINF_2:def_8_:_ for D being non empty set for IT being Subset of D holds ( IT is countable iff ( IT is empty or ex F being Function of NAT,D st IT = rng F ) ); registration cluster non empty ext-real-membered V78() for Element of K19(ExtREAL); existence not for b1 being non empty Subset of ExtREAL holds b1 is V78() proof set F = the Function of NAT,ExtREAL; reconsider A = rng the Function of NAT,ExtREAL as non empty Subset of ExtREAL ; take A ; ::_thesis: A is V78() assume not A is empty ; :: according to SUPINF_2:def_8 ::_thesis: ex F being Function of NAT,ExtREAL st A = rng F thus ex F being Function of NAT,ExtREAL st A = rng F ; ::_thesis: verum end; end; definition mode Denum_Set_of_R_EAL is non empty V78() Subset of ExtREAL; end; definition let IT be set ; attrIT is nonnegative means :Def9: :: SUPINF_2:def 9 for x being R_eal st x in IT holds 0. <= x; end; :: deftheorem Def9 defines nonnegative SUPINF_2:def_9_:_ for IT being set holds ( IT is nonnegative iff for x being R_eal st x in IT holds 0. <= x ); registration cluster non empty ext-real-membered countable nonnegative for Element of K19(ExtREAL); existence ex b1 being Denum_Set_of_R_EAL st b1 is nonnegative proof reconsider N = NAT as Denum_Set_of_R_EAL by Def8, Th34; take N ; ::_thesis: N is nonnegative thus for x being R_eal st x in N holds 0. <= x by NAT_1:2; :: according to SUPINF_2:def_9 ::_thesis: verum end; 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 :Def10: :: SUPINF_2:def 10 D = rng it; existence ex b1 being Function of NAT,ExtREAL st D = rng b1 by Def8; end; :: deftheorem Def10 defines Num SUPINF_2:def_10_:_ for D being Denum_Set_of_R_EAL for b2 being Function of NAT,ExtREAL holds ( b2 is Num of D iff D = rng b2 ); definition let D be Denum_Set_of_R_EAL; let N be Num of D; func Ser (D,N) -> Function of NAT,ExtREAL means :Def11: :: SUPINF_2:def 11 ( it . 0 = N . 0 & ( for n being Element of NAT for y being R_eal st y = it . n holds it . (n + 1) = y + (N . (n + 1)) ) ); existence ex b1 being Function of NAT,ExtREAL st ( b1 . 0 = N . 0 & ( for n being Element of NAT for y being R_eal st y = b1 . n holds b1 . (n + 1) = y + (N . (n + 1)) ) ) proof defpred S1[ set , set , set ] means for a, b being R_eal for s being Element of NAT st s = \$1 & a = \$2 & b = \$3 holds b = a + (N . (s + 1)); reconsider A = N . 0 as R_eal ; A1: for n being Element of NAT for x being Element of ExtREAL ex y being Element of ExtREAL st S1[n,x,y] proof let n be Element of NAT ; ::_thesis: for x being Element of ExtREAL ex y being Element of ExtREAL st S1[n,x,y] let x be Element of ExtREAL ; ::_thesis: ex y being Element of ExtREAL st S1[n,x,y] reconsider y = x + (N . (n + 1)) as R_eal ; take y ; ::_thesis: S1[n,x,y] thus S1[n,x,y] ; ::_thesis: verum end; consider F being Function of NAT,ExtREAL such that A2: ( F . 0 = A & ( for n being Element of NAT holds S1[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch_2(A1); take F ; ::_thesis: ( F . 0 = N . 0 & ( for n being Element of NAT for y being R_eal st y = F . n holds F . (n + 1) = y + (N . (n + 1)) ) ) thus ( F . 0 = N . 0 & ( for n being Element of NAT for y being R_eal st y = F . n holds F . (n + 1) = y + (N . (n + 1)) ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,ExtREAL st b1 . 0 = N . 0 & ( for n being Element of NAT for y being R_eal st y = b1 . n holds b1 . (n + 1) = y + (N . (n + 1)) ) & b2 . 0 = N . 0 & ( for n being Element of NAT for y being R_eal st y = b2 . n holds b2 . (n + 1) = y + (N . (n + 1)) ) holds b1 = b2 proof let S1, S2 be Function of NAT,ExtREAL; ::_thesis: ( S1 . 0 = N . 0 & ( for n being Element of NAT for y being R_eal st y = S1 . n holds S1 . (n + 1) = y + (N . (n + 1)) ) & S2 . 0 = N . 0 & ( for n being Element of NAT for y being R_eal st y = S2 . n holds S2 . (n + 1) = y + (N . (n + 1)) ) implies S1 = S2 ) assume that A3: S1 . 0 = N . 0 and A4: for n being Element of NAT for y being R_eal st y = S1 . n holds S1 . (n + 1) = y + (N . (n + 1)) and A5: S2 . 0 = N . 0 and A6: for n being Element of NAT for y being R_eal st y = S2 . n holds S2 . (n + 1) = y + (N . (n + 1)) ; ::_thesis: S1 = S2 defpred S1[ set ] means S1 . \$1 = S2 . \$1; for n being set st n in NAT holds S1[n] proof let n be set ; ::_thesis: ( n in NAT implies S1[n] ) assume A7: n in NAT ; ::_thesis: S1[n] then reconsider n = n as Element of REAL ; reconsider n = n as Element of NAT by A7; A8: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) reconsider y2 = S2 . k as R_eal ; assume S1 . k = S2 . k ; ::_thesis: S1[k + 1] hence S1 . (k + 1) = y2 + (N . (k + 1)) by A4 .= S2 . (k + 1) by A6 ; ::_thesis: verum end; A9: S1[ 0 ] by A3, A5; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A9, A8); then S1 . n = S2 . n ; hence S1[n] ; ::_thesis: verum end; hence S1 = S2 by FUNCT_2:12; ::_thesis: verum end; end; :: deftheorem Def11 defines Ser SUPINF_2:def_11_:_ for D being Denum_Set_of_R_EAL for N being Num of D for b3 being Function of NAT,ExtREAL holds ( b3 = Ser (D,N) iff ( b3 . 0 = N . 0 & ( for n being Element of NAT for y being R_eal st y = b3 . n holds b3 . (n + 1) = y + (N . (n + 1)) ) ) ); theorem Th35: :: SUPINF_2:35 for D being Pos_Denum_Set_of_R_EAL for N being Num of D for n being Element of NAT holds 0. <= N . n proof let D be Pos_Denum_Set_of_R_EAL; ::_thesis: for N being Num of D for n being Element of NAT holds 0. <= N . n let N be Num of D; ::_thesis: for n being Element of NAT holds 0. <= N . n let n be Element of NAT ; ::_thesis: 0. <= N . n D = rng N by Def10; then N . n in D by FUNCT_2:4; hence 0. <= N . n by Def9; ::_thesis: verum end; theorem Th36: :: SUPINF_2:36 for D being Pos_Denum_Set_of_R_EAL for N being Num of D for n being Element of NAT holds ( (Ser (D,N)) . n <= (Ser (D,N)) . (n + 1) & 0. <= (Ser (D,N)) . n ) proof let D be Pos_Denum_Set_of_R_EAL; ::_thesis: for N being Num of D for n being Element of NAT holds ( (Ser (D,N)) . n <= (Ser (D,N)) . (n + 1) & 0. <= (Ser (D,N)) . n ) let N be Num of D; ::_thesis: for n being Element of NAT holds ( (Ser (D,N)) . n <= (Ser (D,N)) . (n + 1) & 0. <= (Ser (D,N)) . n ) let n be Element of NAT ; ::_thesis: ( (Ser (D,N)) . n <= (Ser (D,N)) . (n + 1) & 0. <= (Ser (D,N)) . n ) set F = Ser (D,N); defpred S1[ Element of NAT ] means ( (Ser (D,N)) . \$1 <= (Ser (D,N)) . (\$1 + 1) & 0. <= (Ser (D,N)) . \$1 ); A1: (Ser (D,N)) . (0 + 1) = ((Ser (D,N)) . 0) + (N . 1) by Def11; A2: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume that A3: (Ser (D,N)) . k <= (Ser (D,N)) . (k + 1) and A4: 0. <= (Ser (D,N)) . k ; ::_thesis: S1[k + 1] A5: 0. <= N . ((k + 1) + 1) by Th35; (Ser (D,N)) . ((k + 1) + 1) = ((Ser (D,N)) . (k + 1)) + (N . ((k + 1) + 1)) by Def11; hence S1[k + 1] by A3, A4, A5, XXREAL_0:2, XXREAL_3:39; ::_thesis: verum end; (Ser (D,N)) . 0 = N . 0 by Def11; then A6: S1[ 0 ] by A1, Th35, XXREAL_3:39; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A2); hence ( (Ser (D,N)) . n <= (Ser (D,N)) . (n + 1) & 0. <= (Ser (D,N)) . n ) ; ::_thesis: verum end; theorem Th37: :: SUPINF_2:37 for D being Pos_Denum_Set_of_R_EAL for N being Num of D for n, m being Element of NAT holds (Ser (D,N)) . n <= (Ser (D,N)) . (n + m) proof let D be Pos_Denum_Set_of_R_EAL; ::_thesis: for N being Num of D for n, m being Element of NAT holds (Ser (D,N)) . n <= (Ser (D,N)) . (n + m) let N be Num of D; ::_thesis: for n, m being Element of NAT holds (Ser (D,N)) . n <= (Ser (D,N)) . (n + m) let n, m be Element of NAT ; ::_thesis: (Ser (D,N)) . n <= (Ser (D,N)) . (n + m) defpred S1[ Element of NAT ] means (Ser (D,N)) . n <= (Ser (D,N)) . (n + \$1); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) (Ser (D,N)) . (n + (k + 1)) = (Ser (D,N)) . ((n + k) + 1) ; then A2: (Ser (D,N)) . (n + k) <= (Ser (D,N)) . (n + (k + 1)) by Th36; assume (Ser (D,N)) . n <= (Ser (D,N)) . (n + k) ; ::_thesis: S1[k + 1] hence S1[k + 1] by A2, XXREAL_0:2; ::_thesis: verum end; A3: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence (Ser (D,N)) . n <= (Ser (D,N)) . (n + m) ; ::_thesis: verum end; definition let D be Denum_Set_of_R_EAL; mode Set_of_Series of D -> non empty Subset of ExtREAL means :: SUPINF_2:def 12 ex N being Num of D st it = rng (Ser (D,N)); existence ex b1 being non empty Subset of ExtREAL ex N being Num of D st b1 = rng (Ser (D,N)) proof take rng (Ser (D, the Num of D)) ; ::_thesis: ex N being Num of D st rng (Ser (D, the Num of D)) = rng (Ser (D,N)) thus ex N being Num of D st rng (Ser (D, the Num of D)) = rng (Ser (D,N)) ; ::_thesis: verum end; end; :: deftheorem defines Set_of_Series SUPINF_2:def_12_:_ for D being Denum_Set_of_R_EAL for b2 being non empty Subset of ExtREAL holds ( b2 is Set_of_Series of D iff ex N being Num of D st b2 = rng (Ser (D,N)) ); 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 13 sup (rng (Ser (D,N))); coherence sup (rng (Ser (D,N))) is R_eal ; end; :: deftheorem defines SUM SUPINF_2:def_13_:_ for D being Pos_Denum_Set_of_R_EAL for N being Num of D holds SUM (D,N) = sup (rng (Ser (D,N))); definition let D be Pos_Denum_Set_of_R_EAL; let N be Num of D; predD is_sumable N means :: SUPINF_2:def 14 SUM (D,N) in REAL ; end; :: deftheorem defines is_sumable SUPINF_2:def_14_:_ for D being Pos_Denum_Set_of_R_EAL for N being Num of D holds ( D is_sumable N iff SUM (D,N) in REAL ); theorem Th38: :: SUPINF_2:38 for F being Function of NAT,ExtREAL holds rng F is Denum_Set_of_R_EAL by Def8; definition let F be Function of NAT,ExtREAL; :: original: rng redefine func rng F -> Denum_Set_of_R_EAL; coherence rng F is Denum_Set_of_R_EAL by Th38; end; definition let F be Function of NAT,ExtREAL; func Ser F -> Function of NAT,ExtREAL means :Def15: :: SUPINF_2:def 15 for N being Num of rng F st N = F holds it = Ser ((rng F),N); existence ex b1 being Function of NAT,ExtREAL st for N being Num of rng F st N = F holds b1 = Ser ((rng F),N) proof reconsider N = F as Num of rng F by Def10; take Ser ((rng F),N) ; ::_thesis: for N being Num of rng F st N = F holds Ser ((rng F),N) = Ser ((rng F),N) thus for N being Num of rng F st N = F holds Ser ((rng F),N) = Ser ((rng F),N) ; ::_thesis: verum end; uniqueness for b1, b2 being Function of NAT,ExtREAL st ( for N being Num of rng F st N = F holds b1 = Ser ((rng F),N) ) & ( for N being Num of rng F st N = F holds b2 = Ser ((rng F),N) ) holds b1 = b2 proof reconsider N = F as Num of rng F by Def10; let S1, S2 be Function of NAT,ExtREAL; ::_thesis: ( ( for N being Num of rng F st N = F holds S1 = Ser ((rng F),N) ) & ( for N being Num of rng F st N = F holds S2 = Ser ((rng F),N) ) implies S1 = S2 ) assume that A1: for N being Num of rng F st N = F holds S1 = Ser ((rng F),N) and A2: for N being Num of rng F st N = F holds S2 = Ser ((rng F),N) ; ::_thesis: S1 = S2 thus S1 = Ser ((rng F),N) by A1 .= S2 by A2 ; ::_thesis: verum end; end; :: deftheorem Def15 defines Ser SUPINF_2:def_15_:_ for F, b2 being Function of NAT,ExtREAL holds ( b2 = Ser F iff for N being Num of rng F st N = F holds b2 = Ser ((rng F),N) ); definition let R be Relation; attrR is nonnegative means :Def16: :: SUPINF_2:def 16 rng R is nonnegative ; end; :: deftheorem Def16 defines nonnegative SUPINF_2:def_16_:_ for R being Relation holds ( R is nonnegative iff rng R is nonnegative ); definition let F be Function of NAT,ExtREAL; func SUM F -> R_eal equals :: SUPINF_2:def 17 sup (rng (Ser F)); coherence sup (rng (Ser F)) is R_eal ; end; :: deftheorem defines SUM SUPINF_2:def_17_:_ for F being Function of NAT,ExtREAL holds SUM F = sup (rng (Ser F)); theorem Th39: :: SUPINF_2:39 for X being set for F being PartFunc of X,ExtREAL holds ( F is nonnegative iff for n being Element of X holds 0. <= F . n ) proof let X be set ; ::_thesis: for F being PartFunc of X,ExtREAL holds ( F is nonnegative iff for n being Element of X holds 0. <= F . n ) let F be PartFunc of X,ExtREAL; ::_thesis: ( F is nonnegative iff for n being Element of X holds 0. <= F . n ) hereby ::_thesis: ( ( for n being Element of X holds 0. <= F . n ) implies F is nonnegative ) assume F is nonnegative ; ::_thesis: for n being Element of X holds 0. <= F . b2 then A1: rng F is nonnegative by Def16; let n be Element of X; ::_thesis: 0. <= F . b1 percases ( n in dom F or not n in dom F ) ; suppose n in dom F ; ::_thesis: 0. <= F . b1 then F . n in rng F by FUNCT_1:def_3; hence 0. <= F . n by A1, Def9; ::_thesis: verum end; suppose not n in dom F ; ::_thesis: 0. <= F . b1 hence 0. <= F . n by FUNCT_1:def_2; ::_thesis: verum end; end; end; assume A2: for n being Element of X holds 0. <= F . n ; ::_thesis: F is nonnegative let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( y in rng F implies 0. <= y ) assume y in rng F ; ::_thesis: 0. <= y then ex x being set st ( x in dom F & y = F . x ) by FUNCT_1:def_3; hence 0. <= y by A2; ::_thesis: verum end; theorem Th40: :: SUPINF_2:40 for F being Function of NAT,ExtREAL for n being Element of NAT st F is nonnegative holds ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) proof let F be Function of NAT,ExtREAL; ::_thesis: for n being Element of NAT st F is nonnegative holds ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) let n be Element of NAT ; ::_thesis: ( F is nonnegative implies ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) ) reconsider N = F as Num of rng F by Def10; assume F is nonnegative ; ::_thesis: ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) then A1: rng F is Pos_Denum_Set_of_R_EAL by Def16; Ser F = Ser ((rng F),N) by Def15; hence ( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n ) by A1, Th36; ::_thesis: verum end; theorem Th41: :: SUPINF_2:41 for F being Function of NAT,ExtREAL st F is nonnegative holds for n, m being Element of NAT holds (Ser F) . n <= (Ser F) . (n + m) proof let F be Function of NAT,ExtREAL; ::_thesis: ( F is nonnegative implies for n, m being Element of NAT holds (Ser F) . n <= (Ser F) . (n + m) ) reconsider N = F as Num of rng F by Def10; assume F is nonnegative ; ::_thesis: for n, m being Element of NAT holds (Ser F) . n <= (Ser F) . (n + m) then A1: rng F is Pos_Denum_Set_of_R_EAL by Def16; let n, m be Element of NAT ; ::_thesis: (Ser F) . n <= (Ser F) . (n + m) Ser F = Ser ((rng F),N) by Def15; hence (Ser F) . n <= (Ser F) . (n + m) by A1, Th37; ::_thesis: verum end; theorem Th42: :: SUPINF_2:42 for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds F1 . n <= F2 . n ) holds for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n proof let F1, F2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds F1 . n <= F2 . n ) implies for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n ) reconsider N2 = F2 as Num of rng F2 by Def10; defpred S1[ Element of NAT ] means (Ser F1) . \$1 <= (Ser F2) . \$1; reconsider N1 = F1 as Num of rng F1 by Def10; assume A1: for n being Element of NAT holds F1 . n <= F2 . n ; ::_thesis: for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n let n be Element of NAT ; ::_thesis: (Ser F1) . n <= (Ser F2) . n A2: Ser F2 = Ser ((rng F2),N2) by Def15; then A3: (Ser F2) . 0 = F2 . 0 by Def11; A4: Ser F1 = Ser ((rng F1),N1) by Def15; A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A6: (Ser F1) . k <= (Ser F2) . k ; ::_thesis: S1[k + 1] A7: F1 . (k + 1) <= F2 . (k + 1) by A1; A8: (Ser F2) . (k + 1) = ((Ser F2) . k) + (F2 . (k + 1)) by A2, Def11; (Ser F1) . (k + 1) = ((Ser F1) . k) + (F1 . (k + 1)) by A4, Def11; hence S1[k + 1] by A6, A8, A7, XXREAL_3:36; ::_thesis: verum end; (Ser F1) . 0 = F1 . 0 by A4, Def11; then A9: S1[ 0 ] by A1, A3; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A9, A5); hence (Ser F1) . n <= (Ser F2) . n ; ::_thesis: verum end; theorem Th43: :: SUPINF_2:43 for F1, F2 being Function of NAT,ExtREAL st ( for n being Element of NAT holds F1 . n <= F2 . n ) holds SUM F1 <= SUM F2 proof let F1, F2 be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds F1 . n <= F2 . n ) implies SUM F1 <= SUM F2 ) assume A1: for n being Element of NAT holds F1 . n <= F2 . n ; ::_thesis: SUM F1 <= SUM F2 for x being ext-real number st x in rng (Ser F1) holds ex y being ext-real number st ( y in rng (Ser F2) & x <= y ) proof let x be ext-real number ; ::_thesis: ( x in rng (Ser F1) implies ex y being ext-real number st ( y in rng (Ser F2) & x <= y ) ) A2: dom (Ser F1) = NAT by FUNCT_2:def_1; assume x in rng (Ser F1) ; ::_thesis: ex y being ext-real number st ( y in rng (Ser F2) & x <= y ) then consider n being set such that A3: n in NAT and A4: x = (Ser F1) . n by A2, FUNCT_1:def_3; reconsider n = n as Element of NAT by A3; reconsider y = (Ser F2) . n as R_eal ; take y ; ::_thesis: ( y in rng (Ser F2) & x <= y ) dom (Ser F2) = NAT by FUNCT_2:def_1; hence ( y in rng (Ser F2) & x <= y ) by A1, A4, Th42, FUNCT_1:def_3; ::_thesis: verum end; hence SUM F1 <= SUM F2 by XXREAL_2:63; ::_thesis: verum end; theorem Th44: :: SUPINF_2:44 for F being Function of NAT,ExtREAL holds ( (Ser F) . 0 = F . 0 & ( for n being Element of NAT for y being R_eal st y = (Ser F) . n holds (Ser F) . (n + 1) = y + (F . (n + 1)) ) ) proof let F be Function of NAT,ExtREAL; ::_thesis: ( (Ser F) . 0 = F . 0 & ( for n being Element of NAT for y being R_eal st y = (Ser F) . n holds (Ser F) . (n + 1) = y + (F . (n + 1)) ) ) reconsider N = F as Num of rng F by Def10; Ser F = Ser ((rng F),N) by Def15; hence ( (Ser F) . 0 = F . 0 & ( for n being Element of NAT for y being R_eal st y = (Ser F) . n holds (Ser F) . (n + 1) = y + (F . (n + 1)) ) ) by Def11; ::_thesis: verum end; theorem Th45: :: SUPINF_2:45 for F being Function of NAT,ExtREAL st F is nonnegative & ex n being Element of NAT st F . n = +infty holds SUM F = +infty proof let F be Function of NAT,ExtREAL; ::_thesis: ( F is nonnegative & ex n being Element of NAT st F . n = +infty implies SUM F = +infty ) assume A1: F is nonnegative ; ::_thesis: ( for n being Element of NAT holds not F . n = +infty or SUM F = +infty ) given n being Element of NAT such that A2: F . n = +infty ; ::_thesis: SUM F = +infty A3: ( ex k being Nat st n = k + 1 implies SUM F = +infty ) proof given k being Nat such that A4: n = k + 1 ; ::_thesis: SUM F = +infty reconsider k = k as Element of NAT by ORDINAL1:def_12; reconsider y = (Ser F) . k as R_eal ; reconsider x = (Ser F) . (k + 1) as R_eal ; A5: (Ser F) . (k + 1) = y + (F . (k + 1)) by Th44; (Ser F) . k <> -infty by A1, Th40, XXREAL_0:6; then A6: x = +infty by A2, A4, A5, XXREAL_3:def_2; then x is UpperBound of rng (Ser F) by XXREAL_2:41; hence SUM F = +infty by A6, FUNCT_2:4, XXREAL_2:55; ::_thesis: verum end; ( n = 0 implies SUM F = +infty ) proof reconsider x = (Ser F) . 0 as R_eal ; assume n = 0 ; ::_thesis: SUM F = +infty then A7: (Ser F) . 0 = +infty by A2, Th44; then x is UpperBound of rng (Ser F) by XXREAL_2:41; hence SUM F = +infty by A7, FUNCT_2:4, XXREAL_2:55; ::_thesis: verum end; hence SUM F = +infty by A3, NAT_1:6; ::_thesis: verum end; definition let F be Function of NAT,ExtREAL; attrF is summable means :Def18: :: SUPINF_2:def 18 SUM F in REAL ; end; :: deftheorem Def18 defines summable SUPINF_2:def_18_:_ for F being Function of NAT,ExtREAL holds ( F is summable iff SUM F in REAL ); theorem :: SUPINF_2:46 for F being Function of NAT,ExtREAL st F is nonnegative & ex n being Element of NAT st F . n = +infty holds not F is summable proof let F be Function of NAT,ExtREAL; ::_thesis: ( F is nonnegative & ex n being Element of NAT st F . n = +infty implies not F is summable ) assume A1: F is nonnegative ; ::_thesis: ( for n being Element of NAT holds not F . n = +infty or not F is summable ) assume ex n being Element of NAT st F . n = +infty ; ::_thesis: not F is summable then not SUM F in REAL by A1, Th45; hence not F is summable by Def18; ::_thesis: verum end; theorem :: SUPINF_2:47 for F1, F2 being Function of NAT,ExtREAL st F1 is nonnegative & ( for n being Element of NAT holds F1 . n <= F2 . n ) & F2 is summable holds F1 is summable proof let F1, F2 be Function of NAT,ExtREAL; ::_thesis: ( F1 is nonnegative & ( for n being Element of NAT holds F1 . n <= F2 . n ) & F2 is summable implies F1 is summable ) assume F1 is nonnegative ; ::_thesis: ( ex n being Element of NAT st not F1 . n <= F2 . n or not F2 is summable or F1 is summable ) then A1: 0. <= (Ser F1) . 0 by Th40; (Ser F1) . 0 <= sup (rng (Ser F1)) by FUNCT_2:4, XXREAL_2:4; then A2: SUM F1 <> -infty by A1, XXREAL_0:2, XXREAL_0:6; assume A3: for n being Element of NAT holds F1 . n <= F2 . n ; ::_thesis: ( not F2 is summable or F1 is summable ) assume F2 is summable ; ::_thesis: F1 is summable then SUM F2 in REAL by Def18; then A4: not SUM F1 = +infty by A3, Th43, XXREAL_0:9; ( SUM F1 in REAL or SUM F1 in {-infty,+infty} ) by XBOOLE_0:def_3; hence F1 is summable by A4, A2, Def18, TARSKI:def_2; ::_thesis: verum end; theorem Th48: :: SUPINF_2:48 for F being Function of NAT,ExtREAL st F is nonnegative holds for n being Nat st ( for r being Element of NAT st n <= r holds F . r = 0. ) holds SUM F = (Ser F) . n proof let F be Function of NAT,ExtREAL; ::_thesis: ( F is nonnegative implies for n being Nat st ( for r being Element of NAT st n <= r holds F . r = 0. ) holds SUM F = (Ser F) . n ) assume A1: F is nonnegative ; ::_thesis: for n being Nat st ( for r being Element of NAT st n <= r holds F . r = 0. ) holds SUM F = (Ser F) . n let n be Nat; ::_thesis: ( ( for r being Element of NAT st n <= r holds F . r = 0. ) implies SUM F = (Ser F) . n ) reconsider n9 = n as Element of NAT by ORDINAL1:def_12; assume A2: for r being Element of NAT st n <= r holds F . r = 0. ; ::_thesis: SUM F = (Ser F) . n A3: for r being Element of NAT st n <= r holds (Ser F) . r <= (Ser F) . n proof defpred S1[ Nat] means (Ser F) . (n + \$1) <= (Ser F) . n; let r be Element of NAT ; ::_thesis: ( n <= r implies (Ser F) . r <= (Ser F) . n ) assume n <= r ; ::_thesis: (Ser F) . r <= (Ser F) . n then A4: ex m being Nat st r = n + m by NAT_1:10; A5: for s being Nat st S1[s] holds S1[s + 1] proof let s be Nat; ::_thesis: ( S1[s] implies S1[s + 1] ) reconsider s9 = s as Element of NAT by ORDINAL1:def_12; reconsider y = (Ser F) . (n + s) as R_eal ; n9 + (s9 + 1) = (n9 + s9) + 1 ; then A6: (Ser F) . (n9 + (s9 + 1)) = y + (F . (n9 + (s9 + 1))) by Th44; 0 <= s + 1 by NAT_1:2; then n + 0 <= n + (s + 1) by XREAL_1:7; then A7: F . (n9 + (s9 + 1)) = 0. by A2; assume (Ser F) . (n + s) <= (Ser F) . n ; ::_thesis: S1[s + 1] hence S1[s + 1] by A6, A7, XXREAL_3:4; ::_thesis: verum end; A8: S1[ 0 ] ; for m being Nat holds S1[m] from NAT_1:sch_2(A8, A5); hence (Ser F) . r <= (Ser F) . n by A4; ::_thesis: verum end; A9: for r being Element of NAT st r <= n holds (Ser F) . r <= (Ser F) . n proof let r be Element of NAT ; ::_thesis: ( r <= n implies (Ser F) . r <= (Ser F) . n ) assume r <= n ; ::_thesis: (Ser F) . r <= (Ser F) . n then consider m being Nat such that A10: n = r + m by NAT_1:10; reconsider m = m as Element of NAT by ORDINAL1:def_12; n = r + m by A10; hence (Ser F) . r <= (Ser F) . n by A1, Th41; ::_thesis: verum end; for y being ext-real number st y in rng (Ser F) holds y <= (Ser F) . n proof let y be ext-real number ; ::_thesis: ( y in rng (Ser F) implies y <= (Ser F) . n ) A11: dom (Ser F) = NAT by FUNCT_2:def_1; assume y in rng (Ser F) ; ::_thesis: y <= (Ser F) . n then consider m being set such that A12: m in NAT and A13: y = (Ser F) . m by A11, FUNCT_1:def_3; reconsider m = m as Element of NAT by A12; ( m <= n or n <= m ) ; hence y <= (Ser F) . n by A3, A9, A13; ::_thesis: verum end; then A14: (Ser F) . n is UpperBound of rng (Ser F) by XXREAL_2:def_1; (Ser F) . n9 in rng (Ser F) by FUNCT_2:4; hence SUM F = (Ser F) . n by A14, XXREAL_2:55; ::_thesis: verum end; theorem Th49: :: SUPINF_2:49 for F being Function of NAT,ExtREAL st ( for n being Element of NAT holds F . n in REAL ) holds for n being Element of NAT holds (Ser F) . n in REAL proof let F be Function of NAT,ExtREAL; ::_thesis: ( ( for n being Element of NAT holds F . n in REAL ) implies for n being Element of NAT holds (Ser F) . n in REAL ) defpred S1[ Element of NAT ] means (Ser F) . \$1 in REAL ; assume A1: for n being Element of NAT holds F . n in REAL ; ::_thesis: for n being Element of NAT holds (Ser F) . n in REAL A2: for s being Element of NAT st S1[s] holds S1[s + 1] proof let s be Element of NAT ; ::_thesis: ( S1[s] implies S1[s + 1] ) reconsider b = F . (s + 1) as Real by A1; reconsider y = (Ser F) . s as R_eal ; assume (Ser F) . s in REAL ; ::_thesis: S1[s + 1] then reconsider a = y as Real ; A3: y + (F . (s + 1)) = a + b by XXREAL_3:def_2; (Ser F) . (s + 1) = y + (F . (s + 1)) by Th44; hence S1[s + 1] by A3; ::_thesis: verum end; (Ser F) . 0 = F . 0 by Th44; then A4: S1[ 0 ] by A1; thus for s being Element of NAT holds S1[s] from NAT_1:sch_1(A4, A2); ::_thesis: verum end; theorem :: SUPINF_2:50 for F being Function of NAT,ExtREAL st F is nonnegative & ex n being Element of NAT st ( ( for k being Element of NAT st n <= k holds F . k = 0. ) & ( for k being Element of NAT st k <= n holds F . k <> +infty ) ) holds F is summable proof let F be Function of NAT,ExtREAL; ::_thesis: ( F is nonnegative & ex n being Element of NAT st ( ( for k being Element of NAT st n <= k holds F . k = 0. ) & ( for k being Element of NAT st k <= n holds F . k <> +infty ) ) implies F is summable ) assume A1: F is nonnegative ; ::_thesis: ( for n being Element of NAT holds ( ex k being Element of NAT st ( n <= k & not F . k = 0. ) or ex k being Element of NAT st ( k <= n & not F . k <> +infty ) ) or F is summable ) given n being Element of NAT such that A2: for k being Element of NAT st n <= k holds F . k = 0. and A3: for k being Element of NAT st k <= n holds F . k <> +infty ; ::_thesis: F is summable for s being Element of NAT holds F . s in REAL proof let s be Element of NAT ; ::_thesis: F . s in REAL A4: ( s <= n implies F . s in REAL ) proof 0. <= F . s by A1, Th39; then A5: F . s <> -infty by XXREAL_0:6; assume s <= n ; ::_thesis: F . s in REAL then A6: not F . s = +infty by A3; ( F . s in REAL or F . s in {-infty,+infty} ) by XBOOLE_0:def_3; hence F . s in REAL by A6, A5, TARSKI:def_2; ::_thesis: verum end; ( n <= s implies F . s in REAL ) proof assume n <= s ; ::_thesis: F . s in REAL then F . s = 0. by A2; hence F . s in REAL ; ::_thesis: verum end; hence F . s in REAL by A4; ::_thesis: verum end; then A7: (Ser F) . n in REAL by Th49; SUM F = (Ser F) . n by A1, A2, Th48; hence F is summable by A7, Def18; ::_thesis: verum end; theorem :: SUPINF_2:51 for X being set for F being PartFunc of X,ExtREAL holds ( F is nonnegative iff for n being set holds 0. <= F . n ) proof let X be set ; ::_thesis: for F being PartFunc of X,ExtREAL holds ( F is nonnegative iff for n being set holds 0. <= F . n ) let F be PartFunc of X,ExtREAL; ::_thesis: ( F is nonnegative iff for n being set holds 0. <= F . n ) hereby ::_thesis: ( ( for n being set holds 0. <= F . n ) implies F is nonnegative ) assume F is nonnegative ; ::_thesis: for n being set holds 0. <= F . b2 then A1: rng F is nonnegative by Def16; let n be set ; ::_thesis: 0. <= F . b1 percases ( n in dom F or not n in dom F ) ; suppose n in dom F ; ::_thesis: 0. <= F . b1 then F . n in rng F by FUNCT_1:def_3; hence 0. <= F . n by A1, Def9; ::_thesis: verum end; suppose not n in dom F ; ::_thesis: 0. <= F . b1 hence 0. <= F . n by FUNCT_1:def_2; ::_thesis: verum end; end; end; assume A2: for n being set holds 0. <= F . n ; ::_thesis: F is nonnegative let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( y in rng F implies 0. <= y ) assume y in rng F ; ::_thesis: 0. <= y then ex x being set st ( x in dom F & y = F . x ) by FUNCT_1:def_3; hence 0. <= y by A2; ::_thesis: verum end; theorem :: SUPINF_2:52 for X being set for F being PartFunc of X,ExtREAL st ( for n being set st n in dom F holds 0. <= F . n ) holds F is nonnegative proof let X be set ; ::_thesis: for F being PartFunc of X,ExtREAL st ( for n being set st n in dom F holds 0. <= F . n ) holds F is nonnegative let F be PartFunc of X,ExtREAL; ::_thesis: ( ( for n being set st n in dom F holds 0. <= F . n ) implies F is nonnegative ) assume A1: for n being set st n in dom F holds 0. <= F . n ; ::_thesis: F is nonnegative let y be R_eal; :: according to SUPINF_2:def_9,SUPINF_2:def_16 ::_thesis: ( y in rng F implies 0. <= y ) assume y in rng F ; ::_thesis: 0. <= y then ex x being set st ( x in dom F & y = F . x ) by FUNCT_1:def_3; hence 0. <= y by A1; ::_thesis: verum end;