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).| ) )

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

hence
f is Lipschitzian
; :: thesis: verum
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).|

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) ; :: thesis: verum

end;|.((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

hence
( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
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;|.((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

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) ; :: thesis: verum