let X, Y be RealNormSpace; :: thesis: ( ex L being Lipschitzian LinearOperator of X,Y st L is isomorphism implies ( X is separable iff Y is separable ) )

given L being Lipschitzian LinearOperator of X,Y such that A1: L is isomorphism ; :: thesis: ( X is separable iff Y is separable )

consider K being Lipschitzian LinearOperator of Y,X such that

A2: ( K = L " & K is isomorphism ) by A1, NORMSP_3:37;

then consider seq being sequence of Y such that

A4: rng seq is dense by NORMSP_3:21;

reconsider seq1 = K * seq as sequence of X ;

rng seq1 = K .: (rng seq) by RELAT_1:127;

then rng seq1 is dense by A2, A4, Th30;

hence X is separable by NORMSP_3:21; :: thesis: verum

given L being Lipschitzian LinearOperator of X,Y such that A1: L is isomorphism ; :: thesis: ( X is separable iff Y is separable )

consider K being Lipschitzian LinearOperator of Y,X such that

A2: ( K = L " & K is isomorphism ) by A1, NORMSP_3:37;

hereby :: thesis: ( Y is separable implies X is separable )

assume
Y is separable
; :: thesis: X is separable assume
X is separable
; :: thesis: Y is separable

then consider seq being sequence of X such that

A3: rng seq is dense by NORMSP_3:21;

reconsider seq1 = L * seq as sequence of Y ;

rng seq1 = L .: (rng seq) by RELAT_1:127;

then rng seq1 is dense by A1, A3, Th30;

hence Y is separable by NORMSP_3:21; :: thesis: verum

end;then consider seq being sequence of X such that

A3: rng seq is dense by NORMSP_3:21;

reconsider seq1 = L * seq as sequence of Y ;

rng seq1 = L .: (rng seq) by RELAT_1:127;

then rng seq1 is dense by A1, A3, Th30;

hence Y is separable by NORMSP_3:21; :: thesis: verum

then consider seq being sequence of Y such that

A4: rng seq is dense by NORMSP_3:21;

reconsider seq1 = K * seq as sequence of X ;

rng seq1 = K .: (rng seq) by RELAT_1:127;

then rng seq1 is dense by A2, A4, Th30;

hence X is separable by NORMSP_3:21; :: thesis: verum