let X be set ; for S, T being RealNormSpace
for f being PartFunc of S,T st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
let S, T be RealNormSpace; for f being PartFunc of S,T st f is_Lipschitzian_on X holds
f is_uniformly_continuous_on X
let f be PartFunc of S,T; ( f is_Lipschitzian_on X implies f is_uniformly_continuous_on X )
assume A1:
f is_Lipschitzian_on X
; f is_uniformly_continuous_on X
hence
X c= dom f
by NFCONT_1:def 9; NFCONT_2:def 1 for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < r ) )
consider r being Real such that
A2:
0 < r
and
A3:
for x1, x2 being Point of S st x1 in X & x2 in X holds
||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).||
by A1, NFCONT_1:def 9;
let p be Real; ( 0 < p implies ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) ) )
assume A4:
0 < p
; ex s being Real st
( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) )
take s = p / r; ( 0 < s & ( for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p ) )
thus
0 < s
by A2, A4, XREAL_1:139; for x1, x2 being Point of S st x1 in X & x2 in X & ||.(x1 - x2).|| < s holds
||.((f /. x1) - (f /. x2)).|| < p
let x1, x2 be Point of S; ( x1 in X & x2 in X & ||.(x1 - x2).|| < s implies ||.((f /. x1) - (f /. x2)).|| < p )
assume
( x1 in X & x2 in X & ||.(x1 - x2).|| < s )
; ||.((f /. x1) - (f /. x2)).|| < p
then
( r * ||.(x1 - x2).|| < s * r & ||.((f /. x1) - (f /. x2)).|| <= r * ||.(x1 - x2).|| )
by A2, A3, XREAL_1:68;
then
||.((f /. x1) - (f /. x2)).|| < (p / r) * r
by XXREAL_0:2;
hence
||.((f /. x1) - (f /. x2)).|| < p
by A2, XCMPLX_1:87; verum