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

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions PSCOMP_1;
theorems FUNCT_2, RELAT_1, FUNCT_1, ZFMISC_1, JGRAPH_2, XBOOLE_1, XBOOLE_0, FUNCOP_1, TOPMETR, RFUNCT_1, XCMPLX_0, JGRAPH_3, JGRAPH_4, VALUED_1, PARTFUN3, JORDAN5A, XREAL_0;
schemes ;
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;
constructors HIDDEN, REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, FUNCOP_1, TOPALG_2, PSCOMP_1, PARTFUN3, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities STRUCT_0, ORDINAL1;
expansions ;


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

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