Analysis

Content created by Louis Wasserman.

Created on 2025-09-03.
Last modified on 2025-12-03.

module analysis where

open import analysis.additive-complete-metric-abelian-groups-real-banach-spaces public
open import analysis.complete-metric-abelian-groups public
open import analysis.convergent-series-complete-metric-abelian-groups public
open import analysis.convergent-series-metric-abelian-groups public
open import analysis.convergent-series-real-banach-spaces public
open import analysis.convergent-series-real-numbers public
open import analysis.derivatives-of-real-functions-on-proper-closed-intervals public
open import analysis.metric-abelian-groups public
open import analysis.metric-abelian-groups-normed-real-vector-spaces public
open import analysis.series-complete-metric-abelian-groups public
open import analysis.series-metric-abelian-groups public
open import analysis.series-real-banach-spaces public
open import analysis.series-real-numbers public

Recent changes

• 2025-12-03. Louis Wasserman. Series in Banach spaces (#1710).
• 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).