let E, F be RealNormSpace; for g being PartFunc of E,F
for A being Subset of E st g is_continuous_on A & dom g = A holds
ex xg being PartFunc of E,[:E,F:] st
( dom xg = A & ( for x being Point of E st x in A holds
xg . x = [x,(g . x)] ) & xg is_continuous_on A )
let g be PartFunc of E,F; for A being Subset of E st g is_continuous_on A & dom g = A holds
ex xg being PartFunc of E,[:E,F:] st
( dom xg = A & ( for x being Point of E st x in A holds
xg . x = [x,(g . x)] ) & xg is_continuous_on A )
let S be Subset of E; ( g is_continuous_on S & dom g = S implies ex xg being PartFunc of E,[:E,F:] st
( dom xg = S & ( for x being Point of E st x in S holds
xg . x = [x,(g . x)] ) & xg is_continuous_on S ) )
assume that
A1:
g is_continuous_on S
and
A2:
dom g = S
; ex xg being PartFunc of E,[:E,F:] st
( dom xg = S & ( for x being Point of E st x in S holds
xg . x = [x,(g . x)] ) & xg is_continuous_on S )
defpred S1[ object , object ] means ex t being Point of E st
( t = $1 & $2 = [t,(g . t)] );
A3:
for x being object st x in S holds
ex y being object st
( y in the carrier of [:E,F:] & S1[x,y] )
proof
let x be
object ;
( x in S implies ex y being object st
( y in the carrier of [:E,F:] & S1[x,y] ) )
assume A4:
x in S
;
ex y being object st
( y in the carrier of [:E,F:] & S1[x,y] )
then reconsider t =
x as
Point of
E ;
take y =
[t,(g . t)];
( y in the carrier of [:E,F:] & S1[x,y] )
g . t in rng g
by A2, A4, FUNCT_1:3;
then reconsider q =
g . t as
Point of
F ;
[t,q] is
Point of
[:E,F:]
;
hence
(
y in the
carrier of
[:E,F:] &
S1[
x,
y] )
;
verum
end;
consider H being Function of S,[:E,F:] such that
A6:
for z being object st z in S holds
S1[z,H . z]
from FUNCT_2:sch 1(A3);
A7:
dom H = S
by FUNCT_2:def 1;
rng H c= the carrier of [:E,F:]
;
then
H in PFuncs ( the carrier of E, the carrier of [:E,F:])
by A7, PARTFUN1:def 3;
then reconsider H = H as PartFunc of E,[:E,F:] by PARTFUN1:46;
take
H
; ( dom H = S & ( for x being Point of E st x in S holds
H . x = [x,(g . x)] ) & H is_continuous_on S )
thus
dom H = S
by FUNCT_2:def 1; ( ( for x being Point of E st x in S holds
H . x = [x,(g . x)] ) & H is_continuous_on S )
thus A11:
for s being Point of E st s in S holds
H . s = [s,(g . s)]
H is_continuous_on S
for x0 being Point of E
for r being Real st x0 in S & 0 < r holds
ex pq being Real st
( 0 < pq & ( for x1 being Point of E st x1 in S & ||.(x1 - x0).|| < pq holds
||.((H /. x1) - (H /. x0)).|| < r ) )
proof
let x0 be
Point of
E;
for r being Real st x0 in S & 0 < r holds
ex pq being Real st
( 0 < pq & ( for x1 being Point of E st x1 in S & ||.(x1 - x0).|| < pq holds
||.((H /. x1) - (H /. x0)).|| < r ) )let r be
Real;
( x0 in S & 0 < r implies ex pq being Real st
( 0 < pq & ( for x1 being Point of E st x1 in S & ||.(x1 - x0).|| < pq holds
||.((H /. x1) - (H /. x0)).|| < r ) ) )
assume A12:
(
x0 in S &
0 < r )
;
ex pq being Real st
( 0 < pq & ( for x1 being Point of E st x1 in S & ||.(x1 - x0).|| < pq holds
||.((H /. x1) - (H /. x0)).|| < r ) )
then A14:
g . x0 in rng g
by A2, FUNCT_1:3;
[x0,(g . x0)] is
set
by TARSKI:1;
then reconsider z0 =
[x0,(g . x0)] as
Point of
[:E,F:] by A14, PRVECT_3:18;
A15:
(
0 < r / 2 &
r / 2
< r )
by A12, XREAL_1:215, XREAL_1:216;
consider q being
Real such that A16:
(
0 < q & ( for
x1 being
Point of
E st
x1 in S &
||.(x1 - x0).|| < q holds
||.((g /. x1) - (g /. x0)).|| < r / 2 ) )
by A1, A12, NFCONT_1:19, XREAL_1:215;
set pq =
min (
q,
(r / 2));
A17:
(
0 < min (
q,
(r / 2)) &
min (
q,
(r / 2))
<= q &
min (
q,
(r / 2))
<= r / 2 )
by A15, A16, XXREAL_0:15, XXREAL_0:17;
take
min (
q,
(r / 2))
;
( 0 < min (q,(r / 2)) & ( for x1 being Point of E st x1 in S & ||.(x1 - x0).|| < min (q,(r / 2)) holds
||.((H /. x1) - (H /. x0)).|| < r ) )
thus
0 < min (
q,
(r / 2))
by A15, A16, XXREAL_0:15;
for x1 being Point of E st x1 in S & ||.(x1 - x0).|| < min (q,(r / 2)) holds
||.((H /. x1) - (H /. x0)).|| < r
thus
for
x1 being
Point of
E st
x1 in S &
||.(x1 - x0).|| < min (
q,
(r / 2)) holds
||.((H /. x1) - (H /. x0)).|| < r
verumproof
let x1 be
Point of
E;
( x1 in S & ||.(x1 - x0).|| < min (q,(r / 2)) implies ||.((H /. x1) - (H /. x0)).|| < r )
assume A18:
(
x1 in S &
||.(x1 - x0).|| < min (
q,
(r / 2)) )
;
||.((H /. x1) - (H /. x0)).|| < r
then
||.(x1 - x0).|| < q
by A17, XXREAL_0:2;
then A21:
||.((g /. x1) - (g /. x0)).|| < r / 2
by A16, A18;
A23:
g . x1 in rng g
by A2, A18, FUNCT_1:3;
[x1,(g . x1)] is
set
by TARSKI:1;
then reconsider z1 =
[x1,(g . x1)] as
Point of
[:E,F:] by A23, PRVECT_3:18;
A24:
z1 = [x1,(g /. x1)]
by A2, A18, PARTFUN1:def 6;
z0 = [x0,(g /. x0)]
by A2, A12, PARTFUN1:def 6;
then
- z0 = [(- x0),(- (g /. x0))]
by PRVECT_3:18;
then
z1 - z0 = [(x1 - x0),((g /. x1) - (g /. x0))]
by A24, PRVECT_3:18;
then A26:
||.(z1 - z0).|| = sqrt ((||.(x1 - x0).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2))
by NDIFF_8:1;
||.(x1 - x0).|| < r / 2
by A17, A18, XXREAL_0:2;
then A27:
||.(x1 - x0).|| ^2 < (r / 2) ^2
by SQUARE_1:16;
||.((g /. x1) - (g /. x0)).|| ^2 <= (r / 2) ^2
by A21, SQUARE_1:15;
then A29:
(||.(x1 - x0).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2) <= ((r ^2) / 4) + ((r ^2) / 4)
by A27, XREAL_1:7;
(r ^2) / 2
< r ^2
by A12, XREAL_1:129, XREAL_1:216;
then
(||.(x1 - x0).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2) < r ^2
by A29, XXREAL_0:2;
then A31:
sqrt ((||.(x1 - x0).|| ^2) + (||.((g /. x1) - (g /. x0)).|| ^2)) < sqrt (r ^2)
by SQUARE_1:27;
A32:
H /. x1 =
H . x1
by A7, A18, PARTFUN1:def 6
.=
z1
by A11, A18
;
H /. x0 =
H . x0
by A7, A12, PARTFUN1:def 6
.=
z0
by A11, A12
;
hence
||.((H /. x1) - (H /. x0)).|| < r
by A12, A26, A31, A32, SQUARE_1:22;
verum
end;
end;
hence
H is_continuous_on S
by A7, NFCONT_1:19; verum