Analysis

Content created by Louis Wasserman.

Created on 2025-09-03.
Last modified on 2025-11-21.

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

Recent changes

• 2025-11-21. Louis Wasserman. Derivatives of real functions defined on proper closed intervals (#1680).
• 2025-09-03. Louis Wasserman. Series in metric abelian groups (#1528).