Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-19 12:23 0df19987

View on Github →

doc(set_theory/*): more documentation about cardinals and ordinals (#6247)

Estimated changes

Modified src/set_theory/cardinal.lean

added theorem cardinal.le_def

Modified src/set_theory/cardinal_ordinal.lean

Modified src/set_theory/cofinality.lean

Modified src/set_theory/ordinal.lean

Modified src/set_theory/ordinal_arithmetic.lean

Modified src/set_theory/ordinal_notation.lean