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.||
proof
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;
hence f is Lipschitzian by A11, BHSP_6:def 4; :: thesis: verum