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

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 ;
cluster f + g -> continuous for RealMap of T;
coherence
for b1 being RealMap of T st b1 = f + g holds
b1 is continuous
proof end;
cluster f - g -> continuous for RealMap of T;
coherence
for b1 being RealMap of T st b1 = f - g holds
b1 is continuous
proof end;
cluster f (#) g -> continuous for RealMap of T;
coherence
for b1 being RealMap of T st b1 = f (#) g holds
b1 is continuous
proof end;
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
proof end;
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
proof end;
end;

Lm1: now :: thesis: for T being non empty TopSpace
for a being Element of REAL holds the carrier of T --> a is continuous
let T be non empty TopSpace; :: thesis: for a being Element of REAL holds the carrier of T --> a is continuous
let a be Element of 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 to PSCOMP_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;
per cases ( 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 ;
( 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
.= the carrier of T by
.= [#] 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 ;
( 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
.= {} T ;
hence ( the carrier of T --> a) " Y is closed ; :: thesis: verum
end;
end;
end;
end;

reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

registration
let T be non empty TopSpace;
cluster V1() V4( the carrier of T) V5( REAL ) non empty Function-like V32( the carrier of T) V36( the carrier of T, REAL ) V145() V146() V147() continuous positive-yielding for Element of K16(K17( the carrier of T,REAL));
existence
ex b1 being RealMap of T st
( b1 is positive-yielding & b1 is continuous )
proof end;
cluster V1() V4( the carrier of T) V5( REAL ) non empty Function-like V32( the carrier of T) V36( the carrier of T, REAL ) V145() V146() V147() continuous negative-yielding for Element of K16(K17( the carrier of T,REAL));
existence
ex b1 being RealMap of T st
( b1 is negative-yielding & b1 is continuous )
proof end;
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
proof end;
end;

registration
let T be non empty TopSpace;
let f be continuous RealMap of T;
let r be Real;
cluster r (#) f -> continuous for RealMap of T;
coherence
for b1 being RealMap of T st b1 = r (#) f holds
b1 is continuous
proof end;
end;

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

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