:: by Hideki Sakurai , Hisayoshi Kunimune and Yasunari Shidama

::

:: Received October 9, 2007

:: Copyright (c) 2007-2021 Association of Mizar Users

theorem Th1: :: LOPBAN_5:1

for seq being Real_Sequence

for r being Real st seq is bounded & 0 <= r holds

lim_inf (r (#) seq) = r * (lim_inf seq)

for r being Real st seq is bounded & 0 <= r holds

lim_inf (r (#) seq) = r * (lim_inf seq)

proof end;

theorem :: LOPBAN_5:2

for seq being Real_Sequence

for r being Real st seq is bounded & 0 <= r holds

lim_sup (r (#) seq) = r * (lim_sup seq)

for r being Real st seq is bounded & 0 <= r holds

lim_sup (r (#) seq) = r * (lim_sup seq)

proof end;

definition

let X be RealNormSpace;

let x0 be Point of X;

let r be Real;

{ x where x is Point of X : ||.(x0 - x).|| < r } is Subset of X

end;
let x0 be Point of X;

let r be Real;

func Ball (x0,r) -> Subset of X equals :: LOPBAN_5:def 1

{ x where x is Point of X : ||.(x0 - x).|| < r } ;

coherence { x where x is Point of X : ||.(x0 - x).|| < r } ;

{ x where x is Point of X : ||.(x0 - x).|| < r } is Subset of X

proof end;

:: deftheorem defines Ball LOPBAN_5:def 1 :

for X being RealNormSpace

for x0 being Point of X

for r being Real holds Ball (x0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } ;

for X being RealNormSpace

for x0 being Point of X

for r being Real holds Ball (x0,r) = { x where x is Point of X : ||.(x0 - x).|| < r } ;

:: Baire Category Theorem (Banach spaces)

theorem Th3: :: LOPBAN_5:3

for X being RealBanachSpace

for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Nat holds Y . n is closed ) holds

ex n0 being Nat ex r being Real ex x0 being Point of X st

( 0 < r & Ball (x0,r) c= Y . n0 )

for Y being SetSequence of X st union (rng Y) = the carrier of X & ( for n being Nat holds Y . n is closed ) holds

ex n0 being Nat ex r being Real ex x0 being Point of X st

( 0 < r & Ball (x0,r) c= Y . n0 )

proof end;

theorem Th4: :: LOPBAN_5:4

for X, Y being RealNormSpace

for f being Lipschitzian LinearOperator of X,Y holds

( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )

for f being Lipschitzian LinearOperator of X,Y holds

( f is_Lipschitzian_on the carrier of X & f is_continuous_on the carrier of X & ( for x being Point of X holds f is_continuous_in x ) )

proof end;

theorem Th5: :: LOPBAN_5:5

for X being RealBanachSpace

for Y being RealNormSpace

for T being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being Real st

( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds

||.(f . x).|| <= K ) ) ) holds

ex L being Real st

( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds

||.f.|| <= L ) )

for Y being RealNormSpace

for T being Subset of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ( for x being Point of X ex K being Real st

( 0 <= K & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds

||.(f . x).|| <= K ) ) ) holds

ex L being Real st

( 0 <= L & ( for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f in T holds

||.f.|| <= L ) )

proof end;

definition

let X, Y be RealNormSpace;

let H be sequence of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y));

let x be Point of X;

ex b_{1} being sequence of Y st

for n being Nat holds b_{1} . n = (H . n) . x

for b_{1}, b_{2} being sequence of Y st ( for n being Nat holds b_{1} . n = (H . n) . x ) & ( for n being Nat holds b_{2} . n = (H . n) . x ) holds

b_{1} = b_{2}

end;
let H be sequence of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y));

let x be Point of X;

func H # x -> sequence of Y means :Def2: :: LOPBAN_5:def 2

for n being Nat holds it . n = (H . n) . x;

existence for n being Nat holds it . n = (H . n) . x;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines # LOPBAN_5:def 2 :

for X, Y being RealNormSpace

for H being sequence of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for x being Point of X

for b_{5} being sequence of Y holds

( b_{5} = H # x iff for n being Nat holds b_{5} . n = (H . n) . x );

for X, Y being RealNormSpace

for H being sequence of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for x being Point of X

for b

( b

theorem Th6: :: LOPBAN_5:6

for X being RealBanachSpace

for Y being RealNormSpace

for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for tseq being Function of X,Y st ( for x being Point of X holds

( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds

( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds

||.ttseq.|| <= lim_inf ||.vseq.|| ) )

for Y being RealNormSpace

for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for tseq being Function of X,Y st ( for x being Point of X holds

( vseq # x is convergent & tseq . x = lim (vseq # x) ) ) holds

( tseq is Lipschitzian LinearOperator of X,Y & ( for x being Point of X holds ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) & ( for ttseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st ttseq = tseq holds

||.ttseq.|| <= lim_inf ||.vseq.|| ) )

proof end;

theorem Th7: :: LOPBAN_5:7

for X being RealBanachSpace

for X0 being Subset of (LinearTopSpaceNorm X)

for Y being RealBanachSpace

for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds

vseq # x is convergent ) & ( for x being Point of X ex K being Real st

( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds

for x being Point of X holds vseq # x is convergent

for X0 being Subset of (LinearTopSpaceNorm X)

for Y being RealBanachSpace

for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds

vseq # x is convergent ) & ( for x being Point of X ex K being Real st

( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds

for x being Point of X holds vseq # x is convergent

proof end;

theorem :: LOPBAN_5:8

for X, Y being RealBanachSpace

for X0 being Subset of (LinearTopSpaceNorm X)

for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds

vseq # x is convergent ) & ( for x being Point of X ex K being Real st

( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds

ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st

( ( for x being Point of X holds

( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )

for X0 being Subset of (LinearTopSpaceNorm X)

for vseq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st X0 is dense & ( for x being Point of X st x in X0 holds

vseq # x is convergent ) & ( for x being Point of X ex K being Real st

( 0 <= K & ( for n being Nat holds ||.((vseq # x) . n).|| <= K ) ) ) holds

ex tseq being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st

( ( for x being Point of X holds

( vseq # x is convergent & tseq . x = lim (vseq # x) & ||.(tseq . x).|| <= (lim_inf ||.vseq.||) * ||.x.|| ) ) & ||.tseq.|| <= lim_inf ||.vseq.|| )

proof end;