TY - Journal of Beijing University of Posts and Telecommunications A1 - SUN Tian-yu, YU Wen-sheng T1 - A Mechanized Proof of Equivalence Between the Axiom of Choice and Tukey’s Lemma Y1 - 2019-11-25 00:00:00.0 JF - Journal of Beijing University of Posts and Telecommunications JO - Journal of Beijing University of Posts and Telecommunications SP - 1 EP - 7 VL - 42 IS - 5 UR - {https://journal.bupt.edu.cn/EN/10.13190/j.jbupt.2019-001} N1 - 10.13190/j.jbupt.2019-001 ER -