LIPIcs.TYPES.2011.1.pdf
- Filesize: 368 kB
- 15 pages
Document
Non-constructive complex analysis in Coq
Author
-
Part of:
Volume:
18th International Workshop on Types for Proofs and Programs (TYPES 2011)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution-NoDerivs 3.0 Unported license
- Publication Date: 2013-01-21
Cite As Get BibTex
Aloïs Brunel. Non-constructive complex analysis in Coq. In 18th International Workshop on Types for Proofs and Programs (TYPES 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 19, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)
https://doi.org/10.4230/LIPIcs.TYPES.2011.1
Abstract
Winding numbers are fundamental objects arising in algebraic topology, with many applications in non-constructive complex analysis. We present a formalization in Coq of the wind- ing numbers and their main properties. As an application of this development, we also give non-constructive proofs of the following theorems: the Fundamental Theorem of Algebra, the 2-dimensional Brouwer Fixed-Point theorem and the 2-dimensional Borsuk-Ulam theorem.
Subject Classification
Keywords
- Coq
- winding number
- complex analysis
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads