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