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

::

:: Received September 27, 1990

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

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;

::$CT

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

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

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 Th15: :: 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 Th16: :: 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 Th17: :: 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 Th18: :: 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 Th19: :: 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

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

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
;

end;
let Y be Subset of ExtREAL;

coherence

for b

( b

coherence

for b

b

theorem :: SUPINF_2:21

theorem Th21: :: 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 Th22: :: 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

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 Th26: :: 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 Th27: :: 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 Th28: :: 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

theorem Th30: :: 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 Th31: :: 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

theorem Th33: :: SUPINF_2:34

( id NAT is sequence of ExtREAL & id NAT is one-to-one & NAT = rng (id NAT) & rng (id NAT) is non empty Subset of ExtREAL )

proof end;

definition

let D be non empty set ;

let IT be Subset of D;

( IT is countable iff ( IT is empty or ex F being sequence of 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 sequence of D st IT = rng F );

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

( IT is empty or ex F being sequence of D st IT = rng F );

( IT is countable iff ( IT is empty or ex F being sequence of 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 sequence of 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 sequence of D st IT = rng F ) );

registration
end;

:: deftheorem defines nonnegative SUPINF_2:def 9 :

for IT being set holds

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

0. <= x );

for IT being set holds

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

0. <= x );

registration
end;

canceled;

::$CD

:: Series of Elements of extended real numbers

:: Series of Elements of extended real numbers

definition

let F be sequence of ExtREAL;

:: original: rng

redefine func rng F -> non empty Subset of ExtREAL;

coherence

rng F is non empty Subset of ExtREAL

end;
:: original: rng

redefine func rng F -> non empty Subset of ExtREAL;

coherence

rng F is non empty Subset of ExtREAL

proof end;

definition

let N be sequence of ExtREAL;

ex b_{1} being sequence of ExtREAL st

( b_{1} . 0 = N . 0 & ( for n being 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 sequence of ExtREAL st b_{1} . 0 = N . 0 & ( for n being 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 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;
func Ser N -> sequence of ExtREAL means :Def11: :: SUPINF_2:def 10

( it . 0 = N . 0 & ( for n being 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 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 10 :

for N, b_{2} being sequence of ExtREAL holds

( b_{2} = Ser N iff ( b_{2} . 0 = N . 0 & ( for n being Nat

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

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

for N, b

( b

for y being R_eal st y = b

b

::$CT 4

definition
end;

:: deftheorem defines nonnegative SUPINF_2:def 11 :

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

for F being sequence of ExtREAL holds SUM F = sup (rng (Ser F));

for F being sequence of ExtREAL holds SUM F = sup (rng (Ser F));

theorem Th38: :: 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 Th39: :: SUPINF_2:40

for F being sequence of ExtREAL

for n being Nat st F is nonnegative holds

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

for n being Nat st F is nonnegative holds

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

proof end;

theorem Th40: :: SUPINF_2:41

for F being sequence of ExtREAL st F is nonnegative holds

for n, m being Nat holds (Ser F) . n <= (Ser F) . (n + m)

for n, m being Nat holds (Ser F) . n <= (Ser F) . (n + m)

proof end;

theorem Th41: :: SUPINF_2:42

for F1, F2 being sequence of 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 Th42: :: SUPINF_2:43

for F1, F2 being sequence of ExtREAL st ( for n being Element of NAT holds F1 . n <= F2 . n ) holds

SUM F1 <= SUM F2

SUM F1 <= SUM F2

proof end;

::$CT

theorem Th44: :: SUPINF_2:45

for F being sequence of ExtREAL st F is nonnegative & ex n being Element of NAT st F . n = +infty holds

SUM F = +infty

SUM F = +infty

proof end;

definition
end;

:: deftheorem defines summable SUPINF_2:def 13 :

for F being sequence of ExtREAL holds

( F is summable iff SUM F in REAL );

for F being sequence of ExtREAL holds

( F is summable iff SUM F in REAL );

theorem :: SUPINF_2:46

theorem :: SUPINF_2:47

for F1, F2 being sequence of 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 Th47: :: SUPINF_2:48

for F being sequence of 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 Th48: :: SUPINF_2:49

for F being sequence of ExtREAL st ( for n being Element of NAT holds F . n in REAL ) holds

for n being Nat holds (Ser F) . n in REAL

for n being Nat holds (Ser F) . n in REAL

proof end;

theorem :: SUPINF_2:50

for F being sequence of 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 object holds 0. <= F . n )

for F being PartFunc of X,ExtREAL holds

( F is nonnegative iff for n being object 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 object st n in dom F holds

0. <= F . n ) holds

F is nonnegative

for F being PartFunc of X,ExtREAL st ( for n being object st n in dom F holds

0. <= F . n ) holds

F is nonnegative

proof end;

definition
end;