:: by J\'ozef Bia{\l}as

::

:: Received September 27, 1990

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

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 func x + y -> R_eal;

coherence

x + y is R_eal by XXREAL_0:def 1;

:: original: -

redefine func x - y -> R_eal;

coherence

x - y is R_eal by XXREAL_0:def 1;

end;
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 func x + y -> R_eal;

coherence

x + y is R_eal by XXREAL_0:def 1;

:: original: -

redefine func x - y -> R_eal;

coherence

x - y is R_eal by XXREAL_0:def 1;

theorem :: SUPINF_2:1

theorem :: SUPINF_2:2

definition

let X, Y be Subset of ExtREAL;

:: original: +

redefine func X + Y -> Subset of ExtREAL;

coherence

X + Y is Subset of ExtREAL by MEMBERED:2;

end;
:: original: +

redefine func X + Y -> Subset of ExtREAL;

coherence

X + Y is Subset of ExtREAL by MEMBERED:2;

definition

let X be Subset of ExtREAL;

:: original: -

redefine func - X -> Subset of ExtREAL;

coherence

- X is Subset of ExtREAL by MEMBERED:2;

end;
:: original: -

redefine func - X -> Subset of ExtREAL;

coherence

- X is Subset of ExtREAL by MEMBERED:2;

theorem :: SUPINF_2:5

theorem :: SUPINF_2:6

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;
:: 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;

theorem :: SUPINF_2:10

theorem :: SUPINF_2:11

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 )

for a being R_eal holds

( a is UpperBound of X iff - a is LowerBound of - X )

proof 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 )

for a being R_eal holds

( a is LowerBound of X iff - a is UpperBound of - X )

proof 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

end;
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 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;

coherence

sup (rng F) is Element of ExtREAL ;

coherence

inf (rng F) is Element of ExtREAL ;

end;
let X be set ;

let Y be Subset of D;

let F be PartFunc of X,Y;

coherence

sup (rng F) is Element of ExtREAL ;

coherence

inf (rng F) is Element of ExtREAL ;

:: 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);

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);

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 func F . x -> R_eal;

coherence

F . x is R_eal by XXREAL_0:def 1;

end;
let x be set ;

:: original: .

redefine func F . x -> R_eal;

coherence

F . x is R_eal by XXREAL_0:def 1;

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;

ex b_{1} being Function of X,(Y + Z) st

for x being Element of X holds b_{1} . x = (F . x) + (G . x)

for b_{1}, b_{2} being Function of X,(Y + Z) st ( for x being Element of X holds b_{1} . x = (F . x) + (G . x) ) & ( for x being Element of X holds b_{2} . x = (F . x) + (G . x) ) holds

b_{1} = b_{2}

end;
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 :Def3: :: SUPINF_2:def 3

for x being Element of X holds it . x = (F . x) + (G . x);

existence for x being Element of X holds it . x = (F . x) + (G . x);

ex b

for x being Element of X holds b

proof end;

uniqueness for b

b

proof 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 b_{6} being Function of X,(Y + Z) holds

( b_{6} = F + G iff for x being Element of X holds b_{6} . x = (F . x) + (G . x) );

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 b

( b

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)

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 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)

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 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)

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 end;

definition

let X be non empty set ;

let Y be non empty Subset of ExtREAL;

let F be Function of X,Y;

ex b_{1} being Function of X,(- Y) st

for x being Element of X holds b_{1} . x = - (F . x)

for b_{1}, b_{2} being Function of X,(- Y) st ( for x being Element of X holds b_{1} . x = - (F . x) ) & ( for x being Element of X holds b_{2} . x = - (F . x) ) holds

b_{1} = b_{2}

end;
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 for x being Element of X holds it . x = - (F . x);

ex b

for x being Element of X holds b

proof end;

uniqueness for b

b

proof 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 b_{4} being Function of X,(- Y) holds

( b_{4} = - F iff for x being Element of X holds b_{4} . x = - (F . x) );

for X being non empty set

for Y being non empty Subset of ExtREAL

for F being Function of X,Y

for b

( b

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)

for Y being non empty Subset of ExtREAL

for F being Function of X,Y holds rng (- F) = - (rng F)

proof 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) )

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 end;

::

:: Bounded Function of X,ExtREAL

::

:: Bounded Function of X,ExtREAL

::

:: 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 );

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 );

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 );

:: 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 ) );

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;

coherence

for b_{1} being Function of X,Y st b_{1} is bounded holds

( b_{1} is bounded_above & b_{1} is bounded_below )
by Def7;

coherence

for b_{1} being Function of X,Y st b_{1} is bounded_above & b_{1} is bounded_below holds

b_{1} is bounded
by Def7;

end;
let Y be Subset of ExtREAL;

coherence

for b

( b

coherence

for b

b

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 ) )

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 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 )

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 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 )

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 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 )

for Y being non empty Subset of ExtREAL

for F being Function of X,Y holds

( F is bounded iff - F is bounded )

proof end;

theorem :: SUPINF_2:25

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 )

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 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 )

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 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 )

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 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 )

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 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 ) )

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 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

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 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

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 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

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 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 end;

::

:: Series of Elements of ExtREAL numbers

::

:: Series of Elements of ExtREAL numbers

::

definition

let D be non empty set ;

let IT be Subset of D;

( IT is countable iff ( IT is empty or ex F being Function of NAT,D st IT = rng F ) )

end;
let IT be Subset of D;

:: original: countable

redefine attr IT is countable means :Def8: :: SUPINF_2:def 8

( IT is empty or ex F being Function of NAT,D st IT = rng F );

compatibility redefine attr IT is countable means :Def8: :: SUPINF_2:def 8

( IT is empty or ex F being Function of NAT,D st IT = rng F );

( IT is countable iff ( IT is empty or ex F being Function of NAT,D st IT = rng F ) )

proof 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 ) );

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
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 );

for IT being set holds

( IT is nonnegative iff for x being R_eal st x in IT holds

0. <= x );

definition

let D be Denum_Set_of_R_EAL;

existence

ex b_{1} being Function of NAT,ExtREAL st D = rng b_{1}
by Def8;

end;
existence

ex b

:: deftheorem Def10 defines Num SUPINF_2:def 10 :

for D being Denum_Set_of_R_EAL

for b_{2} being Function of NAT,ExtREAL holds

( b_{2} is Num of D iff D = rng b_{2} );

for D being Denum_Set_of_R_EAL

for b

( b

definition

let D be Denum_Set_of_R_EAL;

let N be Num of D;

ex b_{1} being Function of NAT,ExtREAL st

( b_{1} . 0 = N . 0 & ( for n being Element of NAT

for y being R_eal st y = b_{1} . n holds

b_{1} . (n + 1) = y + (N . (n + 1)) ) )

for b_{1}, b_{2} being Function of NAT,ExtREAL st b_{1} . 0 = N . 0 & ( for n being Element of NAT

for y being R_eal st y = b_{1} . n holds

b_{1} . (n + 1) = y + (N . (n + 1)) ) & b_{2} . 0 = N . 0 & ( for n being Element of NAT

for y being R_eal st y = b_{2} . n holds

b_{2} . (n + 1) = y + (N . (n + 1)) ) holds

b_{1} = b_{2}

end;
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 ( 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)) ) );

ex b

( b

for y being R_eal st y = b

b

proof end;

uniqueness for b

for y being R_eal st y = b

b

for y being R_eal st y = b

b

b

proof end;

:: deftheorem Def11 defines Ser SUPINF_2:def 11 :

for D being Denum_Set_of_R_EAL

for N being Num of D

for b_{3} being Function of NAT,ExtREAL holds

( b_{3} = Ser (D,N) iff ( b_{3} . 0 = N . 0 & ( for n being Element of NAT

for y being R_eal st y = b_{3} . n holds

b_{3} . (n + 1) = y + (N . (n + 1)) ) ) );

for D being Denum_Set_of_R_EAL

for N being Num of D

for b

( b

for y being R_eal st y = b

b

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

for N being Num of D

for n being Element of NAT holds 0. <= N . n

proof 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 )

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 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)

for N being Num of D

for n, m being Element of NAT holds (Ser (D,N)) . n <= (Ser (D,N)) . (n + m)

proof end;

definition

let D be Denum_Set_of_R_EAL;

ex b_{1} being non empty Subset of ExtREAL ex N being Num of D st b_{1} = rng (Ser (D,N))

end;
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 N being Num of D st it = rng (Ser (D,N));

ex b

proof end;

:: deftheorem defines Set_of_Series SUPINF_2:def 12 :

for D being Denum_Set_of_R_EAL

for b_{2} being non empty Subset of ExtREAL holds

( b_{2} is Set_of_Series of D iff ex N being Num of D st b_{2} = rng (Ser (D,N)) );

for D being Denum_Set_of_R_EAL

for b

( b

definition
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)));

for D being Pos_Denum_Set_of_R_EAL

for N being Num of D holds SUM (D,N) = sup (rng (Ser (D,N)));

:: 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 );

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 );

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;
:: original: rng

redefine func rng F -> Denum_Set_of_R_EAL;

coherence

rng F is Denum_Set_of_R_EAL by Th38;

definition

let F be Function of NAT,ExtREAL;

ex b_{1} being Function of NAT,ExtREAL st

for N being Num of rng F st N = F holds

b_{1} = Ser ((rng F),N)

for b_{1}, b_{2} being Function of NAT,ExtREAL st ( for N being Num of rng F st N = F holds

b_{1} = Ser ((rng F),N) ) & ( for N being Num of rng F st N = F holds

b_{2} = Ser ((rng F),N) ) holds

b_{1} = b_{2}

end;
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 for N being Num of rng F st N = F holds

it = Ser ((rng F),N);

ex b

for N being Num of rng F st N = F holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def15 defines Ser SUPINF_2:def 15 :

for F, b_{2} being Function of NAT,ExtREAL holds

( b_{2} = Ser F iff for N being Num of rng F st N = F holds

b_{2} = Ser ((rng F),N) );

for F, b

( b

b

definition
end;

:: deftheorem Def16 defines nonnegative SUPINF_2:def 16 :

for R being Relation holds

( R is nonnegative iff rng R is nonnegative );

for R being Relation holds

( R is nonnegative iff rng R is nonnegative );

:: deftheorem defines SUM SUPINF_2:def 17 :

for F being Function of NAT,ExtREAL holds SUM F = sup (rng (Ser F));

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 )

for F being PartFunc of X,ExtREAL holds

( F is nonnegative iff for n being Element of X holds 0. <= F . n )

proof 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 )

for n being Element of NAT st F is nonnegative holds

( (Ser F) . n <= (Ser F) . (n + 1) & 0. <= (Ser F) . n )

proof 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)

for n, m being Element of NAT holds (Ser F) . n <= (Ser F) . (n + m)

proof 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

for n being Element of NAT holds (Ser F1) . n <= (Ser F2) . n

proof 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

SUM F1 <= SUM F2

proof 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)) ) )

( (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 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

SUM F = +infty

proof 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 );

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

not F is summable

proof 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

F1 is summable

proof 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

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 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

for n being Element of NAT holds (Ser F) . n in REAL

proof 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

( ( 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 end;

:: Added by AK, 2006.02.06

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 )

for F being PartFunc of X,ExtREAL holds

( F is nonnegative iff for n being set holds 0. <= F . n )

proof 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

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 end;

:: sup F and inf F for Function of X,ExtREAL

::