Commit 2024-09-24 06:31 643916d1

chore(SetTheory/Cardinal/Basic): organize file (#16359) This PR moves related theorems together, and adds captions for each section. Superfluous section, open, universe and variable are deleted. We also move the proof of the well-ordering theorem from the Ordinal/Basic file to here, where it makes more sense and can be potentially used to prove other basic results. This has the nice effect of removing a bunch of imports to the file. No theorem statements were modified, aside from the very minor change of correcting ∀ to Π in prod and mk_pi.