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

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

for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds

seq is convergent

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

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

assume A5:
Y is complete
; :: thesis: X is complete assume A2:
X is complete
; :: thesis: Y is complete

for seq being sequence of Y st seq is Cauchy_sequence_by_Norm holds

seq is convergent

end;for seq being sequence of Y st seq is Cauchy_sequence_by_Norm holds

seq is convergent

proof

hence
Y is complete
by LOPBAN_1:def 15; :: thesis: verum
let seq be sequence of Y; :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )

assume A3: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent

consider K being Lipschitzian LinearOperator of Y,X such that

A4: ( K = L " & K is isomorphism ) by A1, NISOM01;

K * seq is Cauchy_sequence_by_Norm by A3, A4, NISOM05;

then K * seq is convergent by A2, LOPBAN_1:def 15;

hence seq is convergent by A4, NISOM03; :: thesis: verum

end;assume A3: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent

consider K being Lipschitzian LinearOperator of Y,X such that

A4: ( K = L " & K is isomorphism ) by A1, NISOM01;

K * seq is Cauchy_sequence_by_Norm by A3, A4, NISOM05;

then K * seq is convergent by A2, LOPBAN_1:def 15;

hence seq is convergent by A4, NISOM03; :: thesis: verum

for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds

seq is convergent

proof

hence
X is complete
by LOPBAN_1:def 15; :: thesis: verum
let seq be sequence of X; :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )

assume seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent

then L * seq is Cauchy_sequence_by_Norm by A1, NISOM05;

then L * seq is convergent by A5, LOPBAN_1:def 15;

hence seq is convergent by A1, NISOM03; :: thesis: verum

end;assume seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent

then L * seq is Cauchy_sequence_by_Norm by A1, NISOM05;

then L * seq is convergent by A5, LOPBAN_1:def 15;

hence seq is convergent by A1, NISOM03; :: thesis: verum