:: On the Real Valued Functions
:: by Artur Korni{\l}owicz
::
:: Received December 10, 2004
:: Copyright (c) 2004-2012 Association of Mizar Users


begin

registration
let T be non empty TopSpace;
let f, g be continuous RealMap of T;
set c = the carrier of T;
reconsider F = f, G = g as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17;
clusterf + g ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = f + g holds
b1 is continuous
proofend;
clusterf - g ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = f - g holds
b1 is continuous
proofend;
clusterf (#) g ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = f (#) g holds
b1 is continuous
proofend;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
cluster - f ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = - f holds
b1 is continuous
proofend;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
cluster|.f.| ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = abs f holds
b1 is continuous
proofend;
end;

Lm1: now__::_thesis:_for_T_being_non_empty_TopSpace
for_a_being_Real_holds_the_carrier_of_T_-->_a_is_continuous
let T be non empty TopSpace; ::_thesis: for a being Real holds the carrier of T --> a is continuous
let a be Real; ::_thesis: the carrier of T --> a is continuous
set c = the carrier of T;
set f = the carrier of T --> a;
thus  the carrier of T --> a is continuous ::_thesis: verum
proof
let Y be Subset of REAL; :: according toPSCOMP_1:def_3 ::_thesis: ( not Y is closed or ( the carrier of T --> a) " Y is closed )
A1: dom ( the carrier of T --> a) = the carrier of T by FUNCT_2:def_1;
assume  Y is closed ; ::_thesis: ( the carrier of T --> a) " Y is closed
A2: rng ( the carrier of T --> a) = {a} by FUNCOP_1:8;
percases ( a in Y or not a in Y ) ;
suppose a in Y ; ::_thesis: ( the carrier of T --> a) " Y is closed
then A3: rng ( the carrier of T --> a) c= Y by A2, ZFMISC_1:31;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " (rng ( the carrier of T --> a)) by A3, XBOOLE_1:28
.= the carrier of T by A1, RELAT_1:134
.= [#] T ;
hence  ( the carrier of T --> a) " Y is closed ; ::_thesis: verum
end;
suppose not a in Y ; ::_thesis: ( the carrier of T --> a) " Y is closed
then A4: rng ( the carrier of T --> a) misses Y by A2, ZFMISC_1:50;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " {} by A4, XBOOLE_0:def_7
.= {} T ;
hence  ( the carrier of T --> a) " Y is closed ; ::_thesis: verum
end;
end;
end;
end;

registration
let T be non empty TopSpace;
cluster non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous positive-yielding for Element of K6(K7( the carrier of T,REAL));
existence
 ex b1 being RealMap of T st
( b1 is positive-yielding & b1 is continuous )
proofend;
cluster non empty V19() V22( the carrier of T) V23( REAL ) Function-like V29( the carrier of T) V33( the carrier of T, REAL ) V141() V142() V143() continuous negative-yielding for Element of K6(K7( the carrier of T,REAL));
existence
 ex b1 being RealMap of T st
( b1 is negative-yielding & b1 is continuous )
proofend;
end;

registration
let T be non empty TopSpace;
let f be continuous nonnegative-yielding RealMap of T;
cluster sqrt f ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = sqrt f holds
b1 is continuous
proofend;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
let r be real number ;
clusterr (#) f ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = r (#) f holds
b1 is continuous
proofend;
end;

registration
let T be non empty TopSpace;
let f be non-empty continuous RealMap of T;
clusterK498(f) ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = f ^ holds
b1 is continuous
proofend;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
let g be non-empty continuous RealMap of T;
clusterK495(f,g) ->  continuous for RealMap of T;
coherence
 for b1 being RealMap of T st b1 = f / g holds
b1 is continuous
proofend;
end;