let X, Y be RealNormSpace; :: thesis: for A being Subset of X
for B being Subset of Y
for L being Lipschitzian LinearOperator of X,Y st L is isomorphism & B = L .: A holds
( A is dense iff B is dense )
let A be Subset of X; :: thesis: for B being Subset of Y
for L being Lipschitzian LinearOperator of X,Y st L is isomorphism & B = L .: A holds
( A is dense iff B is dense )
let B be Subset of Y; :: thesis: for L being Lipschitzian LinearOperator of X,Y st L is isomorphism & B = L .: A holds
( A is dense iff B is dense )
let L be Lipschitzian LinearOperator of X,Y; :: thesis: ( L is isomorphism & B = L .: A implies ( A is dense iff B is dense ) )
assume A1: ( L is isomorphism & B = L .: A ) ; :: thesis: ( A is dense iff B is dense )
then consider K being Lipschitzian LinearOperator of Y,X such that
A2: ( K = L " & K is isomorphism ) by NORMSP_3:37;
thus ( A is dense implies B is dense ) by A1, Th29; :: thesis: ( B is dense implies A is dense )
assume A3: B is dense ; :: thesis: A is dense
A c= the carrier of X ;
then A c= dom L by FUNCT_2:def 1;
then K .: B = A by A1, A2, FUNCT_1:107;
hence A is dense by A2, A3, Th29; :: thesis: verum