Showing math.LOShow all
2 papers · 1 filter
math.LO2026
Formalization of Filter-Method Construction for Real Numbers in Coq
Guowei Dou, Wensheng Yu
This paper presents a formalization for a theory of constructing real numbers using concepts related to filters. The formalization is implemented using the Coq proof assistant and…
math.LO2024
Formalization of the Filter Extension Principle (FEP) in Coq
Guowei Dou, Wensheng Yu
The Filter Extension Principle (FEP) asserts that every filter can be extended to an ultrafilter, which plays a crucial role in the quest for non-principal ultrafilters. Non-princi…