Derivatives of real functions defined on proper closed intervals

src/analysis.lagda.md

@@ -4,6 +4,7 @@
 module analysis where
 
 open import analysis.convergent-series-metric-abelian-groups public
+open import analysis.derivatives-of-real-functions-on-proper-closed-intervals public
 open import analysis.metric-abelian-groups public
 open import analysis.series-metric-abelian-groups public
 ```