let X be set ; :: thesis: for S being RealNormSpace
for f being PartFunc of REAL, the carrier of S holds
( f | X is Lipschitzian iff ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) ) )
let S be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of S holds
( f | X is Lipschitzian iff ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) ) )
let f be PartFunc of REAL, the carrier of S; :: thesis: ( f | X is Lipschitzian iff ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) ) )
thus ( f | X is Lipschitzian implies ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) ) ) :: thesis: ( ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) ) implies f | X is Lipschitzian )

proof

given r being Real such that A1: 0 < r and
A2: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * |.(x1 - x2).| ; :: according to NFCONT_3:def 3 :: thesis: ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) )
take r ; :: thesis: ( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ) )
thus 0 < r by A1; :: thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).|
let x1, x2 be Real; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| )
A3: ( x1 in REAL & x2 in REAL ) by XREAL_0:def 1;
assume A4: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: ||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).|
then ( (f | X) /. x1 = f /. x1 & (f | X) /. x2 = f /. x2 ) by A3, PARTFUN2:15;
hence ||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| by A2, A4; :: thesis: verum

end;

given r being Real such that A5: 0 < r and
A6: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * |.(x1 - x2).| ; :: thesis: f | X is Lipschitzian
take r ; :: according to NFCONT_3:def 3 :: thesis: ( 0 < r & ( for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * |.(x1 - x2).| ) )
thus 0 < r by A5; :: thesis: for x1, x2 being Real st x1 in dom (f | X) & x2 in dom (f | X) holds
||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * |.(x1 - x2).|
let x1, x2 be Real; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * |.(x1 - x2).| )
A7: ( x1 in REAL & x2 in REAL ) by XREAL_0:def 1;
assume A8: ( x1 in dom (f | X) & x2 in dom (f | X) ) ; :: thesis: ||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * |.(x1 - x2).|
then ( (f | X) /. x1 = f /. x1 & (f | X) /. x2 = f /. x2 ) by A7, PARTFUN2:15;
hence ||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * |.(x1 - x2).| by A6, A8; :: thesis: verum