let X, Y, Z be RealNormSpace; for V being Subset of Y
for g being PartFunc of Y,Z
for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds
( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
let V be Subset of Y; for g being PartFunc of Y,Z
for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds
( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
let g be PartFunc of Y,Z; for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds
( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
let I be LinearOperator of X,Y; ( I is one-to-one & I is onto & I is isometric & g is_differentiable_on V implies ( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V ) )
assume that
A1:
( I is one-to-one & I is onto & I is isometric )
and
A2:
g is_differentiable_on V
; ( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
consider J being LinearOperator of Y,X such that
A3:
( J = I " & J is one-to-one & J is onto & J is isometric )
by A1, NDIFF_7:9;
set f = g * I;
set U = I " V;
A4:
dom J = the carrier of Y
by FUNCT_2:def 1;
A5:
g * I is_differentiable_on I " V
by A1, A2, NDIFF_7:29;
A6:
dom ((g * I) `| (I " V)) = I " V
by A5, NDIFF_1:def 9;
A7:
dom (g `| V) = V
by A2, NDIFF_1:def 9;
set F = (g * I) `| (I " V);
set G = g `| V;
A8:
( g `| V is_continuous_on V implies (g * I) `| (I " V) is_continuous_on I " V )
proof
assume A10:
g `| V is_continuous_on V
;
(g * I) `| (I " V) is_continuous_on I " V
for
x0 being
Point of
X for
e being
Real st
x0 in I " V &
0 < e holds
ex
d being
Real st
(
0 < d & ( for
x1 being
Point of
X st
x1 in I " V &
||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )
proof
let x0 be
Point of
X;
for e being Real st x0 in I " V & 0 < e holds
ex d being Real st
( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )let e be
Real;
( x0 in I " V & 0 < e implies ex d being Real st
( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) ) )
assume A11:
(
x0 in I " V &
0 < e )
;
ex d being Real st
( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )
consider y0 being
Point of
Y such that A12:
x0 = J . y0
by A3, FUNCT_2:113;
A13:
I . x0 = y0
by A1, A3, A12, FUNCT_1:35;
then A14:
y0 in V
by A11, FUNCT_2:38;
then consider d being
Real such that A15:
(
0 < d & ( for
y1 being
Point of
Y st
y1 in V &
||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )
by A10, A11, NFCONT_1:19;
take
d
;
( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )
thus
0 < d
by A15;
for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e
thus
for
x1 being
Point of
X st
x1 in I " V &
||.(x1 - x0).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e
verumproof
let x1 be
Point of
X;
( x1 in I " V & ||.(x1 - x0).|| < d implies ||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e )
assume A16:
(
x1 in I " V &
||.(x1 - x0).|| < d )
;
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e
consider y1 being
Point of
Y such that A17:
x1 = J . y1
by A3, FUNCT_2:113;
A18:
I . x1 = y1
by A1, A3, A17, FUNCT_1:35;
then A19:
y1 in V
by A16, FUNCT_2:38;
||.(y1 - y0).|| = ||.(x1 - x0).||
by A1, A13, A18;
then A20:
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e
by A15, A16, A19;
A21:
(g `| V) /. y1 =
(g `| V) . y1
by A7, A19, PARTFUN1:def 6
.=
(((g * I) `| (I " V)) /. x1) * J
by A1, A2, A3, A17, A19, Th9
;
A22:
(g `| V) /. y0 =
(g `| V) . y0
by A7, A14, PARTFUN1:def 6
.=
(((g * I) `| (I " V)) /. x0) * J
by A1, A2, A3, A12, A14, Th9
;
reconsider dF =
(((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0) as
Lipschitzian LinearOperator of
X,
Z by LOPBAN_1:def 9;
reconsider dG =
((g `| V) /. y1) - ((g `| V) /. y0) as
Lipschitzian LinearOperator of
Y,
Z by LOPBAN_1:def 9;
then
dF * J = dG
;
hence
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e
by A3, A20, NDIFF_7:22;
verum
end;
end;
hence
(g * I) `| (I " V) is_continuous_on I " V
by A6, NFCONT_1:19;
verum
end;
( (g * I) `| (I " V) is_continuous_on I " V implies g `| V is_continuous_on V )
proof
assume A25:
(g * I) `| (I " V) is_continuous_on I " V
;
g `| V is_continuous_on V
for
y0 being
Point of
Y for
e being
Real st
y0 in V &
0 < e holds
ex
d being
Real st
(
0 < d & ( for
y1 being
Point of
Y st
y1 in V &
||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )
proof
let y0 be
Point of
Y;
for e being Real st y0 in V & 0 < e holds
ex d being Real st
( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )let e be
Real;
( y0 in V & 0 < e implies ex d being Real st
( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) ) )
assume A26:
(
y0 in V &
0 < e )
;
ex d being Real st
( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )
set x0 =
J . y0;
I . (J . y0) = y0
by A1, A3, FUNCT_1:35;
then
J . y0 in I " V
by A26, FUNCT_2:38;
then consider d being
Real such that A27:
(
0 < d & ( for
x1 being
Point of
X st
x1 in I " V &
||.(x1 - (J . y0)).|| < d holds
||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. (J . y0))).|| < e ) )
by A25, A26, NFCONT_1:19;
take
d
;
( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )
thus
0 < d
by A27;
for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e
let y1 be
Point of
Y;
( y1 in V & ||.(y1 - y0).|| < d implies ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e )
assume A28:
(
y1 in V &
||.(y1 - y0).|| < d )
;
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e
set x1 =
J . y1;
I . (J . y1) = y1
by A1, A3, FUNCT_1:35;
then A29:
J . y1 in I " V
by A28, FUNCT_2:38;
||.((J . y1) - (J . y0)).|| = ||.(y1 - y0).||
by A3;
then A30:
||.((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))).|| < e
by A27, A28, A29;
A31:
(g `| V) /. y1 =
(g `| V) . y1
by A7, A28, PARTFUN1:def 6
.=
(((g * I) `| (I " V)) /. (J . y1)) * J
by A1, A2, A3, A28, Th9
;
A32:
(g `| V) /. y0 =
(g `| V) . y0
by A7, A26, PARTFUN1:def 6
.=
(((g * I) `| (I " V)) /. (J . y0)) * J
by A1, A2, A3, A26, Th9
;
reconsider dF =
(((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0)) as
Lipschitzian LinearOperator of
X,
Z by LOPBAN_1:def 9;
reconsider dG =
((g `| V) /. y1) - ((g `| V) /. y0) as
Lipschitzian LinearOperator of
Y,
Z by LOPBAN_1:def 9;
then
dF * J = dG
;
hence
||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e
by A3, A30, NDIFF_7:22;
verum
end;
hence
g `| V is_continuous_on V
by A7, NFCONT_1:19;
verum
end;
hence
( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
by A8; verum