:: On the Real Valued Functions
:: by Artur Korni{\l}owicz
::
:: Received December 10, 2004
:: Copyright (c) 2004-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ARYTM_3, XXREAL_0, CARD_1, RELAT_1, SQUARE_1, FUNCT_1,
TARSKI, XBOOLE_0, FUNCOP_1, ARYTM_1, SUBSET_1, VALUED_0, ORDINAL4,
PARTFUN1, VALUED_1, XCMPLX_0, PRALG_1, COMPLEX1, MEMBERED, PARTFUN3,
REAL_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, COMPLEX1, MEMBERED, SQUARE_1,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, MEASURE6, VALUED_0,
VALUED_1, RFUNCT_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1,
FUNCOP_1;
constructors REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, RFUNCT_1, MEASURE6,
FUNCOP_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, FUNCT_1, RELSET_1, FUNCOP_1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, ORDINAL1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin
registration
let r be Real;
cluster r/r -> non negative;
end;
registration
let r be Real;
cluster r*r -> non negative;
cluster r*(r") -> non negative;
end;
registration
let r be non negative Real;
cluster sqrt r -> non negative;
end;
registration
let r be positive Real;
cluster sqrt r -> positive;
end;
theorem :: PARTFUN3:1
for f being Function, A being set st f is one-to-one & A c= dom (f")
holds f.:(f".:A) = A;
registration
let f be non-empty Function;
cluster f"{0} -> empty;
end;
definition
let R be Relation;
attr R is positive-yielding means
:: PARTFUN3:def 1
for r being Real st r in rng R holds 0 < r;
attr R is negative-yielding means
:: PARTFUN3:def 2
for r being Real st r in rng R holds 0 > r;
attr R is nonpositive-yielding means
:: PARTFUN3:def 3
for r being Real st r in rng R holds 0 >= r;
attr R is nonnegative-yielding means
:: PARTFUN3:def 4
for r being Real st r in rng R holds 0 <= r;
end;
registration
let X be set, r be positive Real;
cluster X --> r -> positive-yielding;
end;
registration
let X be set, r be negative Real;
cluster X --> r -> negative-yielding;
end;
registration
let X be set, r be non positive Real;
cluster X --> r -> nonpositive-yielding;
end;
registration
let X be set, r be non negative Real;
cluster X --> r -> nonnegative-yielding;
end;
registration
let X be non empty set;
cluster X --> 0 -> non non-empty;
end;
registration
cluster positive-yielding -> nonnegative-yielding non-empty for Relation;
cluster negative-yielding -> nonpositive-yielding non-empty for Relation;
end;
registration
let X be set;
cluster negative-yielding for Function of X,REAL;
cluster positive-yielding for Function of X,REAL;
end;
registration
cluster non-empty real-valued for Function;
end;
theorem :: PARTFUN3:2
for f being non-empty real-valued Function holds dom(f^) = dom f;
theorem :: PARTFUN3:3
for X being non empty set, f being PartFunc of X,REAL, g being
non-empty PartFunc of X,REAL holds dom(f/g) = dom f /\ dom g;
registration
let X be set;
let f, g be nonpositive-yielding PartFunc of X,REAL;
cluster f+g -> nonpositive-yielding;
end;
registration
let X be set;
let f, g be nonnegative-yielding PartFunc of X,REAL;
cluster f+g -> nonnegative-yielding;
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;
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;
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;
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;
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;
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;
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;
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;
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;
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;
end;
registration
let X be set;
let f, g be nonpositive-yielding PartFunc of X,REAL;
cluster f(#)g -> nonnegative-yielding;
end;
registration
let X be set;
let f, g be nonnegative-yielding PartFunc of X,REAL;
cluster f(#)g -> nonnegative-yielding;
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;
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;
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;
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;
end;
registration
let X be set;
let f, g be positive-yielding PartFunc of X,REAL;
cluster f(#)g -> positive-yielding;
end;
registration
let X be set;
let f, g be negative-yielding PartFunc of X,REAL;
cluster f(#)g -> positive-yielding;
end;
registration
let X be set;
let f, g be non-empty PartFunc of X,REAL;
cluster f(#)g -> non-empty;
end;
registration
let X be set;
let f be PartFunc of X,REAL;
cluster f(#)f -> nonnegative-yielding;
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;
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;
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;
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;
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;
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;
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;
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;
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;
end;
registration
let X be non empty set;
let f, g be nonpositive-yielding PartFunc of X,REAL;
cluster f/g -> nonnegative-yielding;
end;
registration
let X be non empty set;
let f, g be nonnegative-yielding PartFunc of X,REAL;
cluster f/g -> nonnegative-yielding;
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;
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;
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;
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;
end;
registration
let X be non empty set;
let f, g be positive-yielding PartFunc of X,REAL;
cluster f/g -> positive-yielding;
end;
registration
let X be non empty set;
let f, g be negative-yielding PartFunc of X,REAL;
cluster f/g -> positive-yielding;
end;
registration
let X be non empty set;
let f be PartFunc of X,REAL;
cluster f/f -> nonnegative-yielding;
end;
registration
let X be non empty set;
let f, g be non-empty PartFunc of X,REAL;
cluster f/g -> non-empty;
end;
registration
let X be set;
let f be nonpositive-yielding Function of X,REAL;
cluster Inv f -> nonpositive-yielding;
end;
registration
let X be set;
let f be nonnegative-yielding Function of X,REAL;
cluster Inv f -> nonnegative-yielding;
end;
registration
let X be set;
let f be positive-yielding Function of X,REAL;
cluster Inv f -> positive-yielding;
end;
registration
let X be set;
let f be negative-yielding Function of X,REAL;
cluster Inv f -> negative-yielding;
end;
registration
let X be set;
let f be non-empty Function of X,REAL;
cluster Inv f -> non-empty;
end;
registration
let X be set;
let f be non-empty Function of X,REAL;
cluster -f -> non-empty;
end;
registration
let X be set;
let f be nonpositive-yielding Function of X,REAL;
cluster -f -> nonnegative-yielding;
end;
registration
let X be set;
let f be nonnegative-yielding Function of X,REAL;
cluster -f -> nonpositive-yielding;
end;
registration
let X be set;
let f be positive-yielding Function of X,REAL;
cluster -f -> negative-yielding;
end;
registration
let X be set;
let f be negative-yielding Function of X,REAL;
cluster -f -> positive-yielding;
end;
registration
let X be set;
let f be Function of X,REAL;
cluster abs f -> nonnegative-yielding;
end;
registration
let X be set;
let f be non-empty Function of X,REAL;
cluster abs f -> positive-yielding;
end;
registration
let X be non empty set;
let f be nonpositive-yielding Function of X,REAL;
cluster f^ -> nonpositive-yielding;
end;
registration
let X be non empty set;
let f be nonnegative-yielding Function of X,REAL;
cluster f^ -> nonnegative-yielding;
end;
registration
let X be non empty set;
let f be positive-yielding Function of X,REAL;
cluster f^ -> positive-yielding;
end;
registration
let X be non empty set;
let f be negative-yielding Function of X,REAL;
cluster f^ -> negative-yielding;
end;
registration
let X be non empty set;
let f be non-empty Function of X,REAL;
cluster f^ -> non-empty;
end;
definition
let f be real-valued Function;
func sqrt f -> Function means
:: PARTFUN3:def 5
dom it = dom f & for x being object st x in dom it holds it.x = sqrt(f.x);
end;
registration
let f be real-valued Function;
cluster sqrt f -> real-valued;
end;
definition
let C be set, D be real-membered set, f be PartFunc of C,D;
redefine func sqrt f -> PartFunc of C,REAL;
end;
registration
let X be set;
let f be nonnegative-yielding Function of X,REAL;
cluster sqrt f -> nonnegative-yielding;
end;
registration
let X be set;
let f be positive-yielding Function of X,REAL;
cluster sqrt f -> positive-yielding;
end;
definition
let X be set, f be Function of X, REAL;
redefine func sqrt f -> Function of X,REAL;
end;
definition
let X be set, f be non-empty Function of X, REAL;
redefine func f^ -> Function of X,REAL;
end;
definition
let X be non empty set, f be Function of X, REAL, g be non-empty Function of
X, REAL;
redefine func f/g -> Function of X,REAL;
end;