begin
definition
let X,
Y,
Z be
RealNormSpace;
let f be
Element of
BoundedLinearOperators X,
Y;
let g be
Element of
BoundedLinearOperators Y,
Z;
func g * f -> Element of
BoundedLinearOperators X,
Z equals
(modetrans g,Y,Z) * (modetrans f,X,Y);
correctness
coherence
(modetrans g,Y,Z) * (modetrans f,X,Y) is Element of BoundedLinearOperators X,Z;
end;
:: deftheorem defines * NDIFF_2:def 1 :
definition
let X,
Y,
Z be
RealNormSpace;
let f be
Point of
(R_NormSpace_of_BoundedLinearOperators X,Y);
let g be
Point of
(R_NormSpace_of_BoundedLinearOperators Y,Z);
func g * f -> Point of
(R_NormSpace_of_BoundedLinearOperators X,Z) equals
(modetrans g,Y,Z) * (modetrans f,X,Y);
correctness
coherence
(modetrans g,Y,Z) * (modetrans f,X,Y) is Point of (R_NormSpace_of_BoundedLinearOperators X,Z);
end;
:: deftheorem defines * NDIFF_2:def 2 :
theorem Th1:
theorem
theorem Th3:
:: deftheorem Def3 defines is_Gateaux_differentiable_in NDIFF_2:def 3 :
theorem Th4:
:: deftheorem Def4 defines Gateaux_diff NDIFF_2:def 4 :
theorem
theorem
theorem Th7:
theorem
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem