let X, Y be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( L is isomorphism & W = L .: V & W is closed implies V is closed )

assume A1: ( L is isomorphism & W = L .: V ) ; :: thesis: ( 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 ; :: thesis: V is closed

for s1 being sequence of X st rng s1 c= V & s1 is convergent holds

lim s1 in V

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; :: thesis: 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; :: thesis: 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; :: thesis: ( L is isomorphism & W = L .: V & W is closed implies V is closed )

assume A1: ( L is isomorphism & W = L .: V ) ; :: thesis: ( 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 ; :: thesis: V is closed

for s1 being sequence of X st rng s1 c= V & s1 is convergent holds

lim s1 in V

proof

hence
V is closed
; :: thesis: verum
let s1 be sequence of X; :: thesis: ( rng s1 c= V & s1 is convergent implies lim s1 in V )

assume A5: ( rng s1 c= V & s1 is convergent ) ; :: thesis: 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; :: thesis: verum

end;assume A5: ( rng s1 c= V & s1 is convergent ) ; :: thesis: 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; :: thesis: verum