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 number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (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 number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) )
let f be PartFunc of REAL, the carrier of S; :: thesis: ( f | X is Lipschitzian iff ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) )
thus ( f | X is Lipschitzian implies ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) ) :: thesis: ( ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) ) implies f | X is Lipschitzian )

proof

given r being real number such that A1: 0 < r and
A2: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.(((f | X) /. x1) - ((f | X) /. x2)).|| <= r * (abs (x1 - x2)) ; :: according to NFCONT_3:def 3 :: thesis: ex r being real number st
( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) )
take r ; :: thesis: ( 0 < r & ( for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) ) )
thus 0 < r by A1; :: thesis: for x1, x2 being real number st x1 in dom (f | X) & x2 in dom (f | X) holds
||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2))
let x1, x2 be real number ; :: thesis: ( x1 in dom (f | X) & x2 in dom (f | X) implies ||.((f /. x1) - (f /. x2)).|| <= r * (abs (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 * (abs (x1 - x2))
then ( (f | X) /. x1 = f /. x1 & (f | X) /. x2 = f /. x2 ) by PARTFUN2:15, A3;
hence ||.((f /. x1) - (f /. x2)).|| <= r * (abs (x1 - x2)) by A2, A4; :: thesis: verum

end;

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