Skip to main content

Questions tagged [coq-mathcomp-analysis]

Mathematical Components are libraries of formalized mathematics developed using the Coq proof assistant. Use this tag specifically for the analysis component.

Filter by
Sorted by
Tagged with
2 votes
1 answer

About the use of command Canonical in Coq for mantaining Record Type information

Inside the MathComp book there is the following example of use for the Canonical command: ...
Bruno Rafael's user avatar
4 votes
1 answer

How can I prove has_esp when using mathcomp.analysis?

How can I prove the following goal (which I believe to be true) using mathcomp.analysis? ...
lyfeng's user avatar
  • 167