package coq-mk-reals-axioms

  1. Overview
  2. No Docs
A Coq formalization of the axiomatic definition of real numbers

Install

Dune Dependency

github.com Edit opam file Versions (1)

Authors

  1. W
    Wensheng Yu
  2. D
    Dakai Guo
  3. S
    Si Chen
  4. G
    Guowei Dou
  5. S
    Shukun Len

Maintainers

  1. D
    dgw@bupt.edu.cn

Sources

v1.0.0.tar.gz
sha512=1ac72d176ed3f52f8ff3eca2adcbfde5b5795af506188dc031870c3f382e35ae665368ac6235d4493113154cdec8d90f25636d9d6b01ec8feaa14099295c1a70

Description

This repository presents a Coq formalization of the axiomatic definition of real numbers, guided by the 2nd chapter of Zorich's Mathematical Analysis (Part I, 7th expanded edition) and based on the formalization of Morse-Kelley (MK) set theory. In this work, the key algebraic properties and the uniqueness of real number structure are verified.

Tags

keyword:set theory keyword:Morse-Kelley keyword:MK real numbers category:Mathematics/Logic/Set theory date:2024-08-22 logpath:MKReals

Published: 28 Aug 2024

Dependencies (1)

  1. coq >= "8.13.2" & < "8.21~"

Dev Dependencies

None

Used by

None

Conflicts

None