:: SUPINF_2 semantic presentation

definition

func 0. -> R_eal equals :: SUPINF_2:def 1
0;
correctness by SUPINF_1:10;

end;

:: deftheorem defines 0. SUPINF_2:def 1 :

definition

let x, y be R_eal;
func x + y -> R_eal means :Def2: :: 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. ;
existence

proof end;

uniqueness ;
consistency by SUPINF_1:6;
commutativity ;

end;

:: deftheorem Def2 defines + SUPINF_2:def 2 :

theorem Th1: :: SUPINF_2:1

for x, y being R_eal
for a, b being Real st x = a & y = b holds
x + y = a + b

proof end;

theorem Th2: :: SUPINF_2:2

for x being R_eal holds
( x in REAL or x = +infty or x = -infty )

proof end;

definition

let x be R_eal;
func - x -> R_eal means :Def3: :: 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 ;
existence

proof end;

uniqueness ;
consistency ;
involutiveness

proof end;

end;

:: deftheorem Def3 defines - SUPINF_2:def 3 :

definition

let x, y be R_eal;
func x - y -> R_eal equals :: SUPINF_2:def 4
x + (- y);
coherence ;

end;

:: deftheorem defines - SUPINF_2:def 4 :

theorem Th3: :: SUPINF_2:3

for x being R_eal
for a being Real st x = a holds
- x = - a

proof end;

theorem Th4: :: SUPINF_2:4

- -infty = +infty by Def3, SUPINF_1:6, SUPINF_1:14;

theorem Th5: :: SUPINF_2:5

for x, y being R_eal
for a, b being Real st x = a & y = b holds
x - y = a - b

proof end;

theorem Th6: :: SUPINF_2:6

for x being R_eal st x <> +infty holds
( +infty - x = +infty & x - +infty = -infty )

proof end;

theorem Th7: :: SUPINF_2:7

for x being R_eal st x <> -infty holds
( -infty - x = -infty & x - -infty = +infty )

proof end;

theorem Th8: :: SUPINF_2:8

for x, s being R_eal holds
( not x + s = +infty or x = +infty or s = +infty )

proof end;

theorem Th9: :: SUPINF_2:9

for x, s being R_eal holds
( not x + s = -infty or x = -infty or s = -infty )

proof end;

theorem Th10: :: SUPINF_2:10

for x, s being R_eal holds
( not x - s = +infty or x = +infty or s = -infty )

proof end;

theorem Th11: :: SUPINF_2:11

for x, s being R_eal holds
( not x - s = -infty or x = -infty or s = +infty )

proof end;

theorem Th12: :: SUPINF_2:12

for x, s being R_eal holds
( ( x = +infty & s = -infty ) or ( x = -infty & s = +infty ) or not x + s in REAL or ( x in REAL & s in REAL ) )

proof end;

theorem Th13: :: SUPINF_2:13

for x, s being R_eal holds
( ( x = +infty & s = +infty ) or ( x = -infty & s = -infty ) or not x - s in REAL or ( x in REAL & s in REAL ) )

proof end;

theorem Th14: :: SUPINF_2:14

for x, y, s, t being R_eal holds
( ( x = +infty & s = -infty ) or ( x = -infty & s = +infty ) or ( y = +infty & t = -infty ) or ( y = -infty & t = +infty ) or not x <=' y or not s <=' t or x + s <=' y + t )

proof end;

theorem :: SUPINF_2:15

for x, y, s, t being R_eal holds
( ( x = +infty & t = +infty ) or ( x = -infty & t = -infty ) or ( y = +infty & s = +infty ) or ( y = -infty & s = -infty ) or not x <=' y or not s <=' t or x - t <=' y - s )

proof end;

Lm1: for x being R_eal holds
( - x in REAL iff x in REAL )

proof end;

Lm2: for x, y being R_eal st x <=' y holds
- y <=' - x

proof end;

theorem Th16: :: SUPINF_2:16

for x, y being R_eal holds
( x <=' y iff - y <=' - x )

proof end;

theorem :: SUPINF_2:17

for x, y being R_eal holds
( x <' y iff - y <' - x ) by Th16;

theorem Th18: :: SUPINF_2:18

for x being R_eal holds
( x + 0. = x & 0. + x = x )

proof end;

theorem :: SUPINF_2:19

( -infty <' 0. & 0. <' +infty )

proof end;

theorem Th20: :: SUPINF_2:20

for x, y, z being R_eal st 0. <=' z & 0. <=' x & y = x + z holds
x <=' y

proof end;

Lm3: for x, y, s, t being R_eal st 0. <=' x & 0. <=' s & x <=' y & s <=' t holds
x + s <=' y + t

proof end;

theorem Th21: :: SUPINF_2:21

for x being R_eal st x in NAT holds
0. <=' x

proof end;

definition

let X, Y be non empty Subset of ExtREAL ;
func X + Y -> Subset of ExtREAL means :Def5: :: 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 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines + SUPINF_2:def 5 :

registration

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

proof end;

end;

definition

let X be non empty Subset of ExtREAL ;
func - X -> Subset of ExtREAL means :Def6: :: 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 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines - SUPINF_2:def 6 :

registration

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

proof end;

end;

theorem Th22: :: SUPINF_2:22

for X being non empty Subset of ExtREAL holds - (- X) = X

proof end;

theorem Th23: :: SUPINF_2:23

for X being non empty Subset of ExtREAL
for z being R_eal holds
( z in X iff - z in - X )

proof end;

theorem :: SUPINF_2:24

for X, Y being non empty Subset of ExtREAL holds
( X c= Y iff - X c= - Y )

proof end;

theorem :: SUPINF_2:25

for z being R_eal holds
( z in REAL iff - z in REAL )

proof end;

theorem Th26: :: SUPINF_2:26

for X, Y being non empty Subset of ExtREAL holds
( ( -infty in X & +infty in Y ) or ( +infty in X & -infty in Y ) or ( sup X = +infty & sup Y = -infty ) or ( sup X = -infty & sup Y = +infty ) or sup (X + Y) <=' (sup X) + (sup Y) )

proof end;

theorem Th27: :: SUPINF_2:27

for X, Y being non empty Subset of ExtREAL holds
( ( -infty in X & +infty in Y ) or ( +infty in X & -infty in Y ) or ( inf X = +infty & inf Y = -infty ) or ( inf X = -infty & inf Y = +infty ) or (inf X) + (inf Y) <=' inf (X + Y) )

proof end;

theorem :: SUPINF_2:28

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)

proof end;

theorem :: SUPINF_2:29

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)

proof end;

theorem Th30: :: SUPINF_2:30

for X being non empty Subset of ExtREAL
for a being R_eal holds
( a is majorant of X iff - a is minorant of - X )

proof end;

theorem Th31: :: SUPINF_2:31

for X being non empty Subset of ExtREAL
for a being R_eal holds
( a is minorant of X iff - a is majorant of - X )

proof end;

theorem Th32: :: SUPINF_2:32

for X being non empty Subset of ExtREAL holds inf (- X) = - (sup X)

proof end;

theorem Th33: :: SUPINF_2:33

for X being non empty Subset of ExtREAL holds sup (- X) = - (inf 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

proof end;

end;

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

end;

:: deftheorem defines sup SUPINF_2:def 7 :

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

end;

:: deftheorem defines inf SUPINF_2:def 8 :

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;
:: original: .
redefine func F . x -> R_eal;
coherence

proof end;

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;
func F + G -> Function of X,Y + Z means :Def9: :: SUPINF_2:def 9
for x being Element of X holds it . x = (F . x) + (G . x);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines + SUPINF_2:def 9 :

theorem Th34: :: SUPINF_2:34

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

theorem Th35: :: SUPINF_2:35

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

proof end;

theorem Th36: :: SUPINF_2:36

for X being non empty set
for Y, Z being non empty Subset of ExtREAL holds
( ( -infty in Y & +infty in Z ) or ( +infty in Y & -infty in Z ) or for F being Function of X,Y
for G being Function of X,Z holds
( ( inf F = +infty & inf G = -infty ) or ( inf F = -infty & inf G = +infty ) or (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;
func - F -> Function of X, - Y means :Def10: :: SUPINF_2:def 10
for x being Element of X holds it . x = - (F . x);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines - SUPINF_2:def 10 :

theorem Th37: :: SUPINF_2:37

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

theorem Th38: :: SUPINF_2:38

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 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_above means :Def11: :: SUPINF_2:def 11
sup F <' +infty ;

end;

:: deftheorem Def11 defines bounded_above SUPINF_2:def 11 :

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 :Def12: :: SUPINF_2:def 12
-infty <' inf F;

end;

:: deftheorem Def12 defines bounded_below SUPINF_2:def 12 :

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 :Def13: :: SUPINF_2:def 13
( F is bounded_above & F is bounded_below );

end;

:: deftheorem Def13 defines bounded SUPINF_2:def 13 :

registration

let X be non empty set ;
let Y be non empty Subset of ExtREAL ;
cluster bounded -> bounded_above bounded_below M8(X,Y);
coherence by Def13;
cluster bounded_above bounded_below -> bounded M8(X,Y);
coherence by Def13;

end;

theorem :: SUPINF_2:39

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

theorem Th40: :: SUPINF_2:40

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

theorem Th41: :: SUPINF_2:41

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

theorem :: SUPINF_2:42

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

theorem :: SUPINF_2:43

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 SUPINF_1:20, SUPINF_1:21;

theorem :: SUPINF_2:44

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

theorem Th45: :: SUPINF_2:45

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

theorem Th46: :: SUPINF_2:46

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

theorem Th47: :: SUPINF_2:47

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

theorem :: SUPINF_2:48

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

theorem Th49: :: SUPINF_2:49

for X being non empty set
for Y, Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
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 Th50: :: SUPINF_2:50

for X being non empty set
for Y, Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
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:51

for X being non empty set
for Y, Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
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 Th52: :: 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 )

proof end;

notation

let D be non empty set ;
let IT be Subset of D;
synonym denumerable IT for countable D;

end;

definition

let D be non empty set ;
let IT be Subset of D;
:: original: denumerable
redefine attr IT is denumerable means :Def14: :: SUPINF_2:def 14
( IT is empty or ex F being Function of NAT ,D st IT = rng F );
compatibility

proof end;

end;

:: deftheorem Def14 defines denumerable SUPINF_2:def 14 :

registration

cluster non empty V34 Element of K40(ExtREAL );
existence

proof end;

end;

definition

mode Denum_Set_of_R_EAL is non empty V34 Subset of ExtREAL ;

end;

definition

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

end;

:: deftheorem Def15 defines nonnegative SUPINF_2:def 15 :

registration

cluster nonnegative Element of K40(ExtREAL );
existence

proof 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 :Def16: :: SUPINF_2:def 16
D = rng it;
existence by Def14;

end;

:: deftheorem Def16 defines Num SUPINF_2:def 16 :

definition

let N be Function of NAT , ExtREAL ;
let n be Nat;
:: original: .
redefine func N . n -> R_eal;
coherence

proof end;

end;

theorem Th53: :: SUPINF_2:53

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

proof end;

definition

let D be Denum_Set_of_R_EAL;
let N be Num of D;
func Ser D,N -> Function of NAT , ExtREAL means :Def17: :: SUPINF_2:def 17
( 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 by Th53;
uniqueness

proof end;

end;

:: deftheorem Def17 defines Ser SUPINF_2:def 17 :

theorem Th54: :: SUPINF_2:54

for D being Pos_Denum_Set_of_R_EAL
for N being Num of D
for n being Nat holds 0. <=' N . n

proof end;

theorem Th55: :: SUPINF_2:55

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

proof end;

theorem Th56: :: SUPINF_2:56

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

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

proof end;

end;

:: deftheorem defines Set_of_Series SUPINF_2:def 18 :

Lm4: for F being Function of NAT , ExtREAL holds rng F is non empty Subset of ExtREAL

proof end;

definition

let F be Function of NAT , ExtREAL ;
:: original: rng
redefine func rng F -> non empty Subset of ExtREAL ;
coherence by Lm4;

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

end;

:: deftheorem defines SUM SUPINF_2:def 19 :

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;

:: deftheorem defines is_sumable SUPINF_2:def 20 :

theorem Th57: :: SUPINF_2:57

for F being Function of NAT , ExtREAL holds rng F is Denum_Set_of_R_EAL by Def14;

definition

let F be Function of NAT , ExtREAL ;
:: original: rng
redefine func rng F -> Denum_Set_of_R_EAL;
coherence by Th57;

end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines Ser SUPINF_2:def 21 :

definition

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

end;

:: deftheorem Def22 defines nonnegative SUPINF_2:def 22 :

definition

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

end;

:: deftheorem defines SUM SUPINF_2:def 23 :

theorem Th58: :: 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 )

proof end;

theorem Th59: :: SUPINF_2:59

for F being Function of NAT , ExtREAL
for n being Nat st F is nonnegative holds
( (Ser F) . n <=' (Ser F) . (n + 1) & 0. <=' (Ser F) . n )

proof end;

theorem Th60: :: SUPINF_2:60

for F being Function of NAT , ExtREAL st F is nonnegative holds
for n, m being Nat holds (Ser F) . n <=' (Ser F) . (n + m)

proof end;

theorem Th61: :: SUPINF_2:61

for F1, F2 being Function of NAT , ExtREAL st F1 is nonnegative & ( for n being Nat holds F1 . n <=' F2 . n ) holds
for n being Nat holds (Ser F1) . n <=' (Ser F2) . n

proof end;

theorem Th62: :: SUPINF_2:62

for F1, F2 being Function of NAT , ExtREAL st F1 is nonnegative & ( for n being Nat holds F1 . n <=' F2 . n ) holds
SUM F1 <=' SUM F2

proof end;

theorem Th63: :: SUPINF_2:63

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

proof end;

theorem Th64: :: SUPINF_2:64

for F being Function of NAT , ExtREAL st F is nonnegative & ex n being Nat st F . n = +infty holds
SUM F = +infty

proof end;

definition

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

end;

:: deftheorem Def24 defines summable SUPINF_2:def 24 :

theorem :: SUPINF_2:65

for F being Function of NAT , ExtREAL st F is nonnegative & ex n being Nat st F . n = +infty holds
not F is summable

proof end;

theorem :: SUPINF_2:66

for F1, F2 being Function of NAT , ExtREAL st F1 is nonnegative & ( for n being Nat holds F1 . n <=' F2 . n ) & F2 is summable holds
F1 is summable

proof end;

theorem Th67: :: SUPINF_2:67

for F being Function of NAT , ExtREAL st F is nonnegative holds
for n being Nat st ( for r being Nat st n <= r holds
F . r = 0. ) holds
SUM F = (Ser F) . n

proof end;

theorem Th68: :: 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

proof end;

theorem :: SUPINF_2:69

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

proof end;