Hartog's theorem

Stream: Is there code for X?

[Lucas Polymeris]

Hi. Anyone knows if Hartog's theorem ( for every set $X$ there exists an ordinal $\alpha$ such that $|\alpha| \nleq |X|$) has been formalized in Lean? I haven't found anything on mathlib.

[Mario Carneiro]

It is trivialized in lean because of the axiom of choice

[Mario Carneiro]

you can use (cardinal.mk X).succ as such a cardinal

[Lucas Polymeris]

Wouldn't have any interest to have it without choice? I'm new to Lean, so I don't know if there is (as there is in set theory) a tendency to avoid choice when not strictly necesary

[Mario Carneiro]

the short answer is that there is not

[Mario Carneiro]

there is not really any space for developments that depend on LEM but not AC, as with most AC-free set theory

[Mario Carneiro]

Incidentally, metamath is a much friendlier environment for that kind of pure set theory, and there is a proof of Hartogs's theorem there

[Lucas Polymeris]

Right, yes. I'm starting to understand that here LEM kind of takes the role of choice in other places

[Reid Barton]

In Lean, choice is an axiom and used to prove LEM. So there's no way to track (using #print axioms) that a proof uses only LEM and not choice.