The Continuum Hypothesis Implies the Existence of Non-principal Arithmetical Ultrafilters - A Coq Formal Verification.

Guowei Dou, Si Chen, Wensheng Yu, Ru Zhang

Browse the full ICFEM paper archive.