let f, g be PartFunc of REAL,REAL; :: thesis: ( f is continuous & not f is empty & g is continuous & not g is empty & ex a, b, c being Real st
( dom f = [.a,b.] & dom g = [.b,c.] ) & f tolerates g implies ex h being PartFunc of REAL,REAL st
( h = f +* g & ( for x being Real st x in dom h holds
h is_continuous_in x ) ) )
assume A1: ( f is continuous & not f is empty & g is continuous & not g is empty & ex a, b, c being Real st
( dom f = [.a,b.] & dom g = [.b,c.] ) & f tolerates g ) ; :: thesis: ex h being PartFunc of REAL,REAL st
( h = f +* g & ( for x being Real st x in dom h holds
h is_continuous_in x ) )
reconsider ff = f, gg = g as non empty continuous PartFunc of REAL,REAL by A1;
consider a, b, c being Real such that
AB: ( dom f = [.a,b.] & dom g = [.b,c.] ) by A1;
( dom ff <> {} & dom gg <> {} ) ;
then Ab: ( a <= b & b <= c ) by XXREAL_1:29, AB;
AA: (dom f) /\ (dom g) = {b} by XXREAL_1:418, Ab, AB;
reconsider h = f +* g as PartFunc of REAL,REAL ;
take h ; :: thesis: ( h = f +* g & ( for x being Real st x in dom h holds
h is_continuous_in x ) )
thus h = f +* g ; :: thesis: for x being Real st x in dom h holds
h is_continuous_in x
let x be Real; :: thesis: ( x in dom h implies h is_continuous_in x )
J2: h | (dom f) = (g +* f) | (dom f) by FUNCT_4:34, A1
.= f ;
assume JJ: x in dom h ; :: thesis: h is_continuous_in x
per cases then ( x in dom f or x in dom g ) by FUNCT_4:12;
suppose J1: x in dom f ; :: thesis: h is_continuous_in x
set hf = h | (dom f);
set hg = h | (dom g);
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) )
proof
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) ) )
( dom f c= dom h & dom g c= dom h ) by FUNCT_4:10;
then XX: ( dom (h | (dom f)) = dom f & dom (h | (dom g)) = dom g ) by RELAT_1:62;
SF: x in dom (h | (dom f)) by RELAT_1:57, J1, JJ;
assume R0: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) )
then consider s2 being Real such that
SB: ( 0 < s2 & ( for x1 being Real st x1 in dom (h | (dom f)) & |.(x1 - x).| < s2 holds
|.(((h | (dom f)) . x1) - ((h | (dom f)) . x)).| < r / 2 ) ) by J1, J2, A1, FCONT_1:3;
KK: b in (dom f) /\ (dom g) by AA, TARSKI:def 1;
then KA: ( b in dom f & b in dom g ) by XBOOLE_0:def 4;
KI: ( b in dom (h | (dom f)) & b in dom (h | (dom g)) ) by XX, XBOOLE_0:def 4, KK;
consider s1 being Real such that
Sb: ( 0 < s1 & ( for x1 being Real st x1 in dom (h | (dom g)) & |.(x1 - b).| < s1 holds
|.(((h | (dom g)) . x1) - ((h | (dom g)) . b)).| < r / 2 ) ) by FCONT_1:3, R0, A1, KA;
take s = min (s2,s1); :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) )
thus 0 < s by SB, Sb, XXREAL_0:15; :: thesis: for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r
SS: r / 2 < r by XREAL_1:216, R0;
let x1 be Real; :: thesis: ( x1 in dom h & |.(x1 - x).| < s implies |.((h . x1) - (h . x)).| < r )
assume SC: ( x1 in dom h & |.(x1 - x).| < s ) ; :: thesis: |.((h . x1) - (h . x)).| < r
s <= s2 by XXREAL_0:17;
then H1: |.(x1 - x).| < s2 by XXREAL_0:2, SC;
per cases ( x1 in dom f or x1 in dom g ) by FUNCT_4:12, SC;
suppose ZT: x1 in dom f ; :: thesis: |.((h . x1) - (h . x)).| < r
then I1: x1 in dom (h | (dom f)) by RELAT_1:57, SC;
SD: |.(((h | (dom f)) . x1) - ((h | (dom f)) . x)).| < r / 2 by SB, ZT, H1, RELAT_1:57, SC;
s1: (h | (dom f)) . x1 = h . x1 by FUNCT_1:47, I1;
|.((h . x1) - (h . x)).| < r / 2 by SD, s1, FUNCT_1:47, SF;
hence |.((h . x1) - (h . x)).| < r by SS, XXREAL_0:2; :: thesis: verum
end;
suppose P1: x1 in dom g ; :: thesis: |.((h . x1) - (h . x)).| < r
then x1 in dom (h | (dom g)) ;
then P2: h . x1 = (h | (dom g)) . x1 by FUNCT_1:47;
P3: h . x = (h | (dom f)) . x by FUNCT_1:47, SF;
s <= s1 by XXREAL_0:17;
then P6: |.(x1 - x).| < s1 by XXREAL_0:2, SC;
WA: (h | (dom g)) . b = (h | (dom f)) . b by J2, KK, A1, PARTFUN1:def 4;
M3: x + 0 <= b by XXREAL_1:1, J1, AB;
M7: ( b <= x1 & x1 <= c ) by XXREAL_1:1, P1, AB;
m0: x + 0 <= x1 by M7, XXREAL_0:2, M3;
b + 0 <= x1 by XXREAL_1:1, P1, AB;
then M1: |.(x1 - b).| = x1 - b by ABSVALUE:def 1, XREAL_1:19;
M2: |.(b - x).| = b - x by ABSVALUE:def 1, M3, XREAL_1:19;
M8: |.(x1 - x).| = |.(x1 - b).| + |.(b - x).| by M1, M2, m0, ABSVALUE:def 1, XREAL_1:19;
then |.(x1 - b).| <= |.(x1 - x).| by COMPLEX1:46, XREAL_1:31;
then |.(x1 - b).| < s1 by P6, XXREAL_0:2;
then KJ: |.(((h | (dom g)) . x1) - ((h | (dom g)) . b)).| < r / 2 by Sb, P1;
|.(b - x).| <= |.(x1 - x).| by M8, XREAL_1:31, COMPLEX1:46;
then |.(b - x).| < s2 by H1, XXREAL_0:2;
then |.(((h | (dom f)) . b) - ((h | (dom f)) . x)).| < r / 2 by SB, KI;
then WW: |.(((h | (dom g)) . x1) - ((h | (dom g)) . b)).| + |.(((h | (dom f)) . b) - ((h | (dom f)) . x)).| < (r / 2) + (r / 2) by KJ, XREAL_1:8;
|.(((h | (dom g)) . x1) - ((h | (dom f)) . x)).| <= |.(((h | (dom g)) . x1) - ((h | (dom g)) . b)).| + |.(((h | (dom g)) . b) - ((h | (dom f)) . x)).| by COMPLEX1:63;
hence |.((h . x1) - (h . x)).| < r by P2, P3, WA, XXREAL_0:2, WW; :: thesis: verum
end;
end;
end;
hence h is_continuous_in x by FCONT_1:3; :: thesis: verum
end;
suppose J1: x in dom g ; :: thesis: h is_continuous_in x
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) )
proof
let r be Real; :: thesis: ( 0 < r implies ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) ) )
set hf = h | (dom f);
set hg = h | (dom g);
( dom f c= dom h & dom g c= dom h ) by FUNCT_4:10;
then XX: ( dom (h | (dom f)) = dom f & dom (h | (dom g)) = dom g ) by RELAT_1:62;
SF: x in dom (h | (dom g)) by J1;
assume R0: 0 < r ; :: thesis: ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) )
then consider s2 being Real such that
SB: ( 0 < s2 & ( for x1 being Real st x1 in dom (h | (dom g)) & |.(x1 - x).| < s2 holds
|.(((h | (dom g)) . x1) - ((h | (dom g)) . x)).| < r / 2 ) ) by J1, FCONT_1:3, A1;
KK: b in (dom f) /\ (dom g) by AA, TARSKI:def 1;
then KA: ( b in dom f & b in dom g ) by XBOOLE_0:def 4;
KI: ( b in dom (h | (dom f)) & b in dom (h | (dom g)) ) by XX, KK, XBOOLE_0:def 4;
consider s1 being Real such that
Sb: ( 0 < s1 & ( for x1 being Real st x1 in dom (h | (dom f)) & |.(x1 - b).| < s1 holds
|.(((h | (dom f)) . x1) - ((h | (dom f)) . b)).| < r / 2 ) ) by FCONT_1:3, R0, J2, A1, KA;
take s = min (s2,s1); :: thesis: ( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r ) )
thus 0 < s by SB, Sb, XXREAL_0:15; :: thesis: for x1 being Real st x1 in dom h & |.(x1 - x).| < s holds
|.((h . x1) - (h . x)).| < r
SS: r / 2 < r by XREAL_1:216, R0;
let x1 be Real; :: thesis: ( x1 in dom h & |.(x1 - x).| < s implies |.((h . x1) - (h . x)).| < r )
assume SC: ( x1 in dom h & |.(x1 - x).| < s ) ; :: thesis: |.((h . x1) - (h . x)).| < r
s <= s2 by XXREAL_0:17;
then H1: |.(x1 - x).| < s2 by XXREAL_0:2, SC;
per cases ( x1 in dom g or x1 in dom f ) by FUNCT_4:12, SC;
suppose ZT: x1 in dom g ; :: thesis: |.((h . x1) - (h . x)).| < r
then I1: x1 in dom (h | (dom g)) ;
SD: |.(((h | (dom g)) . x1) - ((h | (dom g)) . x)).| < r / 2 by SB, ZT, H1;
s1: (h | (dom g)) . x1 = h . x1 by FUNCT_1:47, I1;
|.((h . x1) - (h . x)).| < r / 2 by SD, s1, FUNCT_1:47, SF;
hence |.((h . x1) - (h . x)).| < r by SS, XXREAL_0:2; :: thesis: verum
end;
suppose P1: x1 in dom f ; :: thesis: |.((h . x1) - (h . x)).| < r
then x1 in dom (h | (dom f)) by RELAT_1:57, SC;
then P2: h . x1 = (h | (dom f)) . x1 by FUNCT_1:47;
P3: h . x = (h | (dom g)) . x by FUNCT_1:47, SF;
s <= s1 by XXREAL_0:17;
then |.(x1 - x).| < s1 by XXREAL_0:2, SC;
then P6: |.(x - x1).| < s1 by COMPLEX1:60;
WA: (h | (dom g)) . b = (h | (dom f)) . b by J2, KK, A1, PARTFUN1:def 4;
M3: x - 0 >= b by XXREAL_1:1, J1, AB;
M7: ( a <= x1 & x1 <= b ) by XXREAL_1:1, P1, AB;
m0: x1 + 0 <= x by M7, XXREAL_0:2, M3;
b - 0 >= x1 by XXREAL_1:1, P1, AB;
then M1: |.(b - x1).| = b - x1 by ABSVALUE:def 1, XREAL_1:11;
M2: |.(x - b).| = x - b by ABSVALUE:def 1, M3, XREAL_1:11;
M8: |.(x - x1).| = |.(b - x1).| + |.(x - b).| by M1, M2, m0, ABSVALUE:def 1, XREAL_1:19;
then |.(b - x1).| <= |.(x - x1).| by COMPLEX1:46, XREAL_1:31;
then |.(b - x1).| < s1 by P6, XXREAL_0:2;
then |.(x1 - b).| < s1 by COMPLEX1:60;
then KJ: |.(((h | (dom f)) . x1) - ((h | (dom f)) . b)).| < r / 2 by Sb, P1, RELAT_1:57, SC;
LK: |.(b - x).| = |.(x - b).| by COMPLEX1:60;
|.(x - b).| <= |.(x - x1).| by M8, XREAL_1:31, COMPLEX1:46;
then |.(b - x).| <= |.(x1 - x).| by COMPLEX1:60, LK;
then |.(b - x).| < s2 by H1, XXREAL_0:2;
then |.(((h | (dom g)) . b) - ((h | (dom g)) . x)).| < r / 2 by SB, KI;
then WW: |.(((h | (dom f)) . x1) - ((h | (dom f)) . b)).| + |.(((h | (dom g)) . b) - ((h | (dom g)) . x)).| < (r / 2) + (r / 2) by KJ, XREAL_1:8;
|.(((h | (dom f)) . x1) - ((h | (dom g)) . x)).| <= |.(((h | (dom f)) . x1) - ((h | (dom f)) . b)).| + |.(((h | (dom f)) . b) - ((h | (dom g)) . x)).| by COMPLEX1:63;
hence |.((h . x1) - (h . x)).| < r by P2, P3, WA, XXREAL_0:2, WW; :: thesis: verum
end;
end;
end;
hence h is_continuous_in x by FCONT_1:3; :: thesis: verum
end;
end;