let S, T be RealNormSpace; :: thesis: for I being LinearOperator of S,T
for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like holds
( Z is closed iff I .: Z is closed )
let I be LinearOperator of S,T; :: thesis: for Z being Subset of S st I is one-to-one & I is onto & I is isometric-like holds
( Z is closed iff I .: Z is closed )
let Z be Subset of S; :: thesis: ( I is one-to-one & I is onto & I is isometric-like implies ( Z is closed iff I .: Z is closed ) )
assume that
A1: ( I is one-to-one & I is onto ) and
A2: I is isometric-like ; :: thesis: ( Z is closed iff I .: Z is closed )
A3: dom I = the carrier of S by FUNCT_2:def 1;
consider J being LinearOperator of T,S such that
A4: ( J = I " & J is one-to-one & J is onto & J is isometric-like ) by A1, A2, Th29;
thus ( Z is closed iff I .: Z is closed ) :: thesis: verum
proof
thus ( Z is closed implies I .: Z is closed ) by A1, A2, Lm4; :: thesis: ( I .: Z is closed implies Z is closed )
assume A5: I .: Z is closed ; :: thesis: Z is closed
J .: (I .: Z) = I " (I .: Z) by A1, A4, FUNCT_1:85
.= Z by A1, A3, FUNCT_1:94 ;
hence Z is closed by A4, A5, Lm4; :: thesis: verum
end;