:: On the Real Valued Functions
:: by Artur Korni{\l}owicz
::
:: Received December 10, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

registration
let r be real number ;
clusterr / r ->  non negative ;
coherence
 not r / r is negative
proofend;
end;

registration
let r be real number ;
clusterr * r ->  non negative ;
coherence
 not r * r is negative by XREAL_1:63;
clusterr * (r ") ->  non negative ;
coherence
 not r * (r ") is negative
proofend;
end;

registration
let r be real non negative number ;
cluster sqrt r ->  non negative ;
coherence
 not sqrt r is negative by SQUARE_1:def_2;
end;

registration
let r be real positive number ;
cluster sqrt r ->  positive ;
coherence
 sqrt r is positive by SQUARE_1:25;
end;

theorem :: PARTFUN3:1
for f being Function
for A being set st f is one-to-one & A c= dom (f ") holds
f .: ((f ") .: A) = A
proofend;

registration
let f be non-empty Function;
clusterf " {0} ->  empty ;
coherence
 f " {0} is empty
proofend;
end;

definition
let R be Relation;
attrR is positive-yielding  means :Def1: :: PARTFUN3:def 1
 for r being real number st r in rng R holds
0 < r;
attrR is negative-yielding  means :Def2: :: PARTFUN3:def 2
 for r being real number st r in rng R holds
0 > r;
attrR is nonpositive-yielding  means :Def3: :: PARTFUN3:def 3
 for r being real number st r in rng R holds
0 >= r;
attrR is nonnegative-yielding  means :Def4: :: PARTFUN3:def 4
 for r being real number st r in rng R holds
0 <= r;
end;

:: deftheorem Def1 defines positive-yielding PARTFUN3:def_1_:_
 for R being Relation holds
( R is positive-yielding iff for r being real number st r in rng R holds
0 < r );

:: deftheorem Def2 defines negative-yielding PARTFUN3:def_2_:_
 for R being Relation holds
( R is negative-yielding iff for r being real number st r in rng R holds
0 > r );

:: deftheorem Def3 defines nonpositive-yielding PARTFUN3:def_3_:_
 for R being Relation holds
( R is nonpositive-yielding iff for r being real number st r in rng R holds
0 >= r );

:: deftheorem Def4 defines nonnegative-yielding PARTFUN3:def_4_:_
 for R being Relation holds
( R is nonnegative-yielding iff for r being real number st r in rng R holds
0 <= r );

registration
let X be set ;
let r be real positive number ;
clusterX --> r ->  positive-yielding ;
coherence
 X --> r is positive-yielding
proofend;
end;

registration
let X be set ;
let r be real negative number ;
clusterX --> r ->  negative-yielding ;
coherence
 X --> r is negative-yielding
proofend;
end;

registration
let X be set ;
let r be real non positive number ;
clusterX --> r ->  nonpositive-yielding ;
coherence
 X --> r is nonpositive-yielding
proofend;
end;

registration
let X be set ;
let r be real non negative number ;
clusterX --> r ->  nonnegative-yielding ;
coherence
 X --> r is nonnegative-yielding
proofend;
end;

registration
let X be non empty set ;
clusterX --> 0 ->  non non-empty ;
coherence
 not X --> 0 is non-empty
proofend;
end;

registration
cluster Relation-like positive-yielding  ->  non-empty nonnegative-yielding for set ;
coherence
 for b1 being Relation st b1 is positive-yielding holds
( b1 is nonnegative-yielding &amp; b1 is non-empty )
proofend;
cluster Relation-like negative-yielding  ->  non-empty nonpositive-yielding for set ;
coherence
 for b1 being Relation st b1 is negative-yielding holds
( b1 is nonpositive-yielding &amp; b1 is non-empty )
proofend;
end;

registration
let X be set ;
cluster Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued negative-yielding for Element of K6(K7(X,REAL));
existence
 ex b1 being Function of X,REAL st b1 is negative-yielding
proofend;
cluster Relation-like X -defined REAL -valued Function-like total V33(X, REAL ) complex-valued ext-real-valued real-valued positive-yielding for Element of K6(K7(X,REAL));
existence
 ex b1 being Function of X,REAL st b1 is positive-yielding
proofend;
end;

registration
cluster Relation-like non-empty Function-like real-valued for set ;
existence
 ex b1 being Function st
( b1 is non-empty &amp; b1 is real-valued )
proofend;
end;

theorem Th2: :: PARTFUN3:2
for f being non-empty real-valued Function holds dom (f ^) = dom f
proofend;

theorem Th3: :: PARTFUN3:3
for X being non empty set
for f being PartFunc of X,REAL
for g being non-empty PartFunc of X,REAL holds dom (f / g) = (dom f) /\ (dom g)
proofend;

registration
let X be set ;
let f, g be nonpositive-yielding PartFunc of X,REAL;
clusterf + g ->  nonpositive-yielding ;
coherence
 f + g is nonpositive-yielding
proofend;
end;

registration
let X be set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;
clusterf + g ->  nonnegative-yielding ;
coherence
 f + g is nonnegative-yielding
proofend;
end;

registration
let X be set ;
let f be positive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
clusterf + g ->  positive-yielding ;
coherence
 f + g is positive-yielding
proofend;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be positive-yielding PartFunc of X,REAL;
clusterf + g ->  positive-yielding ;
coherence
 f + g is positive-yielding ;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
clusterf + g ->  negative-yielding ;
coherence
 f + g is negative-yielding
proofend;
end;

registration
let X be set ;
let f be negative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
clusterf + g ->  negative-yielding ;
coherence
 f + g is negative-yielding ;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
clusterf - g ->  nonnegative-yielding ;
coherence
 f - g is nonnegative-yielding
proofend;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
clusterf - g ->  nonpositive-yielding ;
coherence
 f - g is nonpositive-yielding
proofend;
end;

registration
let X be set ;
let f be positive-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
clusterf - g ->  positive-yielding ;
coherence
 f - g is positive-yielding
proofend;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be positive-yielding PartFunc of X,REAL;
clusterf - g ->  negative-yielding ;
coherence
 f - g is negative-yielding
proofend;
end;

registration
let X be set ;
let f be negative-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
clusterf - g ->  negative-yielding ;
coherence
 f - g is negative-yielding
proofend;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
clusterf - g ->  positive-yielding ;
coherence
 f - g is positive-yielding
proofend;
end;

registration
let X be set ;
let f, g be nonpositive-yielding PartFunc of X,REAL;
clusterf (#) g ->  nonnegative-yielding ;
coherence
 f (#) g is nonnegative-yielding
proofend;
end;

registration
let X be set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;
clusterf (#) g ->  nonnegative-yielding ;
coherence
 f (#) g is nonnegative-yielding
proofend;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
clusterf (#) g ->  nonpositive-yielding ;
coherence
 f (#) g is nonpositive-yielding
proofend;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
clusterf (#) g ->  nonpositive-yielding ;
coherence
 f (#) g is nonpositive-yielding ;
end;

registration
let X be set ;
let f be positive-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
clusterf (#) g ->  negative-yielding ;
coherence
 f (#) g is negative-yielding
proofend;
end;

registration
let X be set ;
let f be negative-yielding PartFunc of X,REAL;
let g be positive-yielding PartFunc of X,REAL;
clusterf (#) g ->  negative-yielding ;
coherence
 f (#) g is negative-yielding ;
end;

registration
let X be set ;
let f, g be positive-yielding PartFunc of X,REAL;
clusterf (#) g ->  positive-yielding ;
coherence
 f (#) g is positive-yielding
proofend;
end;

registration
let X be set ;
let f, g be negative-yielding PartFunc of X,REAL;
clusterf (#) g ->  positive-yielding ;
coherence
 f (#) g is positive-yielding
proofend;
end;

registration
let X be set ;
let f, g be non-empty PartFunc of X,REAL;
clusterf (#) g ->  non-empty ;
coherence
 f (#) g is non-empty
proofend;
end;

registration
let X be set ;
let f be PartFunc of X,REAL;
clusterf (#) f ->  nonnegative-yielding ;
coherence
 f (#) f is nonnegative-yielding
proofend;
end;

registration
let X be set ;
let r be real non positive number ;
let f be nonpositive-yielding PartFunc of X,REAL;
clusterr (#) f ->  nonnegative-yielding ;
coherence
 r (#) f is nonnegative-yielding
proofend;
end;

registration
let X be set ;
let r be real non negative number ;
let f be nonnegative-yielding PartFunc of X,REAL;
clusterr (#) f ->  nonnegative-yielding ;
coherence
 r (#) f is nonnegative-yielding
proofend;
end;

registration
let X be set ;
let r be real non positive number ;
let f be nonnegative-yielding PartFunc of X,REAL;
clusterr (#) f ->  nonpositive-yielding ;
coherence
 r (#) f is nonpositive-yielding
proofend;
end;

registration
let X be set ;
let r be real non negative number ;
let f be nonpositive-yielding PartFunc of X,REAL;
clusterr (#) f ->  nonpositive-yielding ;
coherence
 r (#) f is nonpositive-yielding
proofend;
end;

registration
let X be set ;
let r be real positive number ;
let f be negative-yielding PartFunc of X,REAL;
clusterr (#) f ->  negative-yielding ;
coherence
 r (#) f is negative-yielding
proofend;
end;

registration
let X be set ;
let r be real negative number ;
let f be positive-yielding PartFunc of X,REAL;
clusterr (#) f ->  negative-yielding ;
coherence
 r (#) f is negative-yielding
proofend;
end;

registration
let X be set ;
let r be real positive number ;
let f be positive-yielding PartFunc of X,REAL;
clusterr (#) f ->  positive-yielding ;
coherence
 r (#) f is positive-yielding
proofend;
end;

registration
let X be set ;
let r be real negative number ;
let f be negative-yielding PartFunc of X,REAL;
clusterr (#) f ->  positive-yielding ;
coherence
 r (#) f is positive-yielding
proofend;
end;

registration
let X be set ;
let r be non zero real number ;
let f be non-empty PartFunc of X,REAL;
clusterr (#) f ->  non-empty ;
coherence
 r (#) f is non-empty
proofend;
end;

registration
let X be non empty set ;
let f, g be nonpositive-yielding PartFunc of X,REAL;
clusterf / g ->  nonnegative-yielding ;
coherence
 f / g is nonnegative-yielding
proofend;
end;

registration
let X be non empty set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;
clusterf / g ->  nonnegative-yielding ;
coherence
 f / g is nonnegative-yielding
proofend;
end;

registration
let X be non empty set ;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
clusterf / g ->  nonpositive-yielding ;
coherence
 f / g is nonpositive-yielding
proofend;
end;

registration
let X be non empty set ;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
clusterf / g ->  nonpositive-yielding ;
coherence
 f / g is nonpositive-yielding
proofend;
end;

registration
let X be non empty set ;
let f be positive-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
clusterf / g ->  negative-yielding ;
coherence
 f / g is negative-yielding
proofend;
end;

registration
let X be non empty set ;
let f be negative-yielding PartFunc of X,REAL;
let g be positive-yielding PartFunc of X,REAL;
clusterf / g ->  negative-yielding ;
coherence
 f / g is negative-yielding
proofend;
end;

registration
let X be non empty set ;
let f, g be positive-yielding PartFunc of X,REAL;
clusterf / g ->  positive-yielding ;
coherence
 f / g is positive-yielding
proofend;
end;

registration
let X be non empty set ;
let f, g be negative-yielding PartFunc of X,REAL;
clusterf / g ->  positive-yielding ;
coherence
 f / g is positive-yielding
proofend;
end;

registration
let X be non empty set ;
let f be PartFunc of X,REAL;
clusterf / f ->  nonnegative-yielding ;
coherence
 f / f is nonnegative-yielding
proofend;
end;

registration
let X be non empty set ;
let f, g be non-empty PartFunc of X,REAL;
clusterf / g ->  non-empty ;
coherence
 f / g is non-empty
proofend;
end;

registration
let X be set ;
let f be nonpositive-yielding Function of X,REAL;
cluster Inv f ->  nonpositive-yielding ;
coherence
 Inv f is nonpositive-yielding
proofend;
end;

registration
let X be set ;
let f be nonnegative-yielding Function of X,REAL;
cluster Inv f ->  nonnegative-yielding ;
coherence
 Inv f is nonnegative-yielding
proofend;
end;

registration
let X be set ;
let f be positive-yielding Function of X,REAL;
cluster Inv f ->  positive-yielding ;
coherence
 Inv f is positive-yielding
proofend;
end;

registration
let X be set ;
let f be negative-yielding Function of X,REAL;
cluster Inv f ->  negative-yielding ;
coherence
 Inv f is negative-yielding
proofend;
end;

registration
let X be set ;
let f be non-empty Function of X,REAL;
cluster Inv f ->  non-empty ;
coherence
 Inv f is non-empty
proofend;
end;

registration
let X be set ;
let f be non-empty Function of X,REAL;
cluster - f ->  non-empty ;
coherence
 - f is non-empty ;
end;

registration
let X be set ;
let f be nonpositive-yielding Function of X,REAL;
cluster - f ->  nonnegative-yielding ;
coherence
 - f is nonnegative-yielding ;
end;

registration
let X be set ;
let f be nonnegative-yielding Function of X,REAL;
cluster - f ->  nonpositive-yielding ;
coherence
 - f is nonpositive-yielding ;
end;

registration
let X be set ;
let f be positive-yielding Function of X,REAL;
cluster - f ->  negative-yielding ;
coherence
 - f is negative-yielding ;
end;

registration
let X be set ;
let f be negative-yielding Function of X,REAL;
cluster - f ->  positive-yielding ;
coherence
 - f is positive-yielding ;
end;

registration
let X be set ;
let f be Function of X,REAL;
cluster|.f.| ->  nonnegative-yielding ;
coherence
 abs f is nonnegative-yielding
proofend;
end;

registration
let X be set ;
let f be non-empty Function of X,REAL;
cluster|.f.| ->  positive-yielding ;
coherence
 abs f is positive-yielding
proofend;
end;

registration
let X be non empty set ;
let f be nonpositive-yielding Function of X,REAL;
clusterf ^  ->  nonpositive-yielding ;
coherence
 f ^ is nonpositive-yielding
proofend;
end;

registration
let X be non empty set ;
let f be nonnegative-yielding Function of X,REAL;
clusterf ^  ->  nonnegative-yielding ;
coherence
 f ^ is nonnegative-yielding
proofend;
end;

registration
let X be non empty set ;
let f be positive-yielding Function of X,REAL;
clusterf ^  ->  positive-yielding ;
coherence
 f ^ is positive-yielding
proofend;
end;

registration
let X be non empty set ;
let f be negative-yielding Function of X,REAL;
clusterf ^  ->  negative-yielding ;
coherence
 f ^ is negative-yielding
proofend;
end;

registration
let X be non empty set ;
let f be non-empty Function of X,REAL;
clusterf ^  ->  non-empty ;
coherence
 f ^ is non-empty
proofend;
end;

definition
let f be real-valued Function;
func sqrt f ->  Function means :Def5: :: PARTFUN3:def 5
( dom it = dom f &amp; ( for x being set st x in dom it holds
it . x = sqrt (f . x) ) );
existence
 ex b1 being Function st
( dom b1 = dom f &amp; ( for x being set st x in dom b1 holds
b1 . x = sqrt (f . x) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for x being set st x in dom b1 holds
b1 . x = sqrt (f . x) ) &amp; dom b2 = dom f &amp; ( for x being set st x in dom b2 holds
b2 . x = sqrt (f . x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines sqrt PARTFUN3:def_5_:_
 for f being real-valued Function
for b2 being Function holds
( b2 = sqrt f iff ( dom b2 = dom f &amp; ( for x being set st x in dom b2 holds
b2 . x = sqrt (f . x) ) ) );

registration
let f be real-valued Function;
cluster sqrt f ->  real-valued ;
coherence
 sqrt f is real-valued
proofend;
end;

definition
let C be set ;
let D be real-membered set ;
let f be PartFunc of C,D;
:: original:sqrt
redefine func sqrt f ->  PartFunc of C,REAL;
coherence
 sqrt f is PartFunc of C,REAL
proofend;
end;

registration
let X be set ;
let f be nonnegative-yielding Function of X,REAL;
cluster sqrt f ->  nonnegative-yielding ;
coherence
 sqrt f is nonnegative-yielding
proofend;
end;

registration
let X be set ;
let f be positive-yielding Function of X,REAL;
cluster sqrt f ->  positive-yielding ;
coherence
 sqrt f is positive-yielding
proofend;
end;

definition
let X be set ;
let f be Function of X,REAL;
:: original:sqrt
redefine func sqrt f ->  Function of X,REAL;
coherence
 sqrt f is Function of X,REAL
proofend;
end;

definition
let X be set ;
let f be non-empty Function of X,REAL;
:: original:^
redefine funcf ^  ->  Function of X,REAL;
coherence
 f ^ is Function of X,REAL
proofend;
end;

definition
let X be non empty set ;
let f be Function of X,REAL;
let g be non-empty Function of X,REAL;
:: original:/
redefine funcf / g ->  Function of X,REAL;
coherence
 f / g is Function of X,REAL
proofend;
end;