Commit 2024-10-24 19:02 2473c832

View on Github →

feat(SetTheory/Cardinal/Basic): there exists a well-founded linear ordering of any type (#18183)

Estimated changes

added theorem exists_wellOrder