Commit 2023-02-07 20:26 98e83c3d
View on Github →feat(set_theory/zfc/basic): define hereditarily
(#18328)
We will define von Neumann ordinals as hereditarily transitive sets in #18329. Also there are hereditarily finite sets and hereditarily countable sets in set theory.