lean2/library/theories/analysis/analysis.md

10 lines
332 B
Markdown
Raw Normal View History

theories.analysis
=================
* [metric_space](metric_space.lean)
* [normed_space](normed_space.lean) : real normed spaces
* [real_limit](real_limit.lean)
* [ivt](ivt.lean) : the intermediate value theorem
* [sqrt](sqrt.lean) : the sqrt function on the reals
* [inner_product](inner_product.lean) : real inner product spaces