:: Differentiable Functions on Normed Linear Spaces. {P}art {II}
:: by Hiroshi Imura , Yuji Sakai and Yasunari Shidama
::
:: Received June 4, 2004
:: Copyright (c) 2004 Association of Mizar Users
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 :: NDIFF_2:def 1
(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 :: NDIFF_2:def 2
(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: :: NDIFF_2:1
theorem :: NDIFF_2:2
theorem Th3: :: NDIFF_2:3
:: deftheorem Def3 defines is_Gateaux_differentiable_in NDIFF_2:def 3 :
theorem Th4: :: NDIFF_2:4
:: deftheorem Def4 defines Gateaux_diff NDIFF_2:def 4 :
theorem :: NDIFF_2:5
theorem :: NDIFF_2:6
theorem Th7: :: NDIFF_2:7
theorem :: NDIFF_2:8
theorem Th9: :: NDIFF_2:9
theorem :: NDIFF_2:10
theorem Th11: :: NDIFF_2:11
theorem Th12: :: NDIFF_2:12
theorem :: NDIFF_2:13