Analysis

Content created by Louis Wasserman and Fredrik Bakke.

Created on 2025-09-03.
Last modified on 2026-04-30.

module analysis where

open import analysis.alternation-sequences-metric-abelian-groups 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.limits-of-sequences-metric-abelian-groups public
open import analysis.metric-abelian-groups public
open import analysis.metric-abelian-groups-of-uniformly-continuous-maps-into-metric-abelian-groups public
open import analysis.sequences-metric-abelian-groups public
open import analysis.series-complete-metric-abelian-groups public
open import analysis.series-metric-abelian-groups public

Recent changes

• 2026-04-30. Louis Wasserman. Break out real-analysis from analysis (#1941).
• 2026-04-02. Louis Wasserman. The product rule for derivatives (#1771).
• 2026-03-03. Louis Wasserman. The metric abelian group of uniformly continuous functions into a metric abelian group (#1870).
• 2026-02-11. Louis Wasserman. The derivative of the reciprocal function (#1779).
• 2026-02-11. Fredrik Bakke. Monotone convergence theorem for increasing sequences of reals (#1812).