let X, Y be RealNormSpace; for L being Lipschitzian LinearOperator of X,Y
for V being Subset of X
for W being Subset of Y st L is isomorphism & W = L .: V & W is closed holds
V is closed
let L be Lipschitzian LinearOperator of X,Y; for V being Subset of X
for W being Subset of Y st L is isomorphism & W = L .: V & W is closed holds
V is closed
let V be Subset of X; for W being Subset of Y st L is isomorphism & W = L .: V & W is closed holds
V is closed
let W be Subset of Y; ( L is isomorphism & W = L .: V & W is closed implies V is closed )
assume A1:
( L is isomorphism & W = L .: V )
; ( not W is closed or V is closed )
then consider K being Lipschitzian LinearOperator of Y,X such that
A2:
( K = L " & K is isomorphism )
by NISOM01;
A3:
dom L = the carrier of X
by FUNCT_2:def 1;
assume A4:
W is closed
; V is closed
for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V
proof
let s1 be
sequence of
X;
( rng s1 c= V & s1 is convergent implies lim s1 in V )
assume A5:
(
rng s1 c= V &
s1 is
convergent )
;
lim s1 in V
set s2 =
L * s1;
A6:
(
L * s1 is
convergent &
lim (L * s1) = L . (lim s1) )
by A5, NISOM02;
L .: (rng s1) c= L .: V
by A5, RELAT_1:123;
then
rng (L * s1) c= W
by A1, RELAT_1:127;
then
L . (lim s1) in L .: V
by A1, A4, A6;
then
(L ") . (L . (lim s1)) in K .: (L .: V)
by A2, FUNCT_2:35;
then A8:
lim s1 in K .: (L .: V)
by A1, A3, FUNCT_1:34;
A9:
K .: (L .: V) = L " (L .: V)
by A1, A2, FUNCT_1:85;
L " (L .: V) c= V
by A1, FUNCT_1:82;
hence
lim s1 in V
by A8, A9;
verum
end;
hence
V is closed
; verum