:: NDIFF_2 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
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
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: NDIFF_2:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th3: :: NDIFF_2:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def3 defines is_Gateaux_differentiable_in NDIFF_2:def 3 :
theorem Th4: :: NDIFF_2:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def4 defines Gateaux_diff NDIFF_2:def 4 :
theorem :: NDIFF_2:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: NDIFF_2:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: NDIFF_2:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: NDIFF_2:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th9: :: NDIFF_2:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: NDIFF_2:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th11: :: NDIFF_2:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: NDIFF_2:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: NDIFF_2:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 