begin
theorem DPREP010:
theorem DPREP020:
theorem DPREP030:
theorem DPREP040:
theorem DPREP050:
theorem DPREP060:
theorem DPREP070:
theorem DPREP080:
theorem DPREP090:
theorem LMBOP1:
:: deftheorem LOPBDef5 defines additive PDIFF_6:def 1 :
for n, m being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is additive iff for x, y being Element of REAL m holds IT . (x + y) = (IT . x) + (IT . y) );
:: deftheorem LOPBDef6 defines homogeneous PDIFF_6:def 2 :
for n, m being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is homogeneous iff for x being Element of REAL m
for r being Real holds IT . (r * x) = r * (IT . x) );
theorem SSS1:
theorem EQLOPBDef5:
theorem EQLOPBDef6:
theorem EQLOPBDef56:
:: deftheorem LOPBDef9 defines bounded PDIFF_6:def 3 :
for m, n being Nat
for IT being Function of (REAL m),(REAL n) holds
( IT is bounded iff ex K being Real st
( 0 <= K & ( for x being Element of REAL m holds |.(IT . x).| <= K * |.x.| ) ) );
theorem LOPBTh2581:
theorem LOPBTh255:
theorem LOPBTh258:
theorem LMBOP2:
theorem
theorem
theorem
theorem
theorem DPREP099:
theorem DPREP098:
theorem
begin
theorem DPREP1201:
theorem DPREP1202:
theorem DPREP120:
theorem
:: deftheorem FDDef1 defines is_differentiable_on PDIFF_6:def 4 :
for X being set
for n, m being non empty Element of NAT
for f being PartFunc of (REAL m),(REAL n) holds
( f is_differentiable_on X iff ( X c= dom f & ( for x being Element of REAL m st x in X holds
f | X is_differentiable_in x ) ) );
theorem EQFDDef1:
theorem
theorem
theorem