let X, Y be RealNormSpace; :: thesis: for T being non empty PartFunc of X,Y
for T0 being LinearOperator of X,Y st T0 is Lipschitzian & dom T is closed & T = T0 holds
T is closed
let T be non empty PartFunc of X,Y; :: thesis: for T0 being LinearOperator of X,Y st T0 is Lipschitzian & dom T is closed & T = T0 holds
T is closed
let T0 be LinearOperator of X,Y; :: thesis: ( T0 is Lipschitzian & dom T is closed & T = T0 implies T is closed )
assume A1: ( T0 is Lipschitzian & dom T is closed & T = T0 ) ; :: thesis: T is closed
then A2: T is_continuous_in 0. X by Th5, Th6;
for seq being sequence of X st rng seq c= dom T & seq is convergent & T /* seq is convergent holds
( lim seq in dom T & lim (T /* seq) = T . (lim seq) )
proof
let seq be sequence of X; :: thesis: ( rng seq c= dom T & seq is convergent & T /* seq is convergent implies ( lim seq in dom T & lim (T /* seq) = T . (lim seq) ) )
assume A3: ( rng seq c= dom T & seq is convergent & T /* seq is convergent ) ; :: thesis: ( lim seq in dom T & lim (T /* seq) = T . (lim seq) )
A4: T is_continuous_in lim seq by A1, A2, Th4;
T /. (lim seq) = T . (lim seq) by A1, A3, NFCONT_1:def 3, PARTFUN1:def 6;
hence ( lim seq in dom T & lim (T /* seq) = T . (lim seq) ) by A3, A4, NFCONT_1:def 5; :: thesis: verum
end;
hence T is closed by Th12; :: thesis: verum