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 holds

( V is closed iff W 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 holds

( V is closed iff W is closed )

let V be Subset of X; :: thesis: for W being Subset of Y st L is isomorphism & W = L .: V holds

( V is closed iff W is closed )

let W be Subset of Y; :: thesis: ( L is isomorphism & W = L .: V implies ( V is closed iff W is closed ) )

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

K .: (L .: V) = L " (L .: V) by A1, A2, FUNCT_1:85;

then V = K .: W by A1, A3, FUNCT_1:76, FUNCT_1:82;

hence ( V is closed implies W is closed ) by A2, NISOM06; :: thesis: ( W is closed implies V is closed )

thus ( W is closed implies V is closed ) by A1, NISOM06; :: thesis: verum

for V being Subset of X

for W being Subset of Y st L is isomorphism & W = L .: V holds

( V is closed iff W 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 holds

( V is closed iff W is closed )

let V be Subset of X; :: thesis: for W being Subset of Y st L is isomorphism & W = L .: V holds

( V is closed iff W is closed )

let W be Subset of Y; :: thesis: ( L is isomorphism & W = L .: V implies ( V is closed iff W is closed ) )

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

K .: (L .: V) = L " (L .: V) by A1, A2, FUNCT_1:85;

then V = K .: W by A1, A3, FUNCT_1:76, FUNCT_1:82;

hence ( V is closed implies W is closed ) by A2, NISOM06; :: thesis: ( W is closed implies V is closed )

thus ( W is closed implies V is closed ) by A1, NISOM06; :: thesis: verum