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