let X be RealUnitarySpace; :: thesis: for f being Function of X,REAL

for g being Function of (RUSp2RNSp X),REAL st f = g holds

( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )

let f be Function of X,REAL; :: thesis: for g being Function of (RUSp2RNSp X),REAL st f = g holds

( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )

let g be Function of (RUSp2RNSp X),REAL; :: thesis: ( f = g implies ( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) ) )

assume AS: f = g ; :: thesis: ( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )

set Y = RUSp2RNSp X;

thus ( f is_Lipschitzian_on the carrier of X implies g is_Lipschitzian_on the carrier of (RUSp2RNSp X) ) :: thesis: ( g is_Lipschitzian_on the carrier of (RUSp2RNSp X) implies f is_Lipschitzian_on the carrier of X )

then consider r being Real such that

A2: ( 0 < r & ( for y1, y2 being Point of (RUSp2RNSp X) st y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) holds

|.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).|| ) ) ;

for x1, x2 being Point of X st x1 in the carrier of X & x2 in the carrier of X holds

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

for g being Function of (RUSp2RNSp X),REAL st f = g holds

( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )

let f be Function of X,REAL; :: thesis: for g being Function of (RUSp2RNSp X),REAL st f = g holds

( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )

let g be Function of (RUSp2RNSp X),REAL; :: thesis: ( f = g implies ( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) ) )

assume AS: f = g ; :: thesis: ( f is_Lipschitzian_on the carrier of X iff g is_Lipschitzian_on the carrier of (RUSp2RNSp X) )

set Y = RUSp2RNSp X;

thus ( f is_Lipschitzian_on the carrier of X implies g is_Lipschitzian_on the carrier of (RUSp2RNSp X) ) :: thesis: ( g is_Lipschitzian_on the carrier of (RUSp2RNSp X) implies f is_Lipschitzian_on the carrier of X )

proof

assume A11:
g is_Lipschitzian_on the carrier of (RUSp2RNSp X)
; :: thesis: f is_Lipschitzian_on the carrier of X
assume A11:
f is_Lipschitzian_on the carrier of X
; :: thesis: g is_Lipschitzian_on the carrier of (RUSp2RNSp X)

then consider r being Real such that

A2: ( 0 < r & ( for x1, x2 being Point of X st x1 in the carrier of X & x2 in the carrier of X holds

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

for y1, y2 being Point of (RUSp2RNSp X) st y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) holds

|.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).||

end;then consider r being Real such that

A2: ( 0 < r & ( for x1, x2 being Point of X st x1 in the carrier of X & x2 in the carrier of X holds

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

for y1, y2 being Point of (RUSp2RNSp X) st y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) holds

|.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).||

proof

hence
g is_Lipschitzian_on the carrier of (RUSp2RNSp X)
by A2, A11, AS; :: thesis: verum
let y1, y2 be Point of (RUSp2RNSp X); :: thesis: ( y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) implies |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).|| )

assume ( y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) ) ; :: thesis: |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).||

reconsider x1 = y1, x2 = y2 as Point of X ;

||.(y1 - y2).|| = ||.(x1 - x2).|| by RHS4, RHS6;

hence |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).|| by A2, AS; :: thesis: verum

end;assume ( y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) ) ; :: thesis: |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).||

reconsider x1 = y1, x2 = y2 as Point of X ;

||.(y1 - y2).|| = ||.(x1 - x2).|| by RHS4, RHS6;

hence |.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).|| by A2, AS; :: thesis: verum

then consider r being Real such that

A2: ( 0 < r & ( for y1, y2 being Point of (RUSp2RNSp X) st y1 in the carrier of (RUSp2RNSp X) & y2 in the carrier of (RUSp2RNSp X) holds

|.((g /. y1) - (g /. y2)).| <= r * ||.(y1 - y2).|| ) ) ;

for x1, x2 being Point of X st x1 in the carrier of X & x2 in the carrier of X holds

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

proof

hence
f is_Lipschitzian_on the carrier of X
by A2, A11, AS; :: thesis: verum
let x1, x2 be Point of X; :: thesis: ( x1 in the carrier of X & x2 in the carrier of X implies |.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| )

assume ( x1 in the carrier of X & x2 in the carrier of X ) ; :: thesis: |.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).||

reconsider y1 = x1, y2 = x2 as Point of (RUSp2RNSp X) ;

||.(x1 - x2).|| = ||.(y1 - y2).|| by RHS4, RHS6;

hence |.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| by A2, AS; :: thesis: verum

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

reconsider y1 = x1, y2 = x2 as Point of (RUSp2RNSp X) ;

||.(x1 - x2).|| = ||.(y1 - y2).|| by RHS4, RHS6;

hence |.((f /. x1) - (f /. x2)).| <= r * ||.(x1 - x2).|| by A2, AS; :: thesis: verum