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

registration
let r be Real;
cluster r / r -> non negative ;
coherence
not r / r is negative
proof end;
end;

registration
let r be Real;
cluster r * r -> non negative ;
coherence
not r * r is negative
by XREAL_1:63;
cluster r * (r ") -> non negative ;
coherence
not r * (r ") is negative
proof end;
end;

registration
let r be non negative Real;
cluster sqrt r -> non negative ;
coherence
not sqrt r is negative
by SQUARE_1:def 2;
end;

registration
let r be positive Real;
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
proof end;

registration
let f be non-empty Function;
cluster f " -> empty ;
coherence
f " is empty
proof end;
end;

definition
let R be Relation;
attr R is positive-yielding means :Def1: :: PARTFUN3:def 1
for r being Real st r in rng R holds
0 < r;
attr R is negative-yielding means :Def2: :: PARTFUN3:def 2
for r being Real st r in rng R holds
0 > r;
attr R is nonpositive-yielding means :Def3: :: PARTFUN3:def 3
for r being Real st r in rng R holds
0 >= r;
attr R is nonnegative-yielding means :Def4: :: PARTFUN3:def 4
for r being Real 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 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 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 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 st r in rng R holds
0 <= r );

registration
let X be set ;
let r be positive Real;
cluster K296(X,r) -> positive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be negative Real;
cluster K296(X,r) -> negative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be non positive Real;
cluster K296(X,r) -> nonpositive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be non negative Real;
cluster K296(X,r) -> nonnegative-yielding ;
coherence
proof end;
end;

registration
let X be non empty set ;
cluster K296(X,0) -> non non-empty ;
coherence
not X --> 0 is non-empty
proof end;
end;

registration
coherence
for b1 being Relation st b1 is positive-yielding holds
( b1 is nonnegative-yielding & b1 is non-empty )
;
coherence
for b1 being Relation st b1 is negative-yielding holds
( b1 is nonpositive-yielding & b1 is non-empty )
;
end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

registration
let X be set ;
existence
ex b1 being Function of X,REAL st b1 is negative-yielding
proof end;
existence
ex b1 being Function of X,REAL st b1 is positive-yielding
proof end;
end;

registration
existence
ex b1 being Function st
( b1 is non-empty & b1 is real-valued )
proof end;
end;

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

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

registration
let X be set ;
let f, g be nonpositive-yielding PartFunc of X,REAL;
cluster K225(f,g) -> nonpositive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;
cluster K225(f,g) -> nonnegative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f be positive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
cluster K225(f,g) -> positive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be positive-yielding PartFunc of X,REAL;
cluster K225(f,g) -> positive-yielding ;
coherence ;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
cluster K225(f,g) -> negative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f be negative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
cluster K225(f,g) -> negative-yielding ;
coherence ;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
cluster K269(f,g) -> nonnegative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
cluster K269(f,g) -> nonpositive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f be positive-yielding PartFunc of X,REAL;
let g be nonpositive-yielding PartFunc of X,REAL;
cluster K269(f,g) -> positive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be positive-yielding PartFunc of X,REAL;
cluster K269(f,g) -> negative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f be negative-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
cluster K269(f,g) -> negative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f be nonnegative-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
cluster K269(f,g) -> positive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f, g be nonpositive-yielding PartFunc of X,REAL;
cluster K242(f,g) -> nonnegative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;
cluster K242(f,g) -> nonnegative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f be nonpositive-yielding PartFunc of X,REAL;
let g be nonnegative-yielding PartFunc of X,REAL;
cluster K242(f,g) -> nonpositive-yielding ;
coherence
proof end;
end;

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

registration
let X be set ;
let f be positive-yielding PartFunc of X,REAL;
let g be negative-yielding PartFunc of X,REAL;
cluster K242(f,g) -> negative-yielding ;
coherence
proof end;
end;

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

registration
let X be set ;
let f, g be positive-yielding PartFunc of X,REAL;
cluster K242(f,g) -> positive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let f, g be negative-yielding PartFunc of X,REAL;
cluster K242(f,g) -> positive-yielding ;
coherence
proof end;
end;

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

registration
let X be set ;
let f be PartFunc of X,REAL;
cluster K242(f,f) -> nonnegative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be non positive Real;
let f be nonpositive-yielding PartFunc of X,REAL;
cluster K248(f,r) -> nonnegative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be non negative Real;
let f be nonnegative-yielding PartFunc of X,REAL;
cluster K248(f,r) -> nonnegative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be non positive Real;
let f be nonnegative-yielding PartFunc of X,REAL;
cluster K248(f,r) -> nonpositive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be non negative Real;
let f be nonpositive-yielding PartFunc of X,REAL;
cluster K248(f,r) -> nonpositive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be positive Real;
let f be negative-yielding PartFunc of X,REAL;
cluster K248(f,r) -> negative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be negative Real;
let f be positive-yielding PartFunc of X,REAL;
cluster K248(f,r) -> negative-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be positive Real;
let f be positive-yielding PartFunc of X,REAL;
cluster K248(f,r) -> positive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be negative Real;
let f be negative-yielding PartFunc of X,REAL;
cluster K248(f,r) -> positive-yielding ;
coherence
proof end;
end;

registration
let X be set ;
let r be non zero Real;
let f be non-empty PartFunc of X,REAL;
cluster K248(f,r) -> non-empty ;
coherence
r (#) f is non-empty
proof end;
end;

registration
let X be non empty set ;
let f, g be nonpositive-yielding PartFunc of X,REAL;
cluster K168(f,g) -> nonnegative-yielding ;
coherence
proof end;
end;

registration
let X be non empty set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;
cluster K168(f,g) -> nonnegative-yielding ;
coherence
proof end;
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;
cluster K168(f,g) -> nonpositive-yielding ;
coherence
proof end;
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;
cluster K168(f,g) -> nonpositive-yielding ;
coherence
proof end;
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;
cluster K168(f,g) -> negative-yielding ;
coherence
proof end;
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;
cluster K168(f,g) -> negative-yielding ;
coherence
proof end;
end;

registration
let X be non empty set ;
let f, g be positive-yielding PartFunc of X,REAL;
cluster K168(f,g) -> positive-yielding ;
coherence
proof end;
end;

registration
let X be non empty set ;
let f, g be negative-yielding PartFunc of X,REAL;
cluster K168(f,g) -> positive-yielding ;
coherence
proof end;
end;

registration
let X be non empty set ;
let f be PartFunc of X,REAL;
cluster K168(f,f) -> nonnegative-yielding ;
coherence
proof end;
end;

registration
let X be non empty set ;
let f, g be non-empty PartFunc of X,REAL;
cluster K168(f,g) -> non-empty ;
coherence
f / g is non-empty
proof end;
end;

registration
let X be set ;
let f be nonpositive-yielding Function of X,REAL;
coherence
proof end;
end;

registration
let X be set ;
let f be nonnegative-yielding Function of X,REAL;
coherence
proof end;
end;

registration
let X be set ;
let f be positive-yielding Function of X,REAL;
coherence
proof end;
end;

registration
let X be set ;
let f be negative-yielding Function of X,REAL;
coherence
proof end;
end;

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

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

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

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

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

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

registration
let X be set ;
let f be Function of X,REAL;
coherence
proof end;
end;

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

registration
let X be non empty set ;
let f be nonpositive-yielding Function of X,REAL;
coherence
proof end;
end;

registration
let X be non empty set ;
let f be nonnegative-yielding Function of X,REAL;
coherence
proof end;
end;

registration
let X be non empty set ;
let f be positive-yielding Function of X,REAL;
coherence
proof end;
end;

registration
let X be non empty set ;
let f be negative-yielding Function of X,REAL;
coherence
proof end;
end;

registration
let X be non empty set ;
let f be non-empty Function of X,REAL;
cluster K171(f) -> non-empty ;
coherence
f ^ is non-empty
proof end;
end;

definition
let f be real-valued Function;
func sqrt f -> Function means :Def5: :: PARTFUN3:def 5
( dom it = dom f & ( for x being object st x in dom it holds
it . x = sqrt (f . x) ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being object st x in dom b1 holds
b1 . x = sqrt (f . x) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being object st x in dom b1 holds
b1 . x = sqrt (f . x) ) & dom b2 = dom f & ( for x being object st x in dom b2 holds
b2 . x = sqrt (f . x) ) holds
b1 = b2
proof end;
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 & ( for x being object st x in dom b2 holds
b2 . x = sqrt (f . x) ) ) );

registration
let f be real-valued Function;
coherence
proof end;
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
proof end;
end;

registration
let X be set ;
let f be nonnegative-yielding Function of X,REAL;
coherence
proof end;
end;

registration
let X be set ;
let f be positive-yielding Function of X,REAL;
cluster (f) -> positive-yielding ;
coherence
proof end;
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
proof end;
end;

definition
let X be set ;
let f be non-empty Function of X,REAL;
:: original: ^
redefine func f ^ -> Function of X,REAL;
coherence
f ^ is Function of X,REAL
proof end;
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 func f / g -> Function of X,REAL;
coherence
f / g is Function of X,REAL
proof end;
end;