Formalization of the Equivalence among Completeness Theorems of Real Number in Coq

The formalization of mathematics based on theorem prover becomes increasingly important in mathematics and computer science, and, particularly, formalizing fundamental mathematical theories becomes especially essential. In this paper, we describe the formalization in Coq of eight very representative...

Full description

Bibliographic Details
Main Authors: Yaoshun Fu, Wensheng Yu
Format: Article
Language:English
Published: MDPI AG 2020-12-01
Series:Mathematics
Subjects:
Online Access:https://www.mdpi.com/2227-7390/9/1/38