:: by Yasunari Shidama

::

:: Received December 22, 2003

:: Copyright (c) 2003-2012 Association of Mizar Users

begin

definition

let X be set ;

let Y be non empty set ;

let F be Function of [:REAL,Y:],Y;

let a be real number ;

let f be Function of X,Y;

:: original: [;]

redefine func F [;] (a,f) -> Element of Funcs (X,Y);

coherence

F [;] (a,f) is Element of Funcs (X,Y)

end;
let Y be non empty set ;

let F be Function of [:REAL,Y:],Y;

let a be real number ;

let f be Function of X,Y;

:: original: [;]

redefine func F [;] (a,f) -> Element of Funcs (X,Y);

coherence

F [;] (a,f) is Element of Funcs (X,Y)

proof end;

definition

let X be non empty set ;

let Y be non empty addLoopStr ;

ex b_{1} being BinOp of (Funcs (X, the carrier of Y)) st

for f, g being Element of Funcs (X, the carrier of Y) holds b_{1} . (f,g) = the addF of Y .: (f,g)

for b_{1}, b_{2} being BinOp of (Funcs (X, the carrier of Y)) st ( for f, g being Element of Funcs (X, the carrier of Y) holds b_{1} . (f,g) = the addF of Y .: (f,g) ) & ( for f, g being Element of Funcs (X, the carrier of Y) holds b_{2} . (f,g) = the addF of Y .: (f,g) ) holds

b_{1} = b_{2}

end;
let Y be non empty addLoopStr ;

func FuncAdd (X,Y) -> BinOp of (Funcs (X, the carrier of Y)) means :Def1: :: LOPBAN_1:def 1

for f, g being Element of Funcs (X, the carrier of Y) holds it . (f,g) = the addF of Y .: (f,g);

existence for f, g being Element of Funcs (X, the carrier of Y) holds it . (f,g) = the addF of Y .: (f,g);

ex b

for f, g being Element of Funcs (X, the carrier of Y) holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines FuncAdd LOPBAN_1:def 1 :

for X being non empty set

for Y being non empty addLoopStr

for b_{3} being BinOp of (Funcs (X, the carrier of Y)) holds

( b_{3} = FuncAdd (X,Y) iff for f, g being Element of Funcs (X, the carrier of Y) holds b_{3} . (f,g) = the addF of Y .: (f,g) );

for X being non empty set

for Y being non empty addLoopStr

for b

( b

definition

let X be non empty set ;

let Y be RealLinearSpace;

ex b_{1} being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st

for a being Real

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (b_{1} . [a,f]) . x = a * (f . x)

for b_{1}, b_{2} being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) st ( for a being Real

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (b_{1} . [a,f]) . x = a * (f . x) ) & ( for a being Real

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (b_{2} . [a,f]) . x = a * (f . x) ) holds

b_{1} = b_{2}

end;
let Y be RealLinearSpace;

func FuncExtMult (X,Y) -> Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) means :Def2: :: LOPBAN_1:def 2

for a being Real

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (it . [a,f]) . x = a * (f . x);

existence for a being Real

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (it . [a,f]) . x = a * (f . x);

ex b

for a being Real

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (b

proof end;

uniqueness for b

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (b

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (b

b

proof end;

:: deftheorem Def2 defines FuncExtMult LOPBAN_1:def 2 :

for X being non empty set

for Y being RealLinearSpace

for b_{3} being Function of [:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)) holds

( b_{3} = FuncExtMult (X,Y) iff for a being Real

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (b_{3} . [a,f]) . x = a * (f . x) );

for X being non empty set

for Y being RealLinearSpace

for b

( b

for f being Element of Funcs (X, the carrier of Y)

for x being Element of X holds (b

definition

let X be set ;

let Y be non empty ZeroStr ;

coherence

X --> (0. Y) is Element of Funcs (X, the carrier of Y) by FUNCT_2:8;

end;
let Y be non empty ZeroStr ;

coherence

X --> (0. Y) is Element of Funcs (X, the carrier of Y) by FUNCT_2:8;

:: deftheorem defines FuncZero LOPBAN_1:def 3 :

for X being set

for Y being non empty ZeroStr holds FuncZero (X,Y) = X --> (0. Y);

for X being set

for Y being non empty ZeroStr holds FuncZero (X,Y) = X --> (0. Y);

Lm1: for A, B being non empty set

for x being Element of A

for f being Function of A,B holds x in dom f

proof end;

theorem Th1: :: LOPBAN_1:1

for X being non empty set

for Y being non empty addLoopStr

for f, g, h being Element of Funcs (X, the carrier of Y) holds

( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) )

for Y being non empty addLoopStr

for f, g, h being Element of Funcs (X, the carrier of Y) holds

( h = (FuncAdd (X,Y)) . (f,g) iff for x being Element of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th2: :: LOPBAN_1:2

for X being non empty set

for Y being RealLinearSpace

for h, f being Element of Funcs (X, the carrier of Y)

for a being Real holds

( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )

for Y being RealLinearSpace

for h, f being Element of Funcs (X, the carrier of Y)

for a being Real holds

( h = (FuncExtMult (X,Y)) . [a,f] iff for x being Element of X holds h . x = a * (f . x) )

proof end;

theorem Th3: :: LOPBAN_1:3

for X being non empty set

for Y being RealLinearSpace

for f, g being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)

for Y being RealLinearSpace

for f, g being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,g) = (FuncAdd (X,Y)) . (g,f)

proof end;

theorem Th4: :: LOPBAN_1:4

for X being non empty set

for Y being RealLinearSpace

for f, g, h being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)

for Y being RealLinearSpace

for f, g, h being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncAdd (X,Y)) . (g,h))) = (FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (f,g)),h)

proof end;

theorem Th5: :: LOPBAN_1:5

for X being non empty set

for Y being RealLinearSpace

for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f

for Y being RealLinearSpace

for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . ((FuncZero (X,Y)),f) = f

proof end;

theorem Th6: :: LOPBAN_1:6

for X being non empty set

for Y being RealLinearSpace

for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)

for Y being RealLinearSpace

for f being Element of Funcs (X, the carrier of Y) holds (FuncAdd (X,Y)) . (f,((FuncExtMult (X,Y)) . [(- 1),f])) = FuncZero (X,Y)

proof end;

theorem Th7: :: LOPBAN_1:7

for X being non empty set

for Y being RealLinearSpace

for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1,f] = f

for Y being RealLinearSpace

for f being Element of Funcs (X, the carrier of Y) holds (FuncExtMult (X,Y)) . [1,f] = f

proof end;

theorem Th8: :: LOPBAN_1:8

for X being non empty set

for Y being RealLinearSpace

for f being Element of Funcs (X, the carrier of Y)

for a, b being Real holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

for Y being RealLinearSpace

for f being Element of Funcs (X, the carrier of Y)

for a, b being Real holds (FuncExtMult (X,Y)) . [a,((FuncExtMult (X,Y)) . [b,f])] = (FuncExtMult (X,Y)) . [(a * b),f]

proof end;

theorem Th9: :: LOPBAN_1:9

for X being non empty set

for Y being RealLinearSpace

for f being Element of Funcs (X, the carrier of Y)

for a, b being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]

for Y being RealLinearSpace

for f being Element of Funcs (X, the carrier of Y)

for a, b being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [b,f])) = (FuncExtMult (X,Y)) . [(a + b),f]

proof end;

Lm2: for X being non empty set

for Y being RealLinearSpace

for f, g being Element of Funcs (X, the carrier of Y)

for a being Real holds (FuncAdd (X,Y)) . (((FuncExtMult (X,Y)) . [a,f]),((FuncExtMult (X,Y)) . [a,g])) = (FuncExtMult (X,Y)) . [a,((FuncAdd (X,Y)) . (f,g))]

proof end;

theorem Th10: :: LOPBAN_1:10

for X being non empty set

for Y being RealLinearSpace holds RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace

for Y being RealLinearSpace holds RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace

proof end;

definition

let X be non empty set ;

let Y be RealLinearSpace;

RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace by Th10;

end;
let Y be RealLinearSpace;

func RealVectSpace (X,Y) -> RealLinearSpace equals :: LOPBAN_1:def 4

RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);

coherence RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);

RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #) is RealLinearSpace by Th10;

:: deftheorem defines RealVectSpace LOPBAN_1:def 4 :

for X being non empty set

for Y being RealLinearSpace holds RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);

for X being non empty set

for Y being RealLinearSpace holds RealVectSpace (X,Y) = RLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(FuncExtMult (X,Y)) #);

registration
end;

registration

let X be non empty set ;

let Y be RealLinearSpace;

coherence

RealVectSpace (X,Y) is constituted-Functions by MONOID_0:80;

end;
let Y be RealLinearSpace;

coherence

RealVectSpace (X,Y) is constituted-Functions by MONOID_0:80;

definition

let X be non empty set ;

let Y be RealLinearSpace;

let f be VECTOR of (RealVectSpace (X,Y));

let x be Element of X;

:: original: .

redefine func f . x -> VECTOR of Y;

coherence

f . x is VECTOR of Y

end;
let Y be RealLinearSpace;

let f be VECTOR of (RealVectSpace (X,Y));

let x be Element of X;

:: original: .

redefine func f . x -> VECTOR of Y;

coherence

f . x is VECTOR of Y

proof end;

theorem :: LOPBAN_1:11

theorem :: LOPBAN_1:12

theorem :: LOPBAN_1:13

for X being non empty set

for Y being RealLinearSpace holds 0. (RealVectSpace (X,Y)) = X --> (0. Y) ;

for Y being RealLinearSpace holds 0. (RealVectSpace (X,Y)) = X --> (0. Y) ;

begin

definition

let X, Y be non empty RLSStruct ;

let IT be Function of X,Y;

end;
let IT be Function of X,Y;

attr IT is homogeneous means :Def5: :: LOPBAN_1:def 5

for x being VECTOR of X

for r being Real holds IT . (r * x) = r * (IT . x);

for x being VECTOR of X

for r being Real holds IT . (r * x) = r * (IT . x);

:: deftheorem Def5 defines homogeneous LOPBAN_1:def 5 :

for X, Y being non empty RLSStruct

for IT being Function of X,Y holds

( IT is homogeneous iff for x being VECTOR of X

for r being Real holds IT . (r * x) = r * (IT . x) );

for X, Y being non empty RLSStruct

for IT being Function of X,Y holds

( IT is homogeneous iff for x being VECTOR of X

for r being Real holds IT . (r * x) = r * (IT . x) );

registration

let X be non empty RLSStruct ;

let Y be RealLinearSpace;

ex b_{1} being Function of X,Y st

( b_{1} is additive & b_{1} is homogeneous )

end;
let Y be RealLinearSpace;

cluster non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total additive homogeneous for Element of bool [: the carrier of X, the carrier of Y:];

existence ex b

( b

proof end;

definition
end;

definition

let X, Y be RealLinearSpace;

ex b_{1} being Subset of (RealVectSpace ( the carrier of X,Y)) st

for x being set holds

( x in b_{1} iff x is LinearOperator of X,Y )

for b_{1}, b_{2} being Subset of (RealVectSpace ( the carrier of X,Y)) st ( for x being set holds

( x in b_{1} iff x is LinearOperator of X,Y ) ) & ( for x being set holds

( x in b_{2} iff x is LinearOperator of X,Y ) ) holds

b_{1} = b_{2}

end;
func LinearOperators (X,Y) -> Subset of (RealVectSpace ( the carrier of X,Y)) means :Def6: :: LOPBAN_1:def 6

for x being set holds

( x in it iff x is LinearOperator of X,Y );

existence for x being set holds

( x in it iff x is LinearOperator of X,Y );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def6 defines LinearOperators LOPBAN_1:def 6 :

for X, Y being RealLinearSpace

for b_{3} being Subset of (RealVectSpace ( the carrier of X,Y)) holds

( b_{3} = LinearOperators (X,Y) iff for x being set holds

( x in b_{3} iff x is LinearOperator of X,Y ) );

for X, Y being RealLinearSpace

for b

( b

( x in b

registration

let X, Y be RealLinearSpace;

coherence

( not LinearOperators (X,Y) is empty & LinearOperators (X,Y) is functional )

end;
coherence

( not LinearOperators (X,Y) is empty & LinearOperators (X,Y) is functional )

proof end;

theorem :: LOPBAN_1:15

for X, Y being RealLinearSpace holds RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is Subspace of RealVectSpace ( the carrier of X,Y) by Th14, RSSPACE:11;

registration

let X, Y be RealLinearSpace;

( RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is Abelian & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is add-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_zeroed & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_complementable & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is vector-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-unital ) by Th14, RSSPACE:11;

end;
cluster RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence ( RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is Abelian & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is add-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_zeroed & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is right_complementable & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is vector-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-distributive & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-associative & RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is scalar-unital ) by Th14, RSSPACE:11;

definition

let X, Y be RealLinearSpace;

RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is RealLinearSpace ;

end;
func R_VectorSpace_of_LinearOperators (X,Y) -> RealLinearSpace equals :: LOPBAN_1:def 7

RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);

coherence RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);

RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #) is RealLinearSpace ;

:: deftheorem defines R_VectorSpace_of_LinearOperators LOPBAN_1:def 7 :

for X, Y being RealLinearSpace holds R_VectorSpace_of_LinearOperators (X,Y) = RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);

for X, Y being RealLinearSpace holds R_VectorSpace_of_LinearOperators (X,Y) = RLSStruct(# (LinearOperators (X,Y)),(Zero_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Add_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))),(Mult_ ((LinearOperators (X,Y)),(RealVectSpace ( the carrier of X,Y)))) #);

registration
end;

registration

let X, Y be RealLinearSpace;

coherence

R_VectorSpace_of_LinearOperators (X,Y) is constituted-Functions by MONOID_0:80;

end;
coherence

R_VectorSpace_of_LinearOperators (X,Y) is constituted-Functions by MONOID_0:80;

definition

let X, Y be RealLinearSpace;

let f be Element of (R_VectorSpace_of_LinearOperators (X,Y));

let v be VECTOR of X;

:: original: .

redefine func f . v -> VECTOR of Y;

coherence

f . v is VECTOR of Y

end;
let f be Element of (R_VectorSpace_of_LinearOperators (X,Y));

let v be VECTOR of X;

:: original: .

redefine func f . v -> VECTOR of Y;

coherence

f . v is VECTOR of Y

proof end;

theorem Th16: :: LOPBAN_1:16

for X, Y being RealLinearSpace

for f, g, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) holds

( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )

for f, g, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y)) holds

( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th17: :: LOPBAN_1:17

for X, Y being RealLinearSpace

for f, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y))

for a being Real holds

( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )

for f, h being VECTOR of (R_VectorSpace_of_LinearOperators (X,Y))

for a being Real holds

( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )

proof end;

theorem Th18: :: LOPBAN_1:18

for X, Y being RealLinearSpace holds 0. (R_VectorSpace_of_LinearOperators (X,Y)) = the carrier of X --> (0. Y)

proof end;

begin

theorem Th20: :: LOPBAN_1:20

for X being RealNormSpace

for seq being sequence of X

for g being Point of X st seq is convergent & lim seq = g holds

( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )

for seq being sequence of X

for g being Point of X st seq is convergent & lim seq = g holds

( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )

proof end;

:: deftheorem Def8 defines Lipschitzian LOPBAN_1:def 8 :

for X, Y being RealNormSpace

for IT being LinearOperator of X,Y holds

( IT is Lipschitzian iff ex K being Real st

( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) ) );

for X, Y being RealNormSpace

for IT being LinearOperator of X,Y holds

( IT is Lipschitzian iff ex K being Real st

( 0 <= K & ( for x being VECTOR of X holds ||.(IT . x).|| <= K * ||.x.|| ) ) );

theorem Th21: :: LOPBAN_1:21

for X, Y being RealNormSpace

for f being LinearOperator of X,Y st ( for x being VECTOR of X holds f . x = 0. Y ) holds

f is Lipschitzian

for f being LinearOperator of X,Y st ( for x being VECTOR of X holds f . x = 0. Y ) holds

f is Lipschitzian

proof end;

registration

let X, Y be RealNormSpace;

ex b_{1} being LinearOperator of X,Y st b_{1} is Lipschitzian

end;
cluster non empty Relation-like the carrier of X -defined the carrier of Y -valued Function-like total quasi_total additive homogeneous Lipschitzian for Element of bool [: the carrier of X, the carrier of Y:];

existence ex b

proof end;

definition

let X, Y be RealNormSpace;

ex b_{1} being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) st

for x being set holds

( x in b_{1} iff x is Lipschitzian LinearOperator of X,Y )

for b_{1}, b_{2} being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) st ( for x being set holds

( x in b_{1} iff x is Lipschitzian LinearOperator of X,Y ) ) & ( for x being set holds

( x in b_{2} iff x is Lipschitzian LinearOperator of X,Y ) ) holds

b_{1} = b_{2}

end;
func BoundedLinearOperators (X,Y) -> Subset of (R_VectorSpace_of_LinearOperators (X,Y)) means :Def9: :: LOPBAN_1:def 9

for x being set holds

( x in it iff x is Lipschitzian LinearOperator of X,Y );

existence for x being set holds

( x in it iff x is Lipschitzian LinearOperator of X,Y );

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

:: deftheorem Def9 defines BoundedLinearOperators LOPBAN_1:def 9 :

for X, Y being RealNormSpace

for b_{3} being Subset of (R_VectorSpace_of_LinearOperators (X,Y)) holds

( b_{3} = BoundedLinearOperators (X,Y) iff for x being set holds

( x in b_{3} iff x is Lipschitzian LinearOperator of X,Y ) );

for X, Y being RealNormSpace

for b

( b

( x in b

registration
end;

theorem :: LOPBAN_1:23

for X, Y being RealNormSpace holds RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is Subspace of R_VectorSpace_of_LinearOperators (X,Y) by Th22, RSSPACE:11;

registration

let X, Y be RealNormSpace;

( RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is Abelian & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is add-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_zeroed & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_complementable & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is vector-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-unital ) by Th22, RSSPACE:11;

end;
cluster RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) -> right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence ( RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is Abelian & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is add-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_zeroed & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is right_complementable & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is vector-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-distributive & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-associative & RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is scalar-unital ) by Th22, RSSPACE:11;

definition

let X, Y be RealNormSpace;

RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is RealLinearSpace ;

end;
func R_VectorSpace_of_BoundedLinearOperators (X,Y) -> RealLinearSpace equals :: LOPBAN_1:def 10

RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #);

coherence RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #);

RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #) is RealLinearSpace ;

:: deftheorem defines R_VectorSpace_of_BoundedLinearOperators LOPBAN_1:def 10 :

for X, Y being RealNormSpace holds R_VectorSpace_of_BoundedLinearOperators (X,Y) = RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #);

for X, Y being RealNormSpace holds R_VectorSpace_of_BoundedLinearOperators (X,Y) = RLSStruct(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))) #);

registration
end;

registration

let X, Y be RealNormSpace;

for b_{1} being Element of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds

( b_{1} is Function-like & b_{1} is Relation-like )
;

end;
cluster -> Relation-like Function-like for Element of the carrier of (R_VectorSpace_of_BoundedLinearOperators (X,Y));

coherence for b

( b

definition

let X, Y be RealNormSpace;

let f be Element of (R_VectorSpace_of_BoundedLinearOperators (X,Y));

let v be VECTOR of X;

:: original: .

redefine func f . v -> VECTOR of Y;

coherence

f . v is VECTOR of Y

end;
let f be Element of (R_VectorSpace_of_BoundedLinearOperators (X,Y));

let v be VECTOR of X;

:: original: .

redefine func f . v -> VECTOR of Y;

coherence

f . v is VECTOR of Y

proof end;

theorem Th24: :: LOPBAN_1:24

for X, Y being RealNormSpace

for f, g, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds

( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )

for f, g, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y)) holds

( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th25: :: LOPBAN_1:25

for X, Y being RealNormSpace

for f, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y))

for a being Real holds

( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )

for f, h being VECTOR of (R_VectorSpace_of_BoundedLinearOperators (X,Y))

for a being Real holds

( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )

proof end;

theorem Th26: :: LOPBAN_1:26

for X, Y being RealNormSpace holds 0. (R_VectorSpace_of_BoundedLinearOperators (X,Y)) = the carrier of X --> (0. Y)

proof end;

definition

let X, Y be RealNormSpace;

let f be set ;

assume A1: f in BoundedLinearOperators (X,Y) ;

coherence

f is Lipschitzian LinearOperator of X,Y by A1, Def9;

end;
let f be set ;

assume A1: f in BoundedLinearOperators (X,Y) ;

coherence

f is Lipschitzian LinearOperator of X,Y by A1, Def9;

:: deftheorem Def11 defines modetrans LOPBAN_1:def 11 :

for X, Y being RealNormSpace

for f being set st f in BoundedLinearOperators (X,Y) holds

modetrans (f,X,Y) = f;

for X, Y being RealNormSpace

for f being set st f in BoundedLinearOperators (X,Y) holds

modetrans (f,X,Y) = f;

definition

let X, Y be RealNormSpace;

let u be LinearOperator of X,Y;

{ ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } is non empty Subset of REAL

end;
let u be LinearOperator of X,Y;

func PreNorms u -> non empty Subset of REAL equals :: LOPBAN_1:def 12

{ ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;

coherence { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;

{ ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } is non empty Subset of REAL

proof end;

:: deftheorem defines PreNorms LOPBAN_1:def 12 :

for X, Y being RealNormSpace

for u being LinearOperator of X,Y holds PreNorms u = { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;

for X, Y being RealNormSpace

for u being LinearOperator of X,Y holds PreNorms u = { ||.(u . t).|| where t is VECTOR of X : ||.t.|| <= 1 } ;

theorem Th27: :: LOPBAN_1:27

for X, Y being RealNormSpace

for g being Lipschitzian LinearOperator of X,Y holds PreNorms g is bounded_above

for g being Lipschitzian LinearOperator of X,Y holds PreNorms g is bounded_above

proof end;

theorem :: LOPBAN_1:28

for X, Y being RealNormSpace

for g being LinearOperator of X,Y holds

( g is Lipschitzian iff PreNorms g is bounded_above )

for g being LinearOperator of X,Y holds

( g is Lipschitzian iff PreNorms g is bounded_above )

proof end;

definition

let X, Y be RealNormSpace;

ex b_{1} being Function of (BoundedLinearOperators (X,Y)),REAL st

for x being set st x in BoundedLinearOperators (X,Y) holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X,Y)))

for b_{1}, b_{2} being Function of (BoundedLinearOperators (X,Y)),REAL st ( for x being set st x in BoundedLinearOperators (X,Y) holds

b_{1} . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being set st x in BoundedLinearOperators (X,Y) holds

b_{2} . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) holds

b_{1} = b_{2}

end;
func BoundedLinearOperatorsNorm (X,Y) -> Function of (BoundedLinearOperators (X,Y)),REAL means :Def13: :: LOPBAN_1:def 13

for x being set st x in BoundedLinearOperators (X,Y) holds

it . x = upper_bound (PreNorms (modetrans (x,X,Y)));

existence for x being set st x in BoundedLinearOperators (X,Y) holds

it . x = upper_bound (PreNorms (modetrans (x,X,Y)));

ex b

for x being set st x in BoundedLinearOperators (X,Y) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def13 defines BoundedLinearOperatorsNorm LOPBAN_1:def 13 :

for X, Y being RealNormSpace

for b_{3} being Function of (BoundedLinearOperators (X,Y)),REAL holds

( b_{3} = BoundedLinearOperatorsNorm (X,Y) iff for x being set st x in BoundedLinearOperators (X,Y) holds

b_{3} . x = upper_bound (PreNorms (modetrans (x,X,Y))) );

for X, Y being RealNormSpace

for b

( b

b

theorem Th29: :: LOPBAN_1:29

for X, Y being RealNormSpace

for f being Lipschitzian LinearOperator of X,Y holds modetrans (f,X,Y) = f

for f being Lipschitzian LinearOperator of X,Y holds modetrans (f,X,Y) = f

proof end;

theorem Th30: :: LOPBAN_1:30

for X, Y being RealNormSpace

for f being Lipschitzian LinearOperator of X,Y holds (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)

for f being Lipschitzian LinearOperator of X,Y holds (BoundedLinearOperatorsNorm (X,Y)) . f = upper_bound (PreNorms f)

proof end;

definition

let X, Y be RealNormSpace;

NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #) is non empty NORMSTR ;

end;
func R_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty NORMSTR equals :: LOPBAN_1:def 14

NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);

coherence NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);

NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #) is non empty NORMSTR ;

:: deftheorem defines R_NormSpace_of_BoundedLinearOperators LOPBAN_1:def 14 :

for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) = NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);

for X, Y being RealNormSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) = NORMSTR(# (BoundedLinearOperators (X,Y)),(Zero_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Add_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(Mult_ ((BoundedLinearOperators (X,Y)),(R_VectorSpace_of_LinearOperators (X,Y)))),(BoundedLinearOperatorsNorm (X,Y)) #);

theorem Th31: :: LOPBAN_1:31

for X, Y being RealNormSpace holds the carrier of X --> (0. Y) = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y))

proof end;

theorem Th32: :: LOPBAN_1:32

for X, Y being RealNormSpace

for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for g being Lipschitzian LinearOperator of X,Y st g = f holds

for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||

for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for g being Lipschitzian LinearOperator of X,Y st g = f holds

for t being VECTOR of X holds ||.(g . t).|| <= ||.f.|| * ||.t.||

proof end;

theorem Th33: :: LOPBAN_1:33

for X, Y being RealNormSpace

for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.||

for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds 0 <= ||.f.||

proof end;

theorem Th34: :: LOPBAN_1:34

for X, Y being RealNormSpace

for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds

0 = ||.f.||

for f being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds

0 = ||.f.||

proof end;

registration

let X, Y be RealNormSpace;

for b_{1} being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds

( b_{1} is Function-like & b_{1} is Relation-like )
;

end;
cluster -> Relation-like Function-like for Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Y));

coherence for b

( b

definition

let X, Y be RealNormSpace;

let f be Element of (R_NormSpace_of_BoundedLinearOperators (X,Y));

let v be VECTOR of X;

:: original: .

redefine func f . v -> VECTOR of Y;

coherence

f . v is VECTOR of Y

end;
let f be Element of (R_NormSpace_of_BoundedLinearOperators (X,Y));

let v be VECTOR of X;

:: original: .

redefine func f . v -> VECTOR of Y;

coherence

f . v is VECTOR of Y

proof end;

theorem Th35: :: LOPBAN_1:35

for X, Y being RealNormSpace

for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds

( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )

for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds

( h = f + g iff for x being VECTOR of X holds h . x = (f . x) + (g . x) )

proof end;

theorem Th36: :: LOPBAN_1:36

for X, Y being RealNormSpace

for f, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a being Real holds

( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )

for f, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a being Real holds

( h = a * f iff for x being VECTOR of X holds h . x = a * (f . x) )

proof end;

theorem Th37: :: LOPBAN_1:37

for X, Y being RealNormSpace

for f, g being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

for f, g being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))

for a being Real holds

( ( ||.f.|| = 0 implies f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) ) & ( f = 0. (R_NormSpace_of_BoundedLinearOperators (X,Y)) implies ||.f.|| = 0 ) & ||.(a * f).|| = (abs a) * ||.f.|| & ||.(f + g).|| <= ||.f.|| + ||.g.|| )

proof end;

theorem Th38: :: LOPBAN_1:38

for X, Y being RealNormSpace holds

( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like )

( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like )

proof end;

registration

let X, Y be RealNormSpace;

( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like & R_NormSpace_of_BoundedLinearOperators (X,Y) is vector-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-unital & R_NormSpace_of_BoundedLinearOperators (X,Y) is Abelian & R_NormSpace_of_BoundedLinearOperators (X,Y) is add-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_zeroed & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_complementable ) by Th39;

end;
cluster R_NormSpace_of_BoundedLinearOperators (X,Y) -> non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital discerning reflexive RealNormSpace-like ;

coherence ( R_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & R_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & R_NormSpace_of_BoundedLinearOperators (X,Y) is RealNormSpace-like & R_NormSpace_of_BoundedLinearOperators (X,Y) is vector-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-distributive & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is scalar-unital & R_NormSpace_of_BoundedLinearOperators (X,Y) is Abelian & R_NormSpace_of_BoundedLinearOperators (X,Y) is add-associative & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_zeroed & R_NormSpace_of_BoundedLinearOperators (X,Y) is right_complementable ) by Th39;

theorem Th40: :: LOPBAN_1:40

for X, Y being RealNormSpace

for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds

( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )

for f, g, h being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds

( h = f - g iff for x being VECTOR of X holds h . x = (f . x) - (g . x) )

proof end;

begin

definition

let X be RealNormSpace;

end;
attr X is complete means :Def15: :: LOPBAN_1:def 15

for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds

seq is convergent ;

for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds

seq is convergent ;

:: deftheorem Def15 defines complete LOPBAN_1:def 15 :

for X being RealNormSpace holds

( X is complete iff for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds

seq is convergent );

for X being RealNormSpace holds

( X is complete iff for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds

seq is convergent );

registration

ex b_{1} being RealNormSpace st b_{1} is complete
end;

cluster non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() discerning reflexive RealNormSpace-like complete for NORMSTR ;

existence ex b

proof end;

Lm3: for e being Real

for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st

for i being Element of NAT st k <= i holds

seq . i <= e holds

lim seq <= e

proof end;

theorem Th41: :: LOPBAN_1:41

for X being RealNormSpace

for seq being sequence of X st seq is convergent holds

( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )

for seq being sequence of X st seq is convergent holds

( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )

proof end;

theorem Th42: :: LOPBAN_1:42

for X, Y being RealNormSpace st Y is complete holds

for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

for seq being sequence of (R_NormSpace_of_BoundedLinearOperators (X,Y)) st seq is Cauchy_sequence_by_Norm holds

seq is convergent

proof end;

theorem Th43: :: LOPBAN_1:43

for X being RealNormSpace

for Y being RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace

for Y being RealBanachSpace holds R_NormSpace_of_BoundedLinearOperators (X,Y) is RealBanachSpace

proof end;

registration

let X be RealNormSpace;

let Y be RealBanachSpace;

coherence

R_NormSpace_of_BoundedLinearOperators (X,Y) is complete by Th43;

end;
let Y be RealBanachSpace;

coherence

R_NormSpace_of_BoundedLinearOperators (X,Y) is complete by Th43;