GCH蕴含AC的一个Metamath形式化
逻辑
2015-06-12 v1
摘要
我们给出了Specker关于“广义连续统假设蕴含选择公理”断言的“局部”版本的形式化，特别关注原非形式化证明中被忽略的一些额外复杂性，特别是关于“典范”构造与康托尔范式。
引用
@article{arxiv.1506.03533,
title = {GCH implies AC, a Metamath Formalization},
author = {Mario Carneiro},
journal= {arXiv preprint arXiv:1506.03533},
year = {2015}
}
备注
4 pages, submitted to FMM 2015