let a, b, p, q, r, s be Real; :: thesis: for f being Function of REAL,REAL st a > 0 & p > 0 & ( for x being Real holds f . x = max (r,(min (s,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) ) holds
f is Lipschitzian
let f be Function of REAL,REAL; :: thesis: ( a > 0 & p > 0 & ( for x being Real holds f . x = max (r,(min (s,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) ) implies f is Lipschitzian )
assume AP: ( a > 0 & p > 0 ) ; :: thesis: ( ex x being Real st not f . x = max (r,(min (s,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) or f is Lipschitzian )
assume A2: for x being Real holds f . x = max (r,(min (s,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x)))) ; :: thesis: f is Lipschitzian
set f1 = ((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[);
((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[) is Function of REAL,REAL by asymTT10;
then A4: ( dom f = REAL & dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) = REAL ) by FUNCT_2:def 1;
ex r1 being Real st
( 0 < r1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r1 * |.(x1 - x2).| ) )
proof
consider r0 being Real such that
A1: 0 < r0 and
A3: for x1, x2 being Real st x1 in dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) & x2 in dom (((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) holds
|.(((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x1) - ((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x2)).| <= r0 * |.(x1 - x2).| by asymTT51, AP;
take r0 ; :: thesis: ( 0 < r0 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r0 * |.(x1 - x2).| ) )
for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r0 * |.(x1 - x2).|
proof
let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= r0 * |.(x1 - x2).| )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= r0 * |.(x1 - x2).|
then A5: |.(((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x1) - ((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x2)).| <= r0 * |.(x1 - x2).| by A3, A4;
|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x1))))) - (f . x2)).| by A2
.= |.((max (r,(min (s,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x1))))) - (max (r,(min (s,((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x2)))))).| by A2 ;
then |.((f . x1) - (f . x2)).| <= |.(((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x1) - ((((AffineMap (a,b)) | ].-infty,((q - b) / (a + p)).[) +* ((AffineMap ((- p),q)) | [.((q - b) / (a + p)),+infty.[)) . x2)).| by LeMM01;
hence |.((f . x1) - (f . x2)).| <= r0 * |.(x1 - x2).| by A5, XXREAL_0:2; :: thesis: verum
end;
hence ( 0 < r0 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
|.((f . x1) - (f . x2)).| <= r0 * |.(x1 - x2).| ) ) by A1; :: thesis: verum
end;
hence f is Lipschitzian ; :: thesis: verum