let S, T be RealNormSpace; :: thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators (S,T))
for r being Real st 0 <= r & ( for x being Point of S st ||.x.|| <= 1 holds
||.(f . x).|| <= r * ||.x.|| ) holds
||.f.|| <= r
let f be Point of (R_NormSpace_of_BoundedLinearOperators (S,T)); :: thesis: for r being Real st 0 <= r & ( for x being Point of S st ||.x.|| <= 1 holds
||.(f . x).|| <= r * ||.x.|| ) holds
||.f.|| <= r
let r be Real; :: thesis: ( 0 <= r & ( for x being Point of S st ||.x.|| <= 1 holds
||.(f . x).|| <= r * ||.x.|| ) implies ||.f.|| <= r )
assume A1: ( 0 <= r & ( for x being Point of S st ||.x.|| <= 1 holds
||.(f . x).|| <= r * ||.x.|| ) ) ; :: thesis: ||.f.|| <= r
A2: now :: thesis: for x being Point of S st ||.x.|| <= 1 holds
||.(f . x).|| <= r
let x be Point of S; :: thesis: ( ||.x.|| <= 1 implies ||.(f . x).|| <= r )
assume ||.x.|| <= 1 ; :: thesis: ||.(f . x).|| <= r
then ( ||.(f . x).|| <= r * ||.x.|| & r * ||.x.|| <= r * 1 ) by A1, XREAL_1:64;
hence ||.(f . x).|| <= r by XXREAL_0:2; :: thesis: verum
end;
reconsider g = f as Lipschitzian LinearOperator of S,T by LOPBAN_1:def 9;
set PreNormS = PreNorms (modetrans (f,S,T));
A3: for y being ExtReal st y in PreNorms (modetrans (f,S,T)) holds
y <= r
proof
let y be ExtReal; :: thesis: ( y in PreNorms (modetrans (f,S,T)) implies y <= r )
assume y in PreNorms (modetrans (f,S,T)) ; :: thesis: y <= r
then consider x being VECTOR of S such that
A4: ( y = ||.((modetrans (f,S,T)) . x).|| & ||.x.|| <= 1 ) ;
y = ||.(g . x).|| by A4, LOPBAN_1:29;
hence y <= r by A2, A4; :: thesis: verum
end;
set UBPreNormS = upper_bound (PreNorms (modetrans (f,S,T)));
set dif = (upper_bound (PreNorms (modetrans (f,S,T)))) - r;
now :: thesis: not upper_bound (PreNorms (modetrans (f,S,T))) > r
assume upper_bound (PreNorms (modetrans (f,S,T))) > r ; :: thesis: contradiction
then A5: (upper_bound (PreNorms (modetrans (f,S,T)))) - r > 0 by XREAL_1:50;
r is UpperBound of PreNorms (modetrans (f,S,T)) by A3, XXREAL_2:def 1;
then PreNorms (modetrans (f,S,T)) is bounded_above by XXREAL_2:def 10;
then ex w being Real st
( w in PreNorms (modetrans (f,S,T)) & (upper_bound (PreNorms (modetrans (f,S,T)))) - ((upper_bound (PreNorms (modetrans (f,S,T)))) - r) < w ) by A5, SEQ_4:def 1;
hence contradiction by A3; :: thesis: verum
end;
then upper_bound (PreNorms g) <= r by LOPBAN_1:def 11;
hence ||.f.|| <= r by LOPBAN_1:30; :: thesis: verum