let X, Y be ComplexNormSpace; :: thesis: for g being Lipschitzian LinearOperator of X,Y holds PreNorms g is bounded_above

let g be Lipschitzian LinearOperator of X,Y; :: thesis: PreNorms g is bounded_above

PreNorms g is bounded_above

let g be Lipschitzian LinearOperator of X,Y; :: thesis: PreNorms g is bounded_above

PreNorms g is bounded_above

proof

hence
PreNorms g is bounded_above
; :: thesis: verum
consider K being Real such that

A1: 0 <= K and

A2: for x being VECTOR of X holds ||.(g . x).|| <= K * ||.x.|| by Def6;

take K ; :: according to XXREAL_2:def 10 :: thesis: K is UpperBound of PreNorms g

let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in PreNorms g or r <= K )

assume r in PreNorms g ; :: thesis: r <= K

then consider t being VECTOR of X such that

A3: r = ||.(g . t).|| and

A4: ||.t.|| <= 1 ;

A5: ||.(g . t).|| <= K * ||.t.|| by A2;

K * ||.t.|| <= K * 1 by A1, A4, XREAL_1:64;

hence r <= K by A3, A5, XXREAL_0:2; :: thesis: verum

end;A1: 0 <= K and

A2: for x being VECTOR of X holds ||.(g . x).|| <= K * ||.x.|| by Def6;

take K ; :: according to XXREAL_2:def 10 :: thesis: K is UpperBound of PreNorms g

let r be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not r in PreNorms g or r <= K )

assume r in PreNorms g ; :: thesis: r <= K

then consider t being VECTOR of X such that

A3: r = ||.(g . t).|| and

A4: ||.t.|| <= 1 ;

A5: ||.(g . t).|| <= K * ||.t.|| by A2;

K * ||.t.|| <= K * 1 by A1, A4, XREAL_1:64;

hence r <= K by A3, A5, XXREAL_0:2; :: thesis: verum