Real analysis

Content created by Louis Wasserman.

Created on 2026-04-30.
Last modified on 2026-04-30.

module real-analysis where

open import real-analysis.absolute-convergence-series-real-numbers public
open import real-analysis.addition-differentiable-real-maps-on-proper-closed-intervals-real-numbers public
open import real-analysis.comparison-test-series-real-numbers public
open import real-analysis.composition-differentiable-real-functions-on-proper-closed-intervals-real-numbers public
open import real-analysis.constructive-intermediate-value-theorem public
open import real-analysis.convergent-series-real-numbers public
open import real-analysis.differentiability-constant-real-maps-on-proper-closed-intervals-real-numbers public
open import real-analysis.differentiability-identity-map-on-proper-closed-intervals-real-numbers public
open import real-analysis.differentiability-reciprocal-function-on-positive-proper-closed-intervals-real-numbers public
open import real-analysis.differentiable-real-maps-on-proper-closed-intervals-real-numbers public
open import real-analysis.intermediate-value-theorem public
open import real-analysis.monotone-convergence-theorem-increasing-sequences-real-numbers public
open import real-analysis.multiplication-differentiable-real-functions-on-proper-closed-intervals-real-numbers public
open import real-analysis.nonnegative-series-real-numbers public
open import real-analysis.ratio-test-series-real-numbers public
open import real-analysis.scalar-multiplication-differentiable-real-maps-on-proper-closed-intervals-real-numbers public
open import real-analysis.series-real-numbers public

Recent changes