Machine proof of Equivalence between Axiom of Choice and Product Theorem of Standard Family Sets

Based on the computer proof assistant Coq, the establishment of a formal system of naive set theory is realized, referring to Morse-Kelley set theory. On this basis, the formal descriptions of the axiom of choice and the product theorem of standard family sets are given, and the proof code for the equivalence between axiom of choice and the product theorem of the standard set family is completed and verified in Coq. All process fully embodies that machine proof of mathematical theorem based on Coq has the characteristics of readability and interactivity.