:: PARTFUN4 semantic presentation 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 proof consider H being Function of T,R^1 such that A1: for p being Point of T for r1, r2 being real number st F . p = r1 & G . p = r2 holds H . p = r1 + r2 and A2: H is continuous by JGRAPH_2:19; reconsider h = H as RealMap of T by TOPMETR:17; A3: dom h = the carrier of T /\ the carrier of T by FUNCT_2:def_1 .= the carrier of T /\ (dom g) by FUNCT_2:def_1 .= (dom f) /\ (dom g) by FUNCT_2:def_1 ; for c being set st c in dom h holds h . c = (f . c) + (g . c) by A1; then h = f + g by A3, VALUED_1:def_1; hence for b1 being RealMap of T st b1 = f + g holds b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum end; clusterf - g -> continuous for RealMap of T; coherence for b1 being RealMap of T st b1 = f - g holds b1 is continuous proof consider H being Function of T,R^1 such that A4: for p being Point of T for r1, r2 being real number st F . p = r1 & G . p = r2 holds H . p = r1 - r2 and A5: H is continuous by JGRAPH_2:21; reconsider h = H as RealMap of T by TOPMETR:17; A6: dom h = the carrier of T /\ the carrier of T by FUNCT_2:def_1 .= the carrier of T /\ (dom g) by FUNCT_2:def_1 .= (dom f) /\ (dom g) by FUNCT_2:def_1 ; ( dom (f - g) = (dom f) /\ (dom g) & ( for c being set st c in dom h holds h . c = (f . c) - (g . c) ) ) by A4, VALUED_1:12; then h = f - g by A6, VALUED_1:14; hence for b1 being RealMap of T st b1 = f - g holds b1 is continuous by A5, JORDAN5A:27; ::_thesis: verum end; clusterf (#) g -> continuous for RealMap of T; coherence for b1 being RealMap of T st b1 = f (#) g holds b1 is continuous proof consider H being Function of T,R^1 such that A7: for p being Point of T for r1, r2 being real number st F . p = r1 & G . p = r2 holds H . p = r1 * r2 and A8: H is continuous by JGRAPH_2:25; reconsider h = H as RealMap of T by TOPMETR:17; A9: dom h = the carrier of T /\ the carrier of T by FUNCT_2:def_1 .= the carrier of T /\ (dom g) by FUNCT_2:def_1 .= (dom f) /\ (dom g) by FUNCT_2:def_1 ; for c being set st c in dom h holds h . c = (f . c) * (g . c) by A7; then h = f (#) g by A9, VALUED_1:def_4; hence for b1 being RealMap of T st b1 = f (#) g holds b1 is continuous by A8, JORDAN5A:27; ::_thesis: verum 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 reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17; set c = the carrier of T; consider H being Function of T,R^1 such that A1: for p being Point of T for r1 being real number st F . p = r1 holds H . p = - r1 and A2: H is continuous by JGRAPH_4:8; reconsider h = H as RealMap of T by TOPMETR:17; A3: dom h = the carrier of T by FUNCT_2:def_1 .= dom f by FUNCT_2:def_1 ; for c being set st c in dom h holds h . c = - (f . c) by A1; then h = - f by A3, VALUED_1:9; hence for b1 being RealMap of T st b1 = - f holds b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum 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 reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17; set c = the carrier of T; consider H being Function of T,R^1 such that A1: for p being Point of T for r1 being real number st F . p = r1 holds H . p = abs r1 and A2: H is continuous by JGRAPH_4:7; reconsider h = H as RealMap of T by TOPMETR:17; A3: dom h = the carrier of T by FUNCT_2:def_1 .= dom f by FUNCT_2:def_1 ; for c being set st c in dom h holds h . c = abs (f . c) by A1; then h = abs f by A3, VALUED_1:def_11; hence for b1 being RealMap of T st b1 = abs f holds b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum end; 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 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; 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 ) proof take f = the carrier of T --> 1; ::_thesis: ( f is positive-yielding & f is continuous ) thus f is positive-yielding ; ::_thesis: f is continuous thus f is continuous by Lm1; ::_thesis: verum end; 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 ) proof take f = the carrier of T --> (- 1); ::_thesis: ( f is negative-yielding & f is continuous ) thus f is negative-yielding ; ::_thesis: f is continuous thus f is continuous by Lm1; ::_thesis: verum 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 reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17; set c = the carrier of T; for q being Point of T ex r being real number st ( f . q = r & r >= 0 ) proof let q be Point of T; ::_thesis: ex r being real number st ( f . q = r & r >= 0 ) take f . q ; ::_thesis: ( f . q = f . q & f . q >= 0 ) thus f . q = f . q ; ::_thesis: f . q >= 0 dom f = the carrier of T by FUNCT_2:def_1; then f . q in rng f by FUNCT_1:def_3; hence f . q >= 0 by PARTFUN3:def_4; ::_thesis: verum end; then consider H being Function of T,R^1 such that A1: for p being Point of T for r1 being real number st F . p = r1 holds H . p = sqrt r1 and A2: H is continuous by JGRAPH_3:5; reconsider h = H as RealMap of T by TOPMETR:17; A3: dom h = the carrier of T by FUNCT_2:def_1 .= dom f by FUNCT_2:def_1 ; for c being set st c in dom h holds h . c = sqrt (f . c) by A1; then h = sqrt f by A3, PARTFUN3:def_5; hence for b1 being RealMap of T st b1 = sqrt f holds b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum end; 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 proof reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17; set c = the carrier of T; consider H being Function of T,R^1 such that A1: for p being Point of T for r1 being real number st F . p = r1 holds H . p = r * r1 and A2: H is continuous by JGRAPH_2:23; reconsider h = H as RealMap of T by TOPMETR:17; A3: dom h = the carrier of T by FUNCT_2:def_1 .= dom f by FUNCT_2:def_1 ; for c being set st c in dom h holds h . c = r * (f . c) by A1; then h = r (#) f by A3, VALUED_1:def_5; hence for b1 being RealMap of T st b1 = r (#) f holds b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum end; 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 proof reconsider F = f as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17; set c = the carrier of T; for q being Point of T holds f . q <> 0 proof let q be Point of T; ::_thesis: f . q <> 0 dom f = the carrier of T by FUNCT_2:def_1; hence f . q <> 0 ; ::_thesis: verum end; then consider H being Function of T,R^1 such that A1: for p being Point of T for r1 being real number st F . p = r1 holds H . p = 1 / r1 and A2: H is continuous by JGRAPH_2:26; reconsider h = H as RealMap of T by TOPMETR:17; A3: now__::_thesis:_for_a_being_set_st_a_in_dom_h_holds_ h_._a_=_(f_._a)_" let a be set ; ::_thesis: ( a in dom h implies h . a = (f . a) " ) assume a in dom h ; ::_thesis: h . a = (f . a) " hence h . a = 1 / (f . a) by A1 .= 1 * ((f . a) ") by XCMPLX_0:def_9 .= (f . a) " ; ::_thesis: verum end; dom h = the carrier of T by FUNCT_2:def_1 .= (dom f) \ (f " {0}) by FUNCT_2:def_1 ; then h = f ^ by A3, RFUNCT_1:def_2; hence for b1 being RealMap of T st b1 = f ^ holds b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum 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; clusterK495(f,g) -> continuous for RealMap of T; coherence for b1 being RealMap of T st b1 = f / g holds b1 is continuous proof reconsider F = f, G = g as continuous Function of T,R^1 by JORDAN5A:27, TOPMETR:17; set c = the carrier of T; for q being Point of T holds g . q <> 0 proof let q be Point of T; ::_thesis: g . q <> 0 dom g = the carrier of T by FUNCT_2:def_1; hence g . q <> 0 ; ::_thesis: verum end; then consider H being Function of T,R^1 such that A1: for p being Point of T for r1, r2 being real number st F . p = r1 & G . p = r2 holds H . p = r1 / r2 and A2: H is continuous by JGRAPH_2:27; reconsider h = H as RealMap of T by TOPMETR:17; A3: now__::_thesis:_for_c_being_set_st_c_in_dom_h_holds_ h_._c_=_(f_._c)_*_((g_._c)_") let c be set ; ::_thesis: ( c in dom h implies h . c = (f . c) * ((g . c) ") ) assume c in dom h ; ::_thesis: h . c = (f . c) * ((g . c) ") hence h . c = (f . c) / (g . c) by A1 .= (f . c) * ((g . c) ") by XCMPLX_0:def_9 ; ::_thesis: verum end; dom h = the carrier of T /\ the carrier of T by FUNCT_2:def_1 .= the carrier of T /\ (dom g) by FUNCT_2:def_1 .= (dom f) /\ ((dom g) \ (g " {0})) by FUNCT_2:def_1 ; then h = f / g by A3, RFUNCT_1:def_1; hence for b1 being RealMap of T st b1 = f / g holds b1 is continuous by A2, JORDAN5A:27; ::_thesis: verum end; end;