:: 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, ORDINAL4, VALUED_1,
COMPLEX1, PRE_TOPC, ORDINAL2, PSCOMP_1, STRUCT_0, TOPMETR, REAL_1,
RCOMP_1, PARTFUN3;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, COMPLEX1, SQUARE_1, FUNCT_1,
RELSET_1, PSCOMP_1, VALUED_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
REAL_1, FUNCOP_1, RCOMP_1, STRUCT_0, PRE_TOPC, TOPALG_2, PARTFUN3;
constructors REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, FUNCOP_1, TOPALG_2,
PSCOMP_1, PARTFUN3, NUMBERS;
registrations XBOOLE_0, FUNCT_1, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC, TOPMETR, VALUED_0, FUNCT_2,
PSCOMP_1, PARTFUN3, RELAT_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin
reserve T for non empty TopSpace,
f, g for continuous RealMap of T,
r for Real;
registration
let T, f, g;
cluster f+g -> continuous for RealMap of T;
cluster f-g -> continuous for RealMap of T;
cluster f(#)g -> continuous for RealMap of T;
end;
registration
let T, f;
cluster -f -> continuous for RealMap of T;
end;
registration
let T, f;
cluster abs f -> continuous for RealMap of T;
end;
registration
let T;
cluster positive-yielding continuous for RealMap of T;
cluster negative-yielding continuous for RealMap of T;
end;
registration
let T;
let f be nonnegative-yielding continuous RealMap of T;
cluster sqrt f -> continuous for RealMap of T;
end;
registration
let T, f, r;
cluster r(#)f -> continuous for RealMap of T;
end;
registration
let T;
let f be non-empty continuous RealMap of T;
cluster f^ -> continuous for RealMap of T;
end;
registration
let T, f;
let g be non-empty continuous RealMap of T;
cluster f/g -> continuous for RealMap of T;
end;