The abstract of the Mizar article:

Real Function Differentiability

by

Konrad Raczkowski, and

Pawel Sadowski

Received June 18, 1990

MML identifier: FDIFF_1

[ Mizar article, MML identifier index ]

environ

 vocabulary PRE_TOPC, SEQ_1, PARTFUN1, SEQ_2, ORDINAL2, FUNCT_1, ARYTM_3,
      RELAT_1, SEQM_3, INCSP_1, ARYTM_1, ARYTM, RCOMP_1, BOOLE, ABSVALUE,
      PARTFUN2, FCONT_1, LATTICES, FDIFF_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, RELSET_1, PARTFUN1,
      PARTFUN2, RFUNCT_2, RCOMP_1, FCONT_1;
 constructors REAL_1, NAT_1, ABSVALUE, SEQ_2, SEQM_3, PARTFUN1, PARTFUN2,
      RFUNCT_2, RCOMP_1, FCONT_1, MEMBERED, XBOOLE_0;
 clusters RCOMP_1, RELSET_1, XREAL_0, SEQ_1, NAT_1, MEMBERED, ZFMISC_1,
      XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin
reserve y,X for set;
reserve x,x0,x1,x2,g,g1,g2,r,r1,s,p,p1,p2 for Real;
reserve n,m,k for Nat;
reserve Y for Subset of REAL;
reserve Z for open Subset of REAL;
reserve s1,s2,s3 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL,REAL;

theorem :: FDIFF_1:1
(for r holds r in Y iff r in REAL) iff Y=REAL;

definition let IT be Real_Sequence;
attr IT is convergent_to_0 means
:: FDIFF_1:def 1
IT is_not_0 & IT is convergent & lim IT = 0;
end;

definition
cluster convergent_to_0 Real_Sequence;
end;

definition
 cluster constant Real_Sequence;
end;

reserve h for convergent_to_0 Real_Sequence;
reserve c for constant Real_Sequence;

definition
let IT be PartFunc of REAL,REAL;
 canceled;

attr IT is REST-like means
:: FDIFF_1:def 3
IT is total &
for h holds (h")(#)(IT*h) is convergent & lim ((h")(#)(IT*h)) = 0;
end;

definition
cluster REST-like PartFunc of REAL,REAL;
end;

definition
  mode REST is REST-like PartFunc of REAL,REAL;
end;

definition let IT be PartFunc of REAL,REAL;
  attr IT is linear means
:: FDIFF_1:def 4
  IT is total & ex r st for p holds IT.p = r*p;
end;

definition
cluster linear PartFunc of REAL,REAL;
end;

definition
mode LINEAR is linear PartFunc of REAL,REAL;
end;

reserve R,R1,R2 for REST;
reserve L,L1,L2 for LINEAR;

canceled 4;

theorem :: FDIFF_1:6
for L1,L2 holds L1+L2 is LINEAR & L1-L2 is LINEAR;

theorem :: FDIFF_1:7
for r,L holds r(#)L is LINEAR;

theorem :: FDIFF_1:8
for R1,R2 holds R1+R2 is REST & R1-R2 is REST & R1(#)R2 is REST;

theorem :: FDIFF_1:9
for r,R holds r(#)R is REST;

theorem :: FDIFF_1:10
L1(#)L2 is REST-like;

theorem :: FDIFF_1:11
R(#)L is REST & L(#)R is REST;

definition let f; let x0 be real number;
pred f is_differentiable_in x0 means
:: FDIFF_1:def 5
ex N being Neighbourhood of x0 st N c= dom f &
ex L,R st for x st x in N holds f.x - f.x0 = L.(x-x0) + R.(x-x0);
end;

definition let f; let x0 be real number;
assume  f is_differentiable_in x0;
func diff(f,x0) -> Real means
:: FDIFF_1:def 6
ex N being Neighbourhood of x0 st N c= dom f &
ex L,R st it=L.1 & for x st x in N holds f.x-f.x0 = L.(x-x0) + R.(x-x0);
end;

definition let f,X;
 pred f is_differentiable_on X means
:: FDIFF_1:def 7
 X c=dom f & for x st x in X holds f|X is_differentiable_in x;
end;

canceled 3;

theorem :: FDIFF_1:15
f is_differentiable_on X implies X is Subset of REAL;

theorem :: FDIFF_1:16
f is_differentiable_on Z iff
Z c=dom f & for x st x in Z holds f is_differentiable_in x;

theorem :: FDIFF_1:17
  f is_differentiable_on Y implies Y is open;

definition let f,X;
 assume  f is_differentiable_on X;
 func f`|X -> PartFunc of REAL,REAL means
:: FDIFF_1:def 8
 dom it = X & for x st x in X holds it.x = diff(f,x);
end;

canceled;

theorem :: FDIFF_1:19
  for f,Z st Z c= dom f & ex r st rng f = {r} holds
f is_differentiable_on Z & for x st x in Z holds (f`|Z).x = 0;

definition let h,n;
 cluster h^\n -> convergent_to_0;
end;

definition let c,n;
 cluster c^\n -> constant;
end;

theorem :: FDIFF_1:20
for x0 being real number for N being Neighbourhood of x0 st
f is_differentiable_in x0 &
N c= dom f holds
for h,c st rng c = {x0} & rng (h+c) c= N holds
h"(#)(f*(h+c) - f*c) is convergent & diff(f,x0) = lim (h"(#)(f*(h+c) - f*c));

theorem :: FDIFF_1:21
for f1,f2,x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0
holds f1+f2 is_differentiable_in x0 & diff(f1+f2,x0)=diff(f1,x0)+diff(f2,x0);

theorem :: FDIFF_1:22
for f1,f2,x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0
holds f1-f2 is_differentiable_in x0 & diff(f1-f2,x0)=diff(f1,x0)-diff(f2,x0);

theorem :: FDIFF_1:23
for r,f,x0 st f is_differentiable_in x0 holds
r(#)f is_differentiable_in x0 & diff((r(#)f),x0) = r*diff(f,x0);

theorem :: FDIFF_1:24
for f1,f2,x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
f1(#)f2 is_differentiable_in x0 &
diff(f1(#)f2,x0)=(f2.x0)*diff(f1,x0)+(f1.x0)*diff(f2,x0);

theorem :: FDIFF_1:25
  for f,Z st Z c= dom f & f|Z = id Z holds
f is_differentiable_on Z & for x st x in Z holds (f`|Z).x = 1;

theorem :: FDIFF_1:26
  for f1,f2,Z st Z c= dom (f1+f2) & f1 is_differentiable_on Z &
f2 is_differentiable_on Z holds f1+f2 is_differentiable_on Z &
for x st x in Z holds ((f1+f2)`|Z).x = diff(f1,x) + diff(f2,x);

theorem :: FDIFF_1:27
  for f1,f2,Z st Z c= dom (f1-f2) & f1 is_differentiable_on Z &
f2 is_differentiable_on Z holds f1-f2 is_differentiable_on Z &
for x st x in Z holds ((f1-f2)`|Z).x = diff(f1,x) - diff(f2,x);

theorem :: FDIFF_1:28
  for r,f,Z st Z c= dom (r(#)f) & f is_differentiable_on Z holds
r(#)f is_differentiable_on Z & for x st x in Z holds ((r(#)
f)`|Z).x =r*diff(f,x);

theorem :: FDIFF_1:29
  for f1,f2,Z st Z c= dom (f1(#)f2) & f1 is_differentiable_on Z &
f2 is_differentiable_on Z holds f1(#)f2 is_differentiable_on Z &
for x st x in Z holds ((f1(#)f2)`|Z).x = (f2.x)*diff(f1,x) + (f1.x)*diff(f2,x);

theorem :: FDIFF_1:30
  Z c= dom f & f is_constant_on Z implies
f is_differentiable_on Z & for x st x in Z holds (f`|Z).x = 0;

theorem :: FDIFF_1:31
  Z c= dom f & (for x st x in Z holds f.x = r*x + p) implies
f is_differentiable_on Z & for x st x in Z holds (f`|Z).x = r;

theorem :: FDIFF_1:32
for x0 being real number holds
 f is_differentiable_in x0 implies f is_continuous_in x0;

theorem :: FDIFF_1:33
  f is_differentiable_on X implies f is_continuous_on X;

theorem :: FDIFF_1:34
  f is_differentiable_on X & Z c= X implies f is_differentiable_on Z;

theorem :: FDIFF_1:35
  f is_differentiable_in x0 implies ex R st R.0=0 & R is_continuous_in 0;