let r, s be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = max (r,(min (s,x))) ) holds
f is Lipschitzian
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = max (r,(min (s,x))) ) implies f is Lipschitzian )
assume A1: for x being Real holds f . x = max (r,(min (s,x))) ; :: thesis: f is Lipschitzian
ex r being Real st
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )
proof
take 1 ; :: thesis: ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) )
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|
proof
let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| )
|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,x1)))) - (f . x2)).| by A1
.= |.((max (r,(min (s,x1)))) - (max (r,(min (s,x2))))).| by A1 ;
hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) by LeMM01; :: thesis: verum
end;
hence ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) ; :: thesis: verum
end;
hence f is Lipschitzian ; :: thesis: verum