package coq-mk-choice-axiom-and-equivalent-propositions

The axiom of choice is an axiom about the existence of mappings in set theory. It was first proposed by Zermelo in 1904 and used to prove the well-ordering theorem. The axiom of choice plays an important role in modern mathematics and is closely related to many profound mathematical conclusions. Without the axiom of choice, it is even impossible to determine whether two sets can compare the number of elements, whether the product of non-empty sets is non-empty, whether a linear space must have a set of bases, whether a ring must have a maximal ideal, etc. The axiom of choice has multiple equivalent theorems, including Tukey lemma, Hausdorf maximum principle, Zermelo assumption, Zorn lemma, and the well-ordering theorem. The important Tychonoff product theorem in topology is a more profound application of the axiom of choice. Starting from the axiom of choice, we prove Tukey lemma, Hausdorff maximum principle, the maximum principle, Zermelo assumption, Zorn lemma, and the well-ordering theorem in turn, and then regard the axiom of choice as a theorem, which is respectively represented by Tukey lemma, Zermelo maximum principle, Zorn lemma, and the well-ordering theorem. Assumptions and the well-ordered theorem prove the axiom of choice, completing the proof of the entire cycle strategy, thus showing that the above propositions are equivalent to the axiom of choice. The manual proof process of these propositions is standard and can be found in related monographs or textbooks on topology or set theory.