let X be RealUnitarySpace; :: thesis: for f being linear-Functional of X st ( for x being VECTOR of X holds f . x = 0 ) holds

f is Lipschitzian

let f be linear-Functional of X; :: thesis: ( ( for x being VECTOR of X holds f . x = 0 ) implies f is Lipschitzian )

assume A1: for x being VECTOR of X holds f . x = 0 ; :: thesis: f is Lipschitzian

for x being VECTOR of X holds |.(f . x).| <= 1 * ||.x.||

f is Lipschitzian

let f be linear-Functional of X; :: thesis: ( ( for x being VECTOR of X holds f . x = 0 ) implies f is Lipschitzian )

assume A1: for x being VECTOR of X holds f . x = 0 ; :: thesis: f is Lipschitzian

for x being VECTOR of X holds |.(f . x).| <= 1 * ||.x.||

proof

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

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

hence |.(f . x).| <= 1 * ||.x.|| by A1, COMPLEX1:44; :: thesis: verum

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

hence |.(f . x).| <= 1 * ||.x.|| by A1, COMPLEX1:44; :: thesis: verum