let X be RealUnitarySpace; :: thesis: for f being linear-Functional of X

for g being linear-Functional of (RUSp2RNSp X) st f = g holds

( f is Lipschitzian iff g is Lipschitzian )

let f be linear-Functional of X; :: thesis: for g being linear-Functional of (RUSp2RNSp X) st f = g holds

( f is Lipschitzian iff g is Lipschitzian )

let g be linear-Functional of (RUSp2RNSp X); :: thesis: ( f = g implies ( f is Lipschitzian iff g is Lipschitzian ) )

assume AS: f = g ; :: thesis: ( f is Lipschitzian iff g is Lipschitzian )

set Y = RUSp2RNSp X;

then consider K being Real such that

A2: ( 0 <= K & ( for y being Point of (RUSp2RNSp X) holds |.(g . y).| <= K * ||.y.|| ) ) ;

A4: K + 0 < K + 1 by XREAL_1:8;

for x being Point of X holds |.(f . x).| <= (K + 1) * ||.x.||

for g being linear-Functional of (RUSp2RNSp X) st f = g holds

( f is Lipschitzian iff g is Lipschitzian )

let f be linear-Functional of X; :: thesis: for g being linear-Functional of (RUSp2RNSp X) st f = g holds

( f is Lipschitzian iff g is Lipschitzian )

let g be linear-Functional of (RUSp2RNSp X); :: thesis: ( f = g implies ( f is Lipschitzian iff g is Lipschitzian ) )

assume AS: f = g ; :: thesis: ( f is Lipschitzian iff g is Lipschitzian )

set Y = RUSp2RNSp X;

hereby :: thesis: ( g is Lipschitzian implies f is Lipschitzian )

assume
g is Lipschitzian
; :: thesis: f is Lipschitzian assume
f is Lipschitzian
; :: thesis: g is Lipschitzian

then consider K being Real such that

A1: ( 0 < K & ( for x being Point of X holds |.(f . x).| <= K * ||.x.|| ) ) by BHSP_6:def 4;

for y being Point of (RUSp2RNSp X) holds |.(g . y).| <= K * ||.y.||

end;then consider K being Real such that

A1: ( 0 < K & ( for x being Point of X holds |.(f . x).| <= K * ||.x.|| ) ) by BHSP_6:def 4;

for y being Point of (RUSp2RNSp X) holds |.(g . y).| <= K * ||.y.||

proof

hence
g is Lipschitzian
by A1; :: thesis: verum
let y be Point of (RUSp2RNSp X); :: thesis: |.(g . y).| <= K * ||.y.||

reconsider x = y as Point of X ;

||.y.|| = ||.x.|| by Def1;

hence |.(g . y).| <= K * ||.y.|| by A1, AS; :: thesis: verum

end;reconsider x = y as Point of X ;

||.y.|| = ||.x.|| by Def1;

hence |.(g . y).| <= K * ||.y.|| by A1, AS; :: thesis: verum

then consider K being Real such that

A2: ( 0 <= K & ( for y being Point of (RUSp2RNSp X) holds |.(g . y).| <= K * ||.y.|| ) ) ;

A4: K + 0 < K + 1 by XREAL_1:8;

for x being Point of X holds |.(f . x).| <= (K + 1) * ||.x.||

proof

hence
f is Lipschitzian
by A2, BHSP_6:def 4; :: thesis: verum
let x be Point of X; :: thesis: |.(f . x).| <= (K + 1) * ||.x.||

reconsider y = x as Point of (RUSp2RNSp X) ;

||.x.|| = ||.y.|| by Def1;

then B3: |.(f . x).| <= K * ||.x.|| by A2, AS;

0 <= ||.x.|| by BHSP_1:28;

then K * ||.x.|| <= (K + 1) * ||.x.|| by A4, XREAL_1:64;

hence |.(f . x).| <= (K + 1) * ||.x.|| by B3, XXREAL_0:2; :: thesis: verum

end;reconsider y = x as Point of (RUSp2RNSp X) ;

||.x.|| = ||.y.|| by Def1;

then B3: |.(f . x).| <= K * ||.x.|| by A2, AS;

0 <= ||.x.|| by BHSP_1:28;

then K * ||.x.|| <= (K + 1) * ||.x.|| by A4, XREAL_1:64;

hence |.(f . x).| <= (K + 1) * ||.x.|| by B3, XXREAL_0:2; :: thesis: verum