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 & A is dense holds
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 & A is dense holds
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 & A is dense holds
B is dense
let L be Lipschitzian LinearOperator of X,Y; :: thesis: ( L is isomorphism & B = L .: A & A is dense implies B is dense )
assume A1: ( L is isomorphism & B = L .: A & A is dense ) ; :: thesis: B is dense
for y being Point of Y ex seq being sequence of Y st
( rng seq c= B & seq is convergent & lim seq = y )
proof
let y be Point of Y; :: thesis: ex seq being sequence of Y st
( rng seq c= B & seq is convergent & lim seq = y )
y in the carrier of Y ;
then y in rng L by A1, FUNCT_2:def 3;
then consider x being Point of X such that
A2: y = L . x by FUNCT_2:113;
consider seq being sequence of X such that
A3: ( rng seq c= A & seq is convergent & lim seq = x ) by A1, NORMSP_3:14;
reconsider seq1 = L * seq as sequence of Y ;
L .: (rng seq) c= L .: A by A3, RELAT_1:123;
then A4: rng seq1 c= B by A1, RELAT_1:127;
( seq1 is convergent & lim seq1 = L . (lim seq) ) by A3, NORMSP_3:38;
hence ex seq being sequence of Y st
( rng seq c= B & seq is convergent & lim seq = y ) by A2, A3, A4; :: thesis: verum
end;
hence B is dense by NORMSP_3:14; :: thesis: verum