/dedekind-reals

A formalization of the Dedekind reals in Coq

Primary LanguageCoq

A formalization of the Dedekind real numbers in Coq.

Structure of the modules:

  • MiscLemmas: various lemmas about rational number
  • Cut: definition of Dedekind cuts and several other basic notions
  • Additive: Additive structure of the reals
  • Multiplication : Multiplicative structure of the relas
  • Order : The order on the reals
  • Archimedean: the proof that the reals satisfy the archimedean property
  • Completeness: the reals are Dedekind-complete