:: On the Real Valued Functions
:: by Artur Korni{\l}owicz
::
:: Received December 10, 2004
:: Copyright (c) 2004-2021 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;

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

proof end;

registration

let f be non-empty Function;

cluster f " {0} -> empty ;

coherence
f " {0} 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 X --> r -> positive-yielding ;

coherence
X --> r is positive-yielding

proof end;

end;

registration

let X be set ;
let r be negative Real;

cluster X --> r -> negative-yielding ;

coherence
X --> r is negative-yielding

proof end;

end;

registration

let X be set ;
let r be non positive Real;

cluster X --> r -> nonpositive-yielding ;

coherence
X --> r is nonpositive-yielding

proof end;

end;

registration

let X be set ;
let r be non negative Real;

cluster X --> r -> nonnegative-yielding ;

coherence
X --> r is nonnegative-yielding

proof end;

end;

registration

let X be non empty set ;

cluster X --> 0 -> non non-empty ;

coherence
not X --> 0 is non-empty

proof end;

end;

registration

cluster Relation-like positive-yielding -> non-empty nonnegative-yielding for set ;

coherence
for b₁ being Relation st b₁ is positive-yielding holds
( b₁ is nonnegative-yielding & b₁ is non-empty ) ;

cluster Relation-like negative-yielding -> non-empty nonpositive-yielding for set ;

coherence
for b₁ being Relation st b₁ is negative-yielding holds
( b₁ is nonpositive-yielding & b₁ is non-empty ) ;

end;

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

registration

let X be set ;

cluster Relation-like X -defined REAL -valued Function-like total V36(X, REAL ) complex-valued ext-real-valued real-valued negative-yielding for Element of K16(K17(X,REAL));

existence
ex b₁ being Function of X,REAL st b₁ is negative-yielding

proof end;

cluster Relation-like X -defined REAL -valued Function-like total V36(X, REAL ) complex-valued ext-real-valued real-valued positive-yielding for Element of K16(K17(X,REAL));

existence
ex b₁ being Function of X,REAL st b₁ is positive-yielding

proof end;

end;

registration

cluster Relation-like non-empty Function-like real-valued for set ;

existence
ex b₁ being Function st
( b₁ is non-empty & b₁ 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 f + g -> nonpositive-yielding ;

coherence
f + g is nonpositive-yielding

proof end;

end;

registration

let X be set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;

cluster f + g -> nonnegative-yielding ;

coherence
f + g is nonnegative-yielding

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 f + g -> positive-yielding ;

coherence
f + g is positive-yielding

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 f + 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;

cluster f + g -> negative-yielding ;

coherence
f + g is negative-yielding

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 f + 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;

cluster f - g -> nonnegative-yielding ;

coherence
f - g is nonnegative-yielding

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 f - g -> nonpositive-yielding ;

coherence
f - g is nonpositive-yielding

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 f - g -> positive-yielding ;

coherence
f - g is positive-yielding

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 f - g -> negative-yielding ;

coherence
f - g is negative-yielding

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 f - g -> negative-yielding ;

coherence
f - g is negative-yielding

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 f - g -> positive-yielding ;

coherence
f - g is positive-yielding

proof end;

end;

registration

let X be set ;
let f, g be nonpositive-yielding PartFunc of X,REAL;

cluster f (#) g -> nonnegative-yielding ;

coherence
f (#) g is nonnegative-yielding

proof end;

end;

registration

let X be set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;

cluster f (#) g -> nonnegative-yielding ;

coherence
f (#) g is nonnegative-yielding

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 f (#) g -> nonpositive-yielding ;

coherence
f (#) g is nonpositive-yielding

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 f (#) 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;

cluster f (#) g -> negative-yielding ;

coherence
f (#) g is negative-yielding

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 f (#) 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;

cluster f (#) g -> positive-yielding ;

coherence
f (#) g is positive-yielding

proof end;

end;

registration

let X be set ;
let f, g be negative-yielding PartFunc of X,REAL;

cluster f (#) g -> positive-yielding ;

coherence
f (#) g is positive-yielding

proof end;

end;

registration

let X be set ;
let f, g be non-empty PartFunc of X,REAL;

cluster 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 f (#) f -> nonnegative-yielding ;

coherence
f (#) f is nonnegative-yielding

proof end;

end;

registration

let X be set ;
let r be non positive Real;
let f be nonpositive-yielding PartFunc of X,REAL;

cluster r (#) f -> nonnegative-yielding ;

coherence
r (#) f is nonnegative-yielding

proof end;

end;

registration

let X be set ;
let r be non negative Real;
let f be nonnegative-yielding PartFunc of X,REAL;

cluster r (#) f -> nonnegative-yielding ;

coherence
r (#) f is nonnegative-yielding

proof end;

end;

registration

let X be set ;
let r be non positive Real;
let f be nonnegative-yielding PartFunc of X,REAL;

cluster r (#) f -> nonpositive-yielding ;

coherence
r (#) f is nonpositive-yielding

proof end;

end;

registration

let X be set ;
let r be non negative Real;
let f be nonpositive-yielding PartFunc of X,REAL;

cluster r (#) f -> nonpositive-yielding ;

coherence
r (#) f is nonpositive-yielding

proof end;

end;

registration

let X be set ;
let r be positive Real;
let f be negative-yielding PartFunc of X,REAL;

cluster r (#) f -> negative-yielding ;

coherence
r (#) f is negative-yielding

proof end;

end;

registration

let X be set ;
let r be negative Real;
let f be positive-yielding PartFunc of X,REAL;

cluster r (#) f -> negative-yielding ;

coherence
r (#) f is negative-yielding

proof end;

end;

registration

let X be set ;
let r be positive Real;
let f be positive-yielding PartFunc of X,REAL;

cluster r (#) f -> positive-yielding ;

coherence
r (#) f is positive-yielding

proof end;

end;

registration

let X be set ;
let r be negative Real;
let f be negative-yielding PartFunc of X,REAL;

cluster r (#) f -> positive-yielding ;

coherence
r (#) f is positive-yielding

proof end;

end;

registration

let X be set ;
let r be non zero Real;
let f be non-empty PartFunc of X,REAL;

cluster r (#) f -> 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 f / g -> nonnegative-yielding ;

coherence
f / g is nonnegative-yielding

proof end;

end;

registration

let X be non empty set ;
let f, g be nonnegative-yielding PartFunc of X,REAL;

cluster f / g -> nonnegative-yielding ;

coherence
f / g is nonnegative-yielding

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 f / g -> nonpositive-yielding ;

coherence
f / g is nonpositive-yielding

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 f / g -> nonpositive-yielding ;

coherence
f / g is nonpositive-yielding

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 f / g -> negative-yielding ;

coherence
f / g is negative-yielding

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 f / g -> negative-yielding ;

coherence
f / g is negative-yielding

proof end;

end;

registration

let X be non empty set ;
let f, g be positive-yielding PartFunc of X,REAL;

cluster f / g -> positive-yielding ;

coherence
f / g is positive-yielding

proof end;

end;

registration

let X be non empty set ;
let f, g be negative-yielding PartFunc of X,REAL;

cluster f / g -> positive-yielding ;

coherence
f / g is positive-yielding

proof end;

end;

registration

let X be non empty set ;
let f be PartFunc of X,REAL;

cluster f / f -> nonnegative-yielding ;

coherence
f / f is nonnegative-yielding

proof end;

end;

registration

let X be non empty set ;
let f, g be non-empty PartFunc of X,REAL;

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

cluster Inv f -> nonpositive-yielding ;

coherence
Inv f is nonpositive-yielding

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

end;

registration

let X be non empty set ;
let f be nonpositive-yielding Function of X,REAL;

cluster f ^ -> nonpositive-yielding ;

coherence
f ^ is nonpositive-yielding

proof end;

end;

registration

let X be non empty set ;
let f be nonnegative-yielding Function of X,REAL;

cluster f ^ -> nonnegative-yielding ;

coherence
f ^ is nonnegative-yielding

proof end;

end;

registration

let X be non empty set ;
let f be positive-yielding Function of X,REAL;

cluster f ^ -> positive-yielding ;

coherence
f ^ is positive-yielding

proof end;

end;

registration

let X be non empty set ;
let f be negative-yielding Function of X,REAL;

cluster f ^ -> negative-yielding ;

coherence
f ^ is negative-yielding

proof end;

end;

registration

let X be non empty set ;
let f be non-empty Function of X,REAL;

cluster 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 b₁ being Function st
( dom b₁ = dom f & ( for x being object st x in dom b₁ holds
b₁ . x = sqrt (f . x) ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom f & ( for x being object st x in dom b₁ holds
b₁ . x = sqrt (f . x) ) & dom b₂ = dom f & ( for x being object st x in dom b₂ holds
b₂ . x = sqrt (f . x) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines sqrt PARTFUN3:def 5 :
for f being real-valued Function
for b₂ being Function holds
( b₂ = sqrt f iff ( dom b₂ = dom f & ( for x being object st x in dom b₂ holds
b₂ . x = sqrt (f . x) ) ) );

registration

let f be real-valued Function;

cluster sqrt f -> real-valued ;

coherence
sqrt f is real-valued

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;

cluster sqrt f -> nonnegative-yielding ;

coherence
sqrt f is nonnegative-yielding

proof end;

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

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;