Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
The abstract of the Mizar article:
-
- 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