@MISC{FDIFF_12.MIZ,
  AUTHOR = {Endou, Noboru},
  TITLE = {Differentiation on Interval},
  DAY = {31},
  MONTH = {March},
  YEAR = {2023},
  ADDRESS1 = {National Institute of Technology, Gifu College\\2236-2 Kamimakuwa, Motosu, Gifu, Japan},
  SECTION1 = {Preliminaries},
  SECTION2 = {Differentiation on Intervals},
  SECTION3 = {Fundamental Properties},
  SECTION4 = {One-Sided Continuity},
  SECTION5 = {Chain Rule},
  SUMMARY = {This article generalizes the differential method on intervals.
  Differentiation of real one-variable functions is introduced in Mizar \cite{FDIFF_1.abs}, but
  the differentiable interval is restricted to open intervals.
  However, when considering the relationship with integration, since integration is an operation
  on a closed interval, it would be convenient for differentiation to be able to handle derivates
  on a closed interval as well.
  Regarding differentiability on a closed interval, the right and left differentiability have
  already been formalized \cite{FDIFF_3.abs}, but they are the derivatives at the endpoints of an
  interval and not demonstrated as a differentiation over intervals.
  Therefore, in this paper, based on these results, although it is limited to real one-variable
  functions, we formalize the differentiation on arbitrary intervals and summarize them as
  various basic propositions.
  In particular, the chain rule \cite{Apostol:1969} is an important formula in relation to
  differentiation and integration.}}


