:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama

::

:: Received September 7, 2000

:: Copyright (c) 2000-2018 Association of Mizar Users

definition

let x, y be R_eal;

:: original: *

redefine func x * y -> R_eal;

coherence

x * y is R_eal by XXREAL_0:def 1;

end;
:: original: *

redefine func x * y -> R_eal;

coherence

x * y is R_eal by XXREAL_0:def 1;

theorem :: EXTREAL1:1

definition

let x, y be ExtReal;

:: original: /

redefine func x / y -> R_eal;

coherence

x / y is R_eal by XXREAL_0:def 1;

end;
:: original: /

redefine func x / y -> R_eal;

coherence

x / y is R_eal by XXREAL_0:def 1;

theorem :: EXTREAL1:2

definition

let x be ExtReal;

coherence

( ( 0 <= x implies x is R_eal ) & ( not 0 <= x implies - x is R_eal ) ) by XXREAL_0:def 1;

consistency

for b_{1} being R_eal holds verum
;

projectivity

for b_{1} being R_eal

for b_{2} being ExtReal st ( 0 <= b_{2} implies b_{1} = b_{2} ) & ( not 0 <= b_{2} implies b_{1} = - b_{2} ) holds

( ( 0 <= b_{1} implies b_{1} = b_{1} ) & ( not 0 <= b_{1} implies b_{1} = - b_{1} ) )
;

end;
coherence

( ( 0 <= x implies x is R_eal ) & ( not 0 <= x implies - x is R_eal ) ) by XXREAL_0:def 1;

consistency

for b

projectivity

for b

for b

( ( 0 <= b

:: deftheorem Def1 defines |. EXTREAL1:def 1 :

for x being ExtReal holds

( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) );

for x being ExtReal holds

( ( 0 <= x implies |.x.| = x ) & ( not 0 <= x implies |.x.| = - x ) );

registration
end;

registration
end;

:: from CONVFUN1, 2010.02.13, A.T.

definition

let F be FinSequence of ExtREAL ;

ex b_{1} being R_eal ex f being sequence of ExtREAL st

( b_{1} = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ) )

for b_{1}, b_{2} being R_eal st ex f being sequence of ExtREAL st

( b_{1} = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ) ) & ex f being sequence of ExtREAL st

( b_{2} = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ) ) holds

b_{1} = b_{2}

end;
func Sum F -> R_eal means :Def2: :: EXTREAL1:def 2

ex f being sequence of ExtREAL st

( it = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ) );

existence ex f being sequence of ExtREAL st

( it = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ) );

ex b

( b

f . (i + 1) = (f . i) + (F . (i + 1)) ) )

proof end;

uniqueness for b

( b

f . (i + 1) = (f . i) + (F . (i + 1)) ) ) & ex f being sequence of ExtREAL st

( b

f . (i + 1) = (f . i) + (F . (i + 1)) ) ) holds

b

proof end;

:: deftheorem Def2 defines Sum EXTREAL1:def 2 :

for F being FinSequence of ExtREAL

for b_{2} being R_eal holds

( b_{2} = Sum F iff ex f being sequence of ExtREAL st

( b_{2} = f . (len F) & f . 0 = 0. & ( for i being Nat st i < len F holds

f . (i + 1) = (f . i) + (F . (i + 1)) ) ) );

for F being FinSequence of ExtREAL

for b

( b

( b

f . (i + 1) = (f . i) + (F . (i + 1)) ) ) );

Lm1: for F being FinSequence of ExtREAL

for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x

proof end;

Lm2: for F being FinSequence of ExtREAL st not -infty in rng F holds

Sum F <> -infty

proof end;

theorem Th8: :: EXTREAL1:10

for F, G being FinSequence of ExtREAL st not -infty in rng F & not -infty in rng G holds

Sum (F ^ G) = (Sum F) + (Sum G)

Sum (F ^ G) = (Sum F) + (Sum G)

proof end;

Lm3: for n, q being Nat st q in Seg (n + 1) holds

ex p being Permutation of (Seg (n + 1)) st

for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) )

proof end;

Lm4: for n, q being Nat

for s, p being Permutation of (Seg (n + 1))

for s9 being FinSequence of Seg (n + 1) st s9 = s & q = s . (n + 1) & ( for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds

p * (s9 | n) is Permutation of (Seg n)

proof end;

Lm5: for n, q being Nat

for p being Permutation of (Seg (n + 1))

for F, H being FinSequence of ExtREAL st F = H * p & q in Seg (n + 1) & len H = n + 1 & not -infty in rng H & ( for i being Element of NAT st i in Seg (n + 1) holds

( ( i < q implies p . i = i ) & ( i = q implies p . i = n + 1 ) & ( i > q implies p . i = i - 1 ) ) ) holds

Sum F = Sum H

proof end;

theorem :: EXTREAL1:11

for F, G being FinSequence of ExtREAL

for s being Permutation of (dom F) st G = F * s & not -infty in rng F holds

Sum F = Sum G

for s being Permutation of (dom F) st G = F * s & not -infty in rng F holds

Sum F = Sum G

proof end;

theorem :: EXTREAL1:28

for x, y being ExtReal st ( ( not x = -infty & not x = +infty ) or ( not y = -infty & not y = +infty ) ) & y <> 0 holds

|.(x / y).| = |.x.| / |.y.|

|.(x / y).| = |.x.| / |.y.|

proof end;

::$CT

theorem :: EXTREAL1:37

for x, y being ExtReal st x <> +infty & y <> +infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) holds

min (x,y) = ((x + y) - |.(x - y).|) / 2

min (x,y) = ((x + y) - |.(x - y).|) / 2

proof end;

theorem :: EXTREAL1:38

for x, y being ExtReal st x <> -infty & y <> -infty & not ( x = +infty & y = +infty ) & not ( x = -infty & y = -infty ) holds

max (x,y) = ((x + y) + |.(x - y).|) / 2

max (x,y) = ((x + y) + |.(x - y).|) / 2

proof end;

definition

let x, y be R_eal;

:: original: max

redefine func max (x,y) -> R_eal;

coherence

max (x,y) is R_eal by XXREAL_0:def 1;

:: original: min

redefine func min (x,y) -> R_eal;

coherence

min (x,y) is R_eal by XXREAL_0:def 1;

end;
:: original: max

redefine func max (x,y) -> R_eal;

coherence

max (x,y) is R_eal by XXREAL_0:def 1;

:: original: min

redefine func min (x,y) -> R_eal;

coherence

min (x,y) is R_eal by XXREAL_0:def 1;

:: missing, 2007.07.20, A.T.

theorem :: EXTREAL1:41