Non-constructive complex analysis in Coq

Author Aloïs Brunel



PDF
Thumbnail PDF

File

LIPIcs.TYPES.2011.1.pdf
  • Filesize: 368 kB
  • 15 pages

Document Identifiers

Author Details

Aloïs Brunel

Cite AsGet 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.
Keywords
  • Coq
  • winding number
  • complex analysis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail