let n be Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) holds

( f is Lipschitzian iff 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).| ) ) )

let f be PartFunc of REAL,(REAL n); :: thesis: ( f is Lipschitzian iff 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 /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) ; :: thesis: f is Lipschitzian

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

hence f is Lipschitzian ; :: thesis: verum

( f is Lipschitzian iff 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).| ) ) )

let f be PartFunc of REAL,(REAL n); :: thesis: ( f is Lipschitzian iff 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).| ) ) )

hereby :: 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).| ) ) implies f is Lipschitzian )

given r being Real such that A4:
( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds ( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) implies f is Lipschitzian )

assume
f is Lipschitzian
; :: 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).| ) )

then consider g being PartFunc of REAL,(REAL-NS n) such that

A1: ( g = f & g is Lipschitzian ) ;

consider r being Real such that

A2: ( 0 < r & ( for x1, x2 being Real st x1 in dom g & x2 in dom g holds

||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).| ) ) by A1;

take r = r; :: thesis: ( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

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

thus 0 < r by A2; :: thesis: for x1, x2 being Real st x1 in dom f & x2 in dom f holds

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

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

|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| :: thesis: verum

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

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

then consider g being PartFunc of REAL,(REAL-NS n) such that

A1: ( g = f & g is Lipschitzian ) ;

consider r being Real such that

A2: ( 0 < r & ( for x1, x2 being Real st x1 in dom g & x2 in dom g holds

||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).| ) ) by A1;

take r = r; :: thesis: ( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

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

thus 0 < r by A2; :: thesis: for x1, x2 being Real st x1 in dom f & x2 in dom f holds

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

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

|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| :: thesis: verum

proof

let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| )

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

then A3: ||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).| by A1, A2;

( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by A1, REAL_NS1:def 4;

hence |.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| by A3, REAL_NS1:1, REAL_NS1:5; :: thesis: verum

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

then A3: ||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).| by A1, A2;

( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by A1, REAL_NS1:def 4;

hence |.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| by A3, REAL_NS1:1, REAL_NS1:5; :: thesis: verum

|.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| ) ) ; :: thesis: f is Lipschitzian

reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;

now :: thesis: for x1, x2 being Real st x1 in dom g & x2 in dom g holds

||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).|

then
g is Lipschitzian
by A4;||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).|

let x1, x2 be Real; :: thesis: ( x1 in dom g & x2 in dom g implies ||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).| )

assume ( x1 in dom g & x2 in dom g ) ; :: thesis: ||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).|

then A5: |.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| by A4;

( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by REAL_NS1:def 4;

hence ||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).| by A5, REAL_NS1:1, REAL_NS1:5; :: thesis: verum

end;assume ( x1 in dom g & x2 in dom g ) ; :: thesis: ||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).|

then A5: |.((f /. x1) - (f /. x2)).| <= r * |.(x1 - x2).| by A4;

( f /. x1 = g /. x1 & f /. x2 = g /. x2 ) by REAL_NS1:def 4;

hence ||.((g /. x1) - (g /. x2)).|| <= r * |.(x1 - x2).| by A5, REAL_NS1:1, REAL_NS1:5; :: thesis: verum

hence f is Lipschitzian ; :: thesis: verum