let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace
for f being MultilinearOperator of X,Y st ( for x being VECTOR of (product X) holds f . x = 0. Y ) holds
f is Lipschitzian
let Y be RealNormSpace; :: thesis: for f being MultilinearOperator of X,Y st ( for x being VECTOR of (product X) holds f . x = 0. Y ) holds
f is Lipschitzian
let f be MultilinearOperator of X,Y; :: thesis: ( ( for x being VECTOR of (product X) holds f . x = 0. Y ) implies f is Lipschitzian )
assume A1: for x being VECTOR of (product X) holds f . x = 0. Y ; :: thesis: f is Lipschitzian
A2: now :: thesis: for x being VECTOR of (product X) holds ||.(f . x).|| = 0 * (NrProduct x)
let x be VECTOR of (product X); :: thesis: ||.(f . x).|| = 0 * (NrProduct x)
thus ||.(f . x).|| = ||.(0. Y).|| by A1
.= 0 * (NrProduct x) ; :: thesis: verum
end;
take 0 ; :: according to LOPBAN10:def 10 :: thesis: ( 0 <= 0 & ( for x being Point of (product X) holds ||.(f . x).|| <= 0 * (NrProduct x) ) )
thus ( 0 <= 0 & ( for x being Point of (product X) holds ||.(f . x).|| <= 0 * (NrProduct x) ) ) by A2; :: thesis: verum