let CNS be ComplexNormSpace; :: thesis: for RNS being RealNormSpace
for f being PartFunc of RNS,CNS st f is total & ( for x1, x2 being Point of RNS holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of RNS st f is_continuous_in x0 holds
f is_continuous_on the carrier of RNS
let RNS be RealNormSpace; :: thesis: for f being PartFunc of RNS,CNS st f is total & ( for x1, x2 being Point of RNS holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of RNS st f is_continuous_in x0 holds
f is_continuous_on the carrier of RNS
let f be PartFunc of RNS,CNS; :: thesis: ( f is total & ( for x1, x2 being Point of RNS holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ) & ex x0 being Point of RNS st f is_continuous_in x0 implies f is_continuous_on the carrier of RNS )
assume that
A1: f is total and
A2: for x1, x2 being Point of RNS holds f /. (x1 + x2) = (f /. x1) + (f /. x2) ; :: thesis: ( for x0 being Point of RNS holds not f is_continuous_in x0 or f is_continuous_on the carrier of RNS )
A3: dom f = the carrier of RNS by A1, PARTFUN1:def 2;
given x0 being Point of RNS such that A4: f is_continuous_in x0 ; :: thesis: f is_continuous_on the carrier of RNS
(f /. x0) + (0. CNS) = f /. x0 by RLVECT_1:4
.= f /. (x0 + (0. RNS)) by RLVECT_1:4
.= (f /. x0) + (f /. (0. RNS)) by A2 ;
then A5: f /. (0. RNS) = 0. CNS by RLVECT_1:8;
A6: now :: thesis: for x1 being Point of RNS holds - (f /. x1) = f /. (- x1)
let x1 be Point of RNS; :: thesis: - (f /. x1) = f /. (- x1)
0. CNS = f /. (x1 + (- x1)) by A5, RLVECT_1:5
.= (f /. x1) + (f /. (- x1)) by A2 ;
hence - (f /. x1) = f /. (- x1) by RLVECT_1:6; :: thesis: verum
end;
A7: now :: thesis: for x1, x2 being Point of RNS holds f /. (x1 - x2) = (f /. x1) - (f /. x2)
let x1, x2 be Point of RNS; :: thesis: f /. (x1 - x2) = (f /. x1) - (f /. x2)
thus f /. (x1 - x2) = f /. (x1 + (- x2)) by RLVECT_1:def 11
.= (f /. x1) + (f /. (- x2)) by A2
.= (f /. x1) + (- (f /. x2)) by A6
.= (f /. x1) - (f /. x2) by RLVECT_1:def 11 ; :: thesis: verum
end;
now :: thesis: for x1 being Point of RNS
for r being Real st x1 in the carrier of RNS & r > 0 holds
ex s being Real st
( s > 0 & ( for x2 being Point of RNS st x2 in the carrier of RNS & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
let x1 be Point of RNS; :: thesis: for r being Real st x1 in the carrier of RNS & r > 0 holds
ex s being Real st
( s > 0 & ( for x2 being Point of RNS st x2 in the carrier of RNS & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
let r be Real; :: thesis: ( x1 in the carrier of RNS & r > 0 implies ex s being Real st
( s > 0 & ( for x2 being Point of RNS st x2 in the carrier of RNS & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) ) )
assume that
x1 in the carrier of RNS and
A8: r > 0 ; :: thesis: ex s being Real st
( s > 0 & ( for x2 being Point of RNS st x2 in the carrier of RNS & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
set y = x1 - x0;
consider s being Real such that
A9: 0 < s and
A10: for x1 being Point of RNS st x1 in dom f & ||.(x1 - x0).|| < s holds
||.((f /. x1) - (f /. x0)).|| < r by A4, A8, Th10;
take s = s; :: thesis: ( s > 0 & ( for x2 being Point of RNS st x2 in the carrier of RNS & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r ) )
thus s > 0 by A9; :: thesis: for x2 being Point of RNS st x2 in the carrier of RNS & ||.(x2 - x1).|| < s holds
||.((f /. x2) - (f /. x1)).|| < r
let x2 be Point of RNS; :: thesis: ( x2 in the carrier of RNS & ||.(x2 - x1).|| < s implies ||.((f /. x2) - (f /. x1)).|| < r )
assume that
x2 in the carrier of RNS and
A11: ||.(x2 - x1).|| < s ; :: thesis: ||.((f /. x2) - (f /. x1)).|| < r
A12: (x1 - x0) + x0 = x1 - (x0 - x0) by RLVECT_1:29
.= x1 - (0. RNS) by RLVECT_1:15
.= x1 by RLVECT_1:13 ;
then A13: ||.((x2 - (x1 - x0)) - x0).|| = ||.(x2 - x1).|| by RLVECT_1:27;
||.((f /. x2) - (f /. x1)).|| = ||.((f /. x2) - ((f /. (x1 - x0)) + (f /. x0))).|| by A2, A12
.= ||.(((f /. x2) - (f /. (x1 - x0))) - (f /. x0)).|| by RLVECT_1:27
.= ||.((f /. (x2 - (x1 - x0))) - (f /. x0)).|| by A7 ;
hence ||.((f /. x2) - (f /. x1)).|| < r by A3, A10, A11, A13; :: thesis: verum
end;
hence f is_continuous_on the carrier of RNS by A3, Th46; :: thesis: verum