Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-21 12:09 7d61199a

View on Github →

feat(set_theory/cofinality): Basic fundamental sequences (#13326)

Estimated changes

Modified src/set_theory/cardinal/cofinality.lean

added theorem ordinal.is_fundamental_sequence_id_of_le_cof

added theorem ordinal.is_fundamental_sequence_succ

added theorem ordinal.is_fundamental_sequence_zero