:: 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 JORDAN5A:27, TOPMETR:17;

coherence

for b_{1} being RealMap of T st b_{1} = f + g holds

b_{1} is continuous

for b_{1} being RealMap of T st b_{1} = f - g holds

b_{1} is continuous

for b_{1} being RealMap of T st b_{1} = f (#) g holds

b_{1} is continuous

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

coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

registration

let T be non empty TopSpace;

let f be continuous RealMap of T;

coherence

for b_{1} being RealMap of T st b_{1} = - f holds

b_{1} is continuous

end;
let f be continuous RealMap of T;

coherence

for b

b

proof end;

registration

let T be non empty TopSpace;

let f be continuous RealMap of T;

coherence

for b_{1} being RealMap of T st b_{1} = abs f holds

b_{1} is continuous

end;
let f be continuous RealMap of T;

coherence

for b

b

proof end;

Lm1: now :: thesis: for T being non empty TopSpace

for a being Element of REAL holds the carrier of T --> a is continuous

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

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

end;
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 )
;

end;

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

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

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

registration

let T be non empty TopSpace;

ex b_{1} being RealMap of T st

( b_{1} is positive-yielding & b_{1} is continuous )

ex b_{1} being RealMap of T st

( b_{1} is negative-yielding & b_{1} is continuous )

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 positive-yielding for Element of K16(K17( the carrier of T,REAL));

existence ex b

( b

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 b

( b

proof end;

registration

let T be non empty TopSpace;

let f be continuous nonnegative-yielding RealMap of T;

coherence

for b_{1} being RealMap of T st b_{1} = sqrt f holds

b_{1} is continuous

end;
let f be continuous nonnegative-yielding RealMap of T;

coherence

for b

b

proof end;

registration

let T be non empty TopSpace;

let f be continuous RealMap of T;

let r be Real;

coherence

for b_{1} being RealMap of T st b_{1} = r (#) f holds

b_{1} is continuous

end;
let f be continuous RealMap of T;

let r be Real;

coherence

for b

b

proof end;

registration

let T be non empty TopSpace;

let f be non-empty continuous RealMap of T;

coherence

for b_{1} being RealMap of T st b_{1} = f ^ holds

b_{1} is continuous

end;
let f be non-empty continuous RealMap of T;

coherence

for b

b

proof end;

registration

let T be non empty TopSpace;

let f be continuous RealMap of T;

let g be non-empty continuous RealMap of T;

coherence

for b_{1} being RealMap of T st b_{1} = f / g holds

b_{1} is continuous

end;
let f be continuous RealMap of T;

let g be non-empty continuous RealMap of T;

coherence

for b

b

proof end;