:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama

::

:: Received September 15, 2000

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

begin

begin

theorem :: EXTREAL2:17

for x, y being R_eal 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;

begin

theorem :: EXTREAL2:26

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

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

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

proof end;

theorem :: EXTREAL2:27

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

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

max (x,y) = ((x + y) + |.(x - y).|) / (R_EAL 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;

begin

:: missing, 2007.07.20, A.T.