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 :
:: deftheorem LOPBDef6 defines homogeneous PDIFF_6:def 2 :
theorem SSS1:
theorem EQLOPBDef5:
theorem EQLOPBDef6:
theorem EQLOPBDef56:
:: deftheorem LOPBDef9 defines bounded PDIFF_6:def 3 :
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 :
theorem EQFDDef1:
theorem
theorem
theorem