Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

The abstract of the Mizar article:

Series of Positive Real Numbers. Measure Theory

by
Jozef Bialas

Received September 27, 1990

MML identifier: SUPINF_2
[ Mizar article, MML identifier index ]


environ

 vocabulary SUPINF_1, ARYTM_1, ARYTM_3, RLVECT_1, BOOLE, ORDINAL2, SEQ_2,
      FUNCT_1, RELAT_1, LATTICES, CARD_4, FUNCT_4, FUNCOP_1, SUPINF_2;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, REAL_1, SUPINF_1,
      RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FUNCT_4, NAT_1, CARD_4;
 constructors REAL_1, SUPINF_1, NAT_1, CARD_4, FUNCOP_1, FUNCT_4, MEMBERED,
      XBOOLE_0;
 clusters SUPINF_1, RELSET_1, FUNCOP_1, FUNCT_1, ARYTM_3, FINSET_1, MEMBERED,
      ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: operations " + "," - " in R_eal numbers

definition
   func 0. -> R_eal equals
:: SUPINF_2:def 1
 0;
end;

definition
  let x,y be R_eal;
func x + y -> R_eal means
:: SUPINF_2:def 2

  ex a,b being Real st x = a & y = b & it = a + b if x in REAL & y in REAL,
  it = +infty if x = +infty & y <> -infty or y = +infty & x <> -infty,
  it = -infty if x = -infty & y <> +infty or y = -infty & x <> +infty
  otherwise it = 0.;
 commutativity;
end;

theorem :: SUPINF_2:1
   for x,y being R_eal holds
   for a,b being Real holds
   (x = a & y = b) implies (x + y = a + b);

theorem :: SUPINF_2:2
 for x being R_eal holds
  x in REAL or x = +infty or x = -infty;

definition
   let x be R_eal;
   func - x -> R_eal means
:: SUPINF_2:def 3
 ex a being Real st x = a & it = - a if x in REAL,
     it = -infty if x = +infty
     otherwise it = +infty;
 involutiveness;
end;

definition
  let x,y be R_eal;
func x - y -> R_eal equals
:: SUPINF_2:def 4
 x + -y;
end;

theorem :: SUPINF_2:3
   for x being R_eal, a being Real st x = a holds - x = - a;

theorem :: SUPINF_2:4
 - -infty = +infty;

theorem :: SUPINF_2:5
   for x,y being R_eal holds
   for a,b being Real holds
   (x = a & y = b) implies (x - y = a - b);

theorem :: SUPINF_2:6
   for x being R_eal holds
    x <> +infty implies +infty - x = +infty & x - +infty = -infty;

theorem :: SUPINF_2:7
   for x being R_eal holds
    x <> -infty implies -infty - x = -infty & x - -infty = +infty;

theorem :: SUPINF_2:8
   for x,s being R_eal holds
   x + s = +infty implies x = +infty or s = +infty;

theorem :: SUPINF_2:9
   for x,s being R_eal holds
   x + s = -infty implies (x = -infty or s = -infty);

theorem :: SUPINF_2:10
   for x,s being R_eal holds
   x - s = +infty implies (x = +infty or s = -infty);

theorem :: SUPINF_2:11
   for x,s being R_eal holds
   x - s = -infty implies (x = -infty or s = +infty);

theorem :: SUPINF_2:12
   for x,s being R_eal holds
   (not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) &
   x + s in REAL) implies (x in REAL & s in REAL);

theorem :: SUPINF_2:13
   for x,s being R_eal holds
   (not ((x = +infty & s = +infty) or (x = -infty & s = -infty)) &
   x - s in REAL) implies (x in REAL & s in REAL);

theorem :: SUPINF_2:14
   for x,y,s,t being R_eal holds
   not ((x = +infty & s = -infty) or (x = -infty & s = +infty)) &
   not ((y = +infty & t = -infty) or (y = -infty & t = +infty
)) & x <=' y & s <=' t implies
   x + s <=' y + t;

theorem :: SUPINF_2:15
     for x,y,s,t being R_eal holds
   not ((x = +infty & t = +infty) or (x = -infty & t = -infty)) &
   not ((y = +infty & s = +infty) or (y = -infty & s = -infty
)) & x <=' y & s <=' t implies
   x - t <=' y - s;

theorem :: SUPINF_2:16
   for x,y being R_eal holds
   x <=' y iff - y <=' - x;

theorem :: SUPINF_2:17
    for x,y being R_eal holds
   x <' y iff - y <' - x;

theorem :: SUPINF_2:18
   for x being R_eal holds x + 0. = x & 0. + x = x;

theorem :: SUPINF_2:19
     -infty <'0. & 0. <'+infty;

theorem :: SUPINF_2:20
   for x,y,z being R_eal holds
   0. <=' z & 0. <=' x & y = x + z implies x <=' y;

theorem :: SUPINF_2:21
   for x being R_eal holds x in NAT implies 0. <=' x;

::
::       operations " + "," - " in SUBDOMAIN of ExtREAL
::

definition
   let X,Y be non empty Subset of ExtREAL;
   func X + Y -> Subset of ExtREAL means
:: SUPINF_2:def 5
for z being R_eal holds
         z in it iff ex x,y being R_eal st (x in X & y in Y & z = x + y);
end;

definition
   let X,Y be non empty Subset of ExtREAL;
   cluster X + Y -> non empty;
end;

definition
   let X be non empty Subset of ExtREAL;
   func - X -> Subset of ExtREAL means
:: SUPINF_2:def 6
for z being R_eal holds
         z in it iff ex x being R_eal st (x in X & z = - x);
end;

definition
   let X be non empty Subset of ExtREAL;
   cluster - X -> non empty;
end;

theorem :: SUPINF_2:22
   for X being non empty Subset of ExtREAL holds
   - (- X) = X;

theorem :: SUPINF_2:23
   for X being non empty Subset of ExtREAL holds
   for z being R_eal holds
   z in X iff - z in - X;

theorem :: SUPINF_2:24
     for X,Y being non empty Subset of ExtREAL holds
   X c= Y iff - X c= - Y;

theorem :: SUPINF_2:25
     for z being R_eal holds
   z in REAL iff - z in REAL;

theorem :: SUPINF_2:26
   for X,Y being non empty Subset of ExtREAL holds
   (not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
   not(sup X = +infty & sup Y = -infty or sup X = -infty & sup Y = +infty
)) implies
   sup (X + Y) <=' sup X + sup Y;

theorem :: SUPINF_2:27
   for X,Y being non empty Subset of ExtREAL holds
   (not(-infty in X & +infty in Y or +infty in X & -infty in Y) &
    not(inf X = +infty & inf Y = -infty or inf X = -infty & inf Y = +infty
)) implies
   inf X + inf Y <=' inf (X + Y);

theorem :: SUPINF_2:28
     for X,Y being non empty Subset of ExtREAL holds
   X is bounded_above & Y is bounded_above implies
   sup (X + Y) <=' sup X + sup Y;

theorem :: SUPINF_2:29
     for X,Y being non empty Subset of ExtREAL holds
   X is bounded_below & Y is bounded_below implies
   inf X + inf Y <=' inf (X + Y);

theorem :: SUPINF_2:30
   for X being non empty Subset of ExtREAL holds
   for a being R_eal holds
   a is majorant of X iff - a is minorant of - X;

theorem :: SUPINF_2:31
   for X being non empty Subset of ExtREAL holds
   for a being R_eal holds
   a is minorant of X iff - a is majorant of - X;

theorem :: SUPINF_2:32
   for X being non empty Subset of ExtREAL holds
   inf(- X) = - sup X;

theorem :: SUPINF_2:33
   for X be non empty Subset of ExtREAL holds
   sup(- X) = - inf X;

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   redefine func rng F -> non empty Subset of ExtREAL;
end;

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

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   func sup F -> R_eal equals
:: SUPINF_2:def 7
 sup(rng F);
end;

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   func inf F -> R_eal equals
:: SUPINF_2:def 8
 inf(rng F);
end;

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   let x be Element of X;
   redefine func F.x -> R_eal;
end;

scheme FunctR_ealEx{X()->non empty set,Y()->set,F(set)->set}:
   ex f being Function of X(),Y() st
   for x being Element of X() holds f.x = F(x)
   provided
for x being Element of X() holds F(x) in Y();

definition
   let X be non empty set;
   let Y,Z be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   let G be Function of X,Z;
   func F + G -> Function of X,Y + Z means
:: SUPINF_2:def 9
 for x being Element of X holds it.x = F.x + G.x;
end;

theorem :: SUPINF_2:34
   for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL holds
   for F being Function of X,Y for G being Function of X,Z holds
   rng(F + G) c= rng F + rng G;

theorem :: SUPINF_2:35
   for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL st
   not(-infty in Y & +infty in Z or +infty in Y & -infty in Z) holds
   for F being Function of X,Y for G being Function of X,Z st
   not(sup F = +infty & sup G = -infty or sup F = -infty & sup G = +infty
) holds
   sup(F + G) <=' sup F + sup G;

theorem :: SUPINF_2:36
   for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL st
   not(-infty in Y & +infty in Z or +infty in Y & -infty in Z) holds
   for F being Function of X,Y for G being Function of X,Z st
   not(inf F = +infty & inf G = -infty or inf F = -infty & inf G = +infty
) holds
   inf F + inf G <=' inf(F + G);

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   func - F -> Function of X,- Y means
:: SUPINF_2:def 10
 for x being Element of X holds it.x = - F.x;
end;

theorem :: SUPINF_2:37
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   rng(- F) = - rng F;

theorem :: SUPINF_2:38
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   inf(- F) = - sup F & sup(- F) = - inf F;

::
::       Bounded Function of X,ExtREAL
::

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   attr F is bounded_above means
:: SUPINF_2:def 11
sup F <'+infty;
end;

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   attr F is bounded_below means
:: SUPINF_2:def 12
-infty <'inf F;
end;

definition
   let X be non empty set;
   let Y be non empty Subset of ExtREAL;
   let F be Function of X,Y;
   attr F is bounded means
:: SUPINF_2:def 13
F is bounded_above & F is bounded_below;
end;

definition let X be non empty set;
           let Y be non empty Subset of ExtREAL;
  cluster bounded -> bounded_above bounded_below Function of X, Y;
  cluster bounded_above bounded_below -> bounded Function of X, Y;
end;

theorem :: SUPINF_2:39
     for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   F is bounded iff sup F <'+infty & -infty <'inf F;

theorem :: SUPINF_2:40
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   F is bounded_above iff - F is bounded_below;

theorem :: SUPINF_2:41
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   F is bounded_below iff - F is bounded_above;

theorem :: SUPINF_2:42
     for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   F is bounded iff - F is bounded;

theorem :: SUPINF_2:43
     for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   for x being Element of X holds
   -infty <=' F.x & F.x <=' +infty;

theorem :: SUPINF_2:44
     for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   for x being Element of X holds
   Y c= REAL implies -infty <'F.x & F.x <'+infty;

theorem :: SUPINF_2:45
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   for x being Element of X holds
   inf F <=' F.x & F.x <=' sup F;

theorem :: SUPINF_2:46
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   Y c= REAL implies (F is bounded_above iff sup F in REAL);

theorem :: SUPINF_2:47
   for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   Y c= REAL implies (F is bounded_below iff inf F in REAL);

theorem :: SUPINF_2:48
     for X being non empty set holds
   for Y being non empty Subset of ExtREAL holds
   for F being Function of X,Y holds
   Y c= REAL implies (F is bounded iff inf F in REAL & sup F in REAL);

theorem :: SUPINF_2:49
   for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
   for F1 being Function of X,Y holds
   for F2 being Function of X,Z holds
   F1 is bounded_above & F2 is bounded_above implies F1 + F2 is bounded_above;

theorem :: SUPINF_2:50
   for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
   for F1 being Function of X,Y holds
   for F2 being Function of X,Z holds
   F1 is bounded_below & F2 is bounded_below implies F1 + F2 is bounded_below;

theorem :: SUPINF_2:51
     for X being non empty set holds
   for Y,Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
   for F1 being Function of X,Y holds
   for F2 being Function of X,Z holds
   F1 is bounded & F2 is bounded implies F1 + F2 is bounded;

theorem :: SUPINF_2:52
   ex F being Function of NAT,ExtREAL st (F is one-to-one & NAT = rng F &
   rng F is non empty Subset of ExtREAL);

::
::       Series of Elements of ExtREAL numbers
::

definition let D be non empty set; let IT be Subset of D;
 redefine attr IT is countable means
:: SUPINF_2:def 14
 IT is empty or ex F being Function of NAT,D st IT = rng F;
 synonym IT is denumerable;
end;

definition
 cluster denumerable (non empty Subset of ExtREAL);
end;

definition
   mode Denum_Set_of_R_EAL is denumerable non empty Subset of ExtREAL;
end;

definition let IT be set;
   attr IT is nonnegative means
:: SUPINF_2:def 15
for x being R_eal holds x in IT implies 0. <=' x;
end;

definition
   cluster nonnegative Denum_Set_of_R_EAL;
end;

definition
   mode Pos_Denum_Set_of_R_EAL is nonnegative Denum_Set_of_R_EAL;
end;

definition
   let D be Denum_Set_of_R_EAL;
   mode Num of D -> Function of NAT,ExtREAL means
:: SUPINF_2:def 16
D = rng it;
end;

definition
   let N be Function of NAT,ExtREAL;
   let n be Nat;
redefine func N.n -> R_eal;
end;

theorem :: SUPINF_2:53
   for D being Denum_Set_of_R_EAL holds
   for N being Num of D holds
   ex F being Function of NAT,ExtREAL st
   F.0 = N.0 &
   for n being Nat,
   y being R_eal st y = F.n holds
   F.(n + 1) = y + N.(n+1);

definition
   let D be Denum_Set_of_R_EAL;
   let N be Num of D;
   func Ser(D,N) -> Function of NAT,ExtREAL means
:: SUPINF_2:def 17
it.0 = N.0 &
   for n being Nat holds
   for y being R_eal st y = it.n holds
   it.(n + 1) = y + N.(n + 1);
end;

theorem :: SUPINF_2:54
   for D being Pos_Denum_Set_of_R_EAL holds
   for N being Num of D holds
   for n being Nat holds 0. <=' N.n;

theorem :: SUPINF_2:55
   for D being Pos_Denum_Set_of_R_EAL holds
   for N being Num of D holds
   for n being Nat holds
   Ser(D,N).n <=' Ser(D,N).(n + 1) & 0. <=' Ser(D,N).n;

theorem :: SUPINF_2:56
   for D being Pos_Denum_Set_of_R_EAL holds
   for N being Num of D holds
   for n,m being Nat holds
   Ser(D,N).n <=' Ser(D,N).(n + m);

definition
   let D be Denum_Set_of_R_EAL;
   mode Set_of_Series of D -> non empty Subset of ExtREAL means
:: SUPINF_2:def 18
   ex N being Num of D st it = rng Ser(D,N);
end;

definition
   let F be Function of NAT,ExtREAL;
redefine func rng F -> non empty Subset of ExtREAL;
end;

definition
   let D be Pos_Denum_Set_of_R_EAL;
   let N be Num of D;
   func SUM(D,N) -> R_eal equals
:: SUPINF_2:def 19
    sup(rng Ser(D,N));
end;

definition
   let D be Pos_Denum_Set_of_R_EAL;
   let N be Num of D;
   pred D is_sumable N means
:: SUPINF_2:def 20
    SUM(D,N) in REAL;
end;

theorem :: SUPINF_2:57
   for F being Function of NAT,ExtREAL holds
   rng F is Denum_Set_of_R_EAL;

definition
   let F be Function of NAT,ExtREAL;
  redefine func rng F -> Denum_Set_of_R_EAL;
end;

definition
   let F be Function of NAT,ExtREAL;
   func Ser(F) -> Function of NAT,ExtREAL means
:: SUPINF_2:def 21
 for N being Num of rng F st N = F holds it = Ser(rng F,N);
end;

definition let X be set;
   let F be Function of X,ExtREAL;
   attr F is nonnegative means
:: SUPINF_2:def 22
rng F is nonnegative;
end;

definition
   let F be Function of NAT,ExtREAL;
   func SUM(F) -> R_eal equals
:: SUPINF_2:def 23
 sup(rng Ser(F));
end;

theorem :: SUPINF_2:58
   for X being non empty set
   for F being Function of X,ExtREAL holds
   F is nonnegative iff for n being Element of X holds 0. <=' F.n;

theorem :: SUPINF_2:59
   for F being Function of NAT,ExtREAL holds
   for n being Nat holds
   F is nonnegative implies (Ser(F)).n <=' (Ser(F)).(n + 1) & 0. <=' (Ser(F)).n
;

theorem :: SUPINF_2:60
   for F being Function of NAT,ExtREAL holds
   F is nonnegative implies
   for n,m being Nat holds Ser(F).n <=' Ser(F).(n + m);

theorem :: SUPINF_2:61
   for F1,F2 being Function of NAT,ExtREAL st
   F1 is nonnegative holds
   ((for n being Nat holds F1.n <=' F2.n) implies
   (for n being Nat holds Ser(F1).n <=' Ser(F2).n));

theorem :: SUPINF_2:62
   for F1,F2 being Function of NAT,ExtREAL st
   F1 is nonnegative holds
   ((for n being Nat holds F1.n <=' F2.n) implies (SUM(F1) <=' SUM(F2)));

theorem :: SUPINF_2:63
   for F being Function of NAT,ExtREAL holds
   Ser(F).0 = F.0 &
   for n being Nat holds
   for y being R_eal st y = Ser(F).n holds
   Ser(F).(n + 1) = y + F.(n + 1);

theorem :: SUPINF_2:64
   for F being Function of NAT,ExtREAL st F is nonnegative holds
   (ex n being Nat st F.n = +infty) implies SUM(F) = +infty;

definition
   let F be Function of NAT,ExtREAL;
   attr F is summable means
:: SUPINF_2:def 24
SUM(F) in REAL;
end;

theorem :: SUPINF_2:65
  for F being Function of NAT,ExtREAL st F is nonnegative holds
   ((ex n being Nat st F.n = +infty) implies F is not summable);

theorem :: SUPINF_2:66
     for F1,F2 being Function of NAT,ExtREAL st
   F1 is nonnegative holds
   ((for n being Nat holds F1.n <=' F2.n) implies
   (F2 is summable implies F1 is summable));

theorem :: SUPINF_2:67
   for F being Function of NAT,ExtREAL st F is nonnegative holds
   for n being Nat st (for r being Nat holds (n <= r implies F.r = 0.))
   holds SUM(F) = Ser(F).n;

theorem :: SUPINF_2:68
   for F being Function of NAT,ExtREAL st
   (for n being Nat holds F.n in REAL ) holds
   (for n being Nat holds Ser(F).n in REAL);

theorem :: SUPINF_2:69
     for F being Function of NAT,ExtREAL st F is nonnegative holds
   (ex n being Nat st (for k being Nat holds (n <= k implies F.k = 0.)) &
   (for k being Nat holds (k <= n implies not F.k = +infty)))
   implies F is summable;

Back to top