package coq-mk-reals-axioms
A Coq formalization of the axiomatic definition of real numbers
Install
Dune Dependency
Authors
Maintainers
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:MKRealsPublished: 28 Aug 2024
On This Page