let f be Function of REAL,REAL; :: thesis: for a, b, r, s being Real st ( for x being Real holds f . x = max (r,(min (s,((AffineMap (a,b)) . x)))) ) holds

f is Lipschitzian

let a, b, r, s be Real; :: thesis: ( ( for x being Real holds f . x = max (r,(min (s,((AffineMap (a,b)) . x)))) ) implies f is Lipschitzian )

assume A1: for x being Real holds f . x = max (r,(min (s,((AffineMap (a,b)) . 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 a, b, r, s be Real; :: thesis: ( ( for x being Real holds f . x = max (r,(min (s,((AffineMap (a,b)) . x)))) ) implies f is Lipschitzian )

assume A1: for x being Real holds f . x = max (r,(min (s,((AffineMap (a,b)) . 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
end;

hence
f is Lipschitzian
; :: thesis: verumper cases
( a = 0 or a <> 0 )
;

end;

suppose C0:
a = 0
; :: thesis: 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).| ) )

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

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

assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (f . x2)).| by A1

.= |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by A1

.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by FCONT_1:def 4

.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((a * x2) + b)))))).| by FCONT_1:def 4

.= 0 by COMPLEX1:44, C0 ;

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

end;assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (f . x2)).| by A1

.= |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by A1

.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by FCONT_1:def 4

.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((a * x2) + b)))))).| by FCONT_1:def 4

.= 0 by COMPLEX1:44, C0 ;

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

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

suppose A2:
a <> 0
; :: thesis: 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).| ) )

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

take
|.a.|
; :: thesis: ( 0 < |.a.| & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).| ) )

for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).|

|.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).| ) ) by A2, COMPLEX1:47; :: thesis: verum

end;|.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).| ) )

for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).|

proof

hence
( 0 < |.a.| & ( 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)).| <= |.a.| * |.(x1 - x2).| )

assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).|

|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (f . x2)).| by A1

.= |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by A1

.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by FCONT_1:def 4

.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((a * x2) + b)))))).| by FCONT_1:def 4 ;

then |.((f . x1) - (f . x2)).| <= |.(((a * x1) + b) - ((a * x2) + b)).| by LeMM01;

then |.((f . x1) - (f . x2)).| <= |.(a * (x1 - x2)).| ;

hence |.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).| by COMPLEX1:65; :: thesis: verum

end;assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).|

|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (f . x2)).| by A1

.= |.((max (r,(min (s,((AffineMap (a,b)) . x1))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by A1

.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((AffineMap (a,b)) . x2)))))).| by FCONT_1:def 4

.= |.((max (r,(min (s,((a * x1) + b))))) - (max (r,(min (s,((a * x2) + b)))))).| by FCONT_1:def 4 ;

then |.((f . x1) - (f . x2)).| <= |.(((a * x1) + b) - ((a * x2) + b)).| by LeMM01;

then |.((f . x1) - (f . x2)).| <= |.(a * (x1 - x2)).| ;

hence |.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).| by COMPLEX1:65; :: thesis: verum

|.((f . x1) - (f . x2)).| <= |.a.| * |.(x1 - x2).| ) ) by A2, COMPLEX1:47; :: thesis: verum