:: by Artur Korni{\l}owicz

::

:: Received December 10, 2004

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

begin

registration
end;

registration

let r be real number ;

coherence

not r * r is negative by XREAL_1:63;

coherence

not r * (r ") is negative

end;
coherence

not r * r is negative by XREAL_1:63;

coherence

not r * (r ") is negative

proof end;

registration
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

for A being set st f is one-to-one & A c= dom (f ") holds

f .: ((f ") .: A) = A

proof end;

registration
end;

definition

let R be Relation;

end;
attr R is positive-yielding means :Def1: :: PARTFUN3:def 1

for r being real number st r in rng R holds

0 < r;

for r being real number st r in rng R holds

0 < r;

attr R is negative-yielding means :Def2: :: PARTFUN3:def 2

for r being real number st r in rng R holds

0 > r;

for r being real number st r in rng R holds

0 > r;

attr R is nonpositive-yielding means :Def3: :: PARTFUN3:def 3

for r being real number st r in rng R holds

0 >= r;

for r being real number st r in rng R holds

0 >= r;

attr R is nonnegative-yielding means :Def4: :: PARTFUN3:def 4

for r being real number st r in rng R holds

0 <= r;

for r being real number st r in rng R holds

0 <= r;

:: 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 );

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

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

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

for R being Relation holds

( R is nonnegative-yielding iff for r being real number st r in rng R holds

0 <= r );

registration
end;

registration
end;

registration

let X be set ;

let r be real non positive number ;

coherence

X --> r is nonpositive-yielding

end;
let r be real non positive number ;

coherence

X --> r is nonpositive-yielding

proof end;

registration

let X be set ;

let r be real non negative number ;

coherence

X --> r is nonnegative-yielding

end;
let r be real non negative number ;

coherence

X --> r is nonnegative-yielding

proof end;

registration

coherence

for b_{1} being Relation st b_{1} is positive-yielding holds

( b_{1} is nonnegative-yielding & b_{1} is non-empty )

for b_{1} being Relation st b_{1} is negative-yielding holds

( b_{1} is nonpositive-yielding & b_{1} is non-empty )

end;
for b

( b

proof end;

coherence for b

( b

proof end;

registration

let X be set ;

ex b_{1} being Function of X,REAL st b_{1} is negative-yielding

ex b_{1} being Function of X,REAL st b_{1} is positive-yielding

end;
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 b

proof end;

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 b

proof end;

registration
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)

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;

coherence

f + g is nonpositive-yielding

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

coherence

f + g is nonpositive-yielding

proof end;

registration

let X be set ;

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

coherence

f + g is nonnegative-yielding

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

coherence

f + g is nonnegative-yielding

proof end;

registration

let X be set ;

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

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

coherence

f + g is positive-yielding

end;
let f be positive-yielding PartFunc of X,REAL;

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

coherence

f + g is positive-yielding

proof end;

registration

let X be set ;

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

let g be positive-yielding PartFunc of X,REAL;

coherence

f + g is positive-yielding ;

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

let g be positive-yielding PartFunc of X,REAL;

coherence

f + g is positive-yielding ;

registration

let X be set ;

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

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

coherence

f + g is negative-yielding

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

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

coherence

f + g is negative-yielding

proof end;

registration

let X be set ;

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

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

coherence

f + g is negative-yielding ;

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

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

coherence

f + g is negative-yielding ;

registration

let X be set ;

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

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

coherence

f - g is nonnegative-yielding

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

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

coherence

f - g is nonnegative-yielding

proof end;

registration

let X be set ;

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

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

coherence

f - g is nonpositive-yielding

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

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

coherence

f - g is nonpositive-yielding

proof end;

registration

let X be set ;

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

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

coherence

f - g is positive-yielding

end;
let f be positive-yielding PartFunc of X,REAL;

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

coherence

f - g is positive-yielding

proof end;

registration

let X be set ;

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

let g be positive-yielding PartFunc of X,REAL;

coherence

f - g is negative-yielding

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

let g be positive-yielding PartFunc of X,REAL;

coherence

f - g is negative-yielding

proof end;

registration

let X be set ;

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

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

coherence

f - g is negative-yielding

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

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

coherence

f - g is negative-yielding

proof end;

registration

let X be set ;

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

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

coherence

f - g is positive-yielding

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

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

coherence

f - g is positive-yielding

proof end;

registration

let X be set ;

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

coherence

f (#) g is nonnegative-yielding

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

coherence

f (#) g is nonnegative-yielding

proof end;

registration

let X be set ;

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

coherence

f (#) g is nonnegative-yielding

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

coherence

f (#) g is nonnegative-yielding

proof end;

registration

let X be set ;

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

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

coherence

f (#) g is nonpositive-yielding

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

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

coherence

f (#) g is nonpositive-yielding

proof end;

registration

let X be set ;

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

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

coherence

f (#) g is nonpositive-yielding ;

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

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

coherence

f (#) g is nonpositive-yielding ;

registration

let X be set ;

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

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

coherence

f (#) g is negative-yielding

end;
let f be positive-yielding PartFunc of X,REAL;

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

coherence

f (#) g is negative-yielding

proof end;

registration

let X be set ;

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

let g be positive-yielding PartFunc of X,REAL;

coherence

f (#) g is negative-yielding ;

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

let g be positive-yielding PartFunc of X,REAL;

coherence

f (#) g is negative-yielding ;

registration

let X be set ;

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

coherence

f (#) g is positive-yielding

end;
let f, g be positive-yielding PartFunc of X,REAL;

coherence

f (#) g is positive-yielding

proof end;

registration

let X be set ;

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

coherence

f (#) g is positive-yielding

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

coherence

f (#) g is positive-yielding

proof end;

registration
end;

registration
end;

registration

let X be set ;

let r be real non positive number ;

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

coherence

r (#) f is nonnegative-yielding

end;
let r be real non positive number ;

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

coherence

r (#) f is nonnegative-yielding

proof end;

registration

let X be set ;

let r be real non negative number ;

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

coherence

r (#) f is nonnegative-yielding

end;
let r be real non negative number ;

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

coherence

r (#) f is nonnegative-yielding

proof end;

registration

let X be set ;

let r be real non positive number ;

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

coherence

r (#) f is nonpositive-yielding

end;
let r be real non positive number ;

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

coherence

r (#) f is nonpositive-yielding

proof end;

registration

let X be set ;

let r be real non negative number ;

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

coherence

r (#) f is nonpositive-yielding

end;
let r be real non negative number ;

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

coherence

r (#) f is nonpositive-yielding

proof end;

registration

let X be set ;

let r be real positive number ;

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

coherence

r (#) f is negative-yielding

end;
let r be real positive number ;

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

coherence

r (#) f is negative-yielding

proof end;

registration

let X be set ;

let r be real negative number ;

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

coherence

r (#) f is negative-yielding

end;
let r be real negative number ;

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

coherence

r (#) f is negative-yielding

proof end;

registration

let X be set ;

let r be real positive number ;

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

coherence

r (#) f is positive-yielding

end;
let r be real positive number ;

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

coherence

r (#) f is positive-yielding

proof end;

registration

let X be set ;

let r be real negative number ;

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

coherence

r (#) f is positive-yielding

end;
let r be real negative number ;

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

coherence

r (#) f is positive-yielding

proof end;

registration

let X be set ;

let r be non zero real number ;

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

coherence

r (#) f is non-empty

end;
let r be non zero real number ;

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

coherence

r (#) f is non-empty

proof end;

registration

let X be non empty set ;

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

coherence

f / g is nonnegative-yielding

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

coherence

f / g is nonnegative-yielding

proof end;

registration

let X be non empty set ;

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

coherence

f / g is nonnegative-yielding

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

coherence

f / g is nonnegative-yielding

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

coherence

f / g is nonpositive-yielding

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

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

coherence

f / g is nonpositive-yielding

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

coherence

f / g is nonpositive-yielding

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

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

coherence

f / g is nonpositive-yielding

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

coherence

f / g is negative-yielding

end;
let f be positive-yielding PartFunc of X,REAL;

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

coherence

f / g is negative-yielding

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

coherence

f / g is negative-yielding

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

let g be positive-yielding PartFunc of X,REAL;

coherence

f / g is negative-yielding

proof end;

registration

let X be non empty set ;

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

coherence

f / g is positive-yielding

end;
let f, g be positive-yielding PartFunc of X,REAL;

coherence

f / g is positive-yielding

proof end;

registration

let X be non empty set ;

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

coherence

f / g is positive-yielding

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

coherence

f / g is positive-yielding

proof end;

registration

let X be non empty set ;

let f be PartFunc of X,REAL;

coherence

f / f is nonnegative-yielding

end;
let f be PartFunc of X,REAL;

coherence

f / f is nonnegative-yielding

proof end;

registration

let X be non empty set ;

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

coherence

f / g is non-empty

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

coherence

f / g is non-empty

proof end;

registration

let X be set ;

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

coherence

Inv f is nonpositive-yielding

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

coherence

Inv f is nonpositive-yielding

proof end;

registration

let X be set ;

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

coherence

Inv f is nonnegative-yielding

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

coherence

Inv f is nonnegative-yielding

proof end;

registration

let X be set ;

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

coherence

Inv f is positive-yielding

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

coherence

Inv f is positive-yielding

proof end;

registration

let X be set ;

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

coherence

Inv f is negative-yielding

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

coherence

Inv f is negative-yielding

proof end;

registration
end;

registration

let X be set ;

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

coherence

- f is nonnegative-yielding ;

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

coherence

- f is nonnegative-yielding ;

registration

let X be set ;

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

coherence

- f is nonpositive-yielding ;

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

coherence

- f is nonpositive-yielding ;

registration
end;

registration
end;

registration
end;

registration

let X be set ;

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

coherence

abs f is positive-yielding

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

coherence

abs f is positive-yielding

proof end;

registration

let X be non empty set ;

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

coherence

f ^ is nonpositive-yielding

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

coherence

f ^ is nonpositive-yielding

proof end;

registration

let X be non empty set ;

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

coherence

f ^ is nonnegative-yielding

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

coherence

f ^ is nonnegative-yielding

proof end;

registration

let X be non empty set ;

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

coherence

f ^ is positive-yielding

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

coherence

f ^ is positive-yielding

proof end;

registration

let X be non empty set ;

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

coherence

f ^ is negative-yielding

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

coherence

f ^ is negative-yielding

proof end;

registration

let X be non empty set ;

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

coherence

f ^ is non-empty

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

coherence

f ^ is non-empty

proof end;

definition

let f be real-valued Function;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = sqrt (f . x) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being set st x in dom b_{1} holds

b_{1} . x = sqrt (f . x) ) & dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} . x = sqrt (f . x) ) holds

b_{1} = b_{2}

end;
func sqrt f -> Function means :Def5: :: PARTFUN3:def 5

( dom it = dom f & ( for x being set st x in dom it holds

it . x = sqrt (f . x) ) );

existence ( dom it = dom f & ( for x being set st x in dom it holds

it . x = sqrt (f . x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def5 defines sqrt PARTFUN3:def 5 :

for f being real-valued Function

for b_{2} being Function holds

( b_{2} = sqrt f iff ( dom b_{2} = dom f & ( for x being set st x in dom b_{2} holds

b_{2} . x = sqrt (f . x) ) ) );

for f being real-valued Function

for b

( b

b

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

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

registration

let X be set ;

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

coherence

sqrt f is nonnegative-yielding

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

coherence

sqrt f is nonnegative-yielding

proof end;

registration

let X be set ;

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

coherence

sqrt f is positive-yielding

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

coherence

sqrt f is positive-yielding

proof 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

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

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

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

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

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