Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes