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

for y being Point of X st ( for x being Point of X holds f . x = x .|. y ) holds

f is Lipschitzian

let f be linear-Functional of X; :: thesis: for y being Point of X st ( for x being Point of X holds f . x = x .|. y ) holds

f is Lipschitzian

let y be Point of X; :: thesis: ( ( for x being Point of X holds f . x = x .|. y ) implies f is Lipschitzian )

assume AS: for x being Point of X holds f . x = x .|. y ; :: thesis: f is Lipschitzian

reconsider K = ||.y.|| + 1 as Real ;

A11: 0 <= ||.y.|| by BHSP_1:28;

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

for y being Point of X st ( for x being Point of X holds f . x = x .|. y ) holds

f is Lipschitzian

let f be linear-Functional of X; :: thesis: for y being Point of X st ( for x being Point of X holds f . x = x .|. y ) holds

f is Lipschitzian

let y be Point of X; :: thesis: ( ( for x being Point of X holds f . x = x .|. y ) implies f is Lipschitzian )

assume AS: for x being Point of X holds f . x = x .|. y ; :: thesis: f is Lipschitzian

reconsider K = ||.y.|| + 1 as Real ;

A11: 0 <= ||.y.|| by BHSP_1:28;

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

proof

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

B1: |.(x .|. y).| <= ||.x.|| * ||.y.|| by BHSP_1:29;

B2: ||.y.|| < ||.y.|| + 1 by XREAL_1:145;

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

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

then |.(x .|. y).| <= (||.y.|| + 1) * ||.x.|| by B1, XXREAL_0:2;

hence |.(f . x).| <= K * ||.x.|| by AS; :: thesis: verum

end;B1: |.(x .|. y).| <= ||.x.|| * ||.y.|| by BHSP_1:29;

B2: ||.y.|| < ||.y.|| + 1 by XREAL_1:145;

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

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

then |.(x .|. y).| <= (||.y.|| + 1) * ||.x.|| by B1, XXREAL_0:2;

hence |.(f . x).| <= K * ||.x.|| by AS; :: thesis: verum