13 search results for "tag:"category:Mathematics/Real Calculus and Topology""
Showing 1 - 13
-
coq-actuary
No documentation
Formalization of actuarial mathematics in Coq2.6MITUsed by 0 other packages11 Nov 2023 -
coq-coqtail
No documentation
Library of mathematical theoremstools proved inside the Coq8.20LGPL-3.0-onlyUsed by 0 other packages14 Jul 2024 -
coq-coquelicot
No documentation
A Coq formalization of real analysis compatible with the stard library3.4.3LGPL-3.0-or-laterUsed by 7 other packages27 Jan 2025 -
coq-corn
No documentation
The Coq Constructive Repository at Nijmegen8.20.0GPL-2.0Used by 0 other packages01 Feb 2025 -
coq-fourcolor-reals
No documentation
Interface for real numbers used in the Four Color Theorem1.4.0CECILL-BUsed by 2 other packages15 Nov 2024 -
coq-hol-light
No documentation
HOL-Light library in Coqlogpath:HOLLight date:2025-01-20 category:Math/Arith/Misc category:Math/Arith/Real Numbers category:Math/Real Numbers category:Mathematics/Real Topology keyword:HOL-Light keyword:list keyword:basic set theory keyword:arithmetic keyword:integer keyword:real keyword:complex keyword:permutation keyword:group keyword:matroid keyword:binomial keyword:topology keyword:metric keyword:space keyword:analysis keyword:homology keyword:vector keyword:linear keyword:algebra keyword:convex keyword:path keyword:polytope keyword:Brouwer keyword:degree keyword:derivative keyword:Clifford keyword:integration keyword:measure keyword:Lebesgue keyword:transcendental3.0.0CeCILL-2.1Used by 0 other packages21 Jan 2025 -
coq-improper-integrals
No documentation
Additions to the coquelicot library for hling improper integrals0.1.0MITUsed by 0 other packages19 Apr 2018 -
coq-interval
No documentation
A Coq tactic for proving bounds on real-valued expressions automaticallykeyword:interval arithmetic keyword:decision procedure keyword:floating-point arithmetic keyword:reflexive tactic keyword:Taylor models category:Mathematics/Real Topology category:Computer Science/Decision Procedures Certified Algorithms/Decision procedures logpath:Interval date:2024-10-214.11.1CeCILL-CUsed by 7 other packages22 Oct 2024 -
coq-mathcomp-analysis
No documentation
An analysis library for mathematical componentscategory:Mathematics/Real Topology keyword:analysis keyword:Cantor keyword:topology keyword:real numbers keyword:sequence keyword:convexity keyword:L au notation keyword:logarithm keyword:sin keyword:cos keyword:tangent keyword:trigonometric function keyword:exponential keyword:differentiation keyword:derivative keyword:measure theory keyword:integration keyword:Lebesgue keyword:probability logpath:mathcomp.analysis1.9.0CECILL-CUsed by 7 other packages20 Feb 2025 -
coq-num-analysis
No documentation
Numerical Analysis in Coq1.0.0LGPL-3.0-or-laterUsed by 0 other packages06 Sep 2022 -
coq-pi-agm
No documentation
Computing thouss or millions of digits of PI with arithmetic-geometric means1.2.8CECILL-BUsed by 0 other packages20 Jun 2024 -
coq-quantumlib
No documentation
Coq library for reasoning about quantum programs1.6.0MITUsed by 0 other packages20 Jan 2025 -
coq-topology
No documentation
General topology in Coq10.2.0LGPL-2.1-or-laterUsed by 0 other packages21 Aug 2023