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