analysis
analysis copied to clipboard
math-comp
Mathematical Components compliant Analysis Library
This is in beginner's style and should heavily rewritten. It contains two files: - `hahnbanach.v` contains a new formalization of Zorn's Lemma depending of the Choice in Prop and to...
A proof of Baire and Banach-Steinhaus theorem, initiated by Theo Vignon. Waiting for [PR#183](https://github.com/math-comp/analysis/pull/183) to be merged to rebase on master.
This PR is the result of a split of the PR #187 . It defines a few standard sequences and proves a few lemmas about them, mostly as a test...
- [ ] ~~Obtain axioms from the std library~~ Keep the explicit list of additional axioms, and derive their standard consequences. - [x] Remove ugly notation for `asbool` - [x]...
countability and finiteness now share the interface of `countType` and `finType` through the coercions `countable >-> Sortclass` and `finite >-> Sortclass` e.g. `rpickle c` is replaced by `@pickle [countType of...
https://github.com/math-comp/analysis/blob/7b88928f524b16b2bbd29940bfd0ce4e69cb61d0/theories/mathcomp_extra.v#L189-L194
It would be nice to have many exercise-level facts proved in the library, which would support the consistency of our formalization. An example is that every metric space is T4...
