@article{SUN Tian-yu:1,
author = {[SUN Tian-yu, YU Wen-sheng]},
title = {A Mechanized Proof of Equivalence Between the Axiom of Choice and Tukey’s Lemma},
publisher = {Journal of Beijing University of Posts and Telecommunications},
year = {2019},
journal = {Journal of Beijing University of Posts and Telecommunications},
volume = {42},
number = {5},
eid = {1},
pages = {1-7},
keywords = {mechanized proof;formal mathematics;axiom of choice;Tukey's lemma},
doi = https://journal.bupt.edu.cn/EN/10.13190/j.jbupt.2019-001
}