theorem
for
E,
F,
G being
RealNormSpace for
f being
BilinearOperator of
E,
F,
G holds
( (
f is_continuous_on the
carrier of
[:E,F:] implies
f is_continuous_in 0. [:E,F:] ) & (
f is_continuous_in 0. [:E,F:] implies
f is_continuous_on the
carrier of
[:E,F:] ) & (
f is_continuous_on the
carrier of
[:E,F:] implies ex
K being
Real st
(
0 <= K & ( for
x being
Point of
E for
y being
Point of
F holds
||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) ) & ( ex
K being
Real st
(
0 <= K & ( for
x being
Point of
E for
y being
Point of
F holds
||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) implies
f is_continuous_on the
carrier of
[:E,F:] ) )