Theorem Ordinal.epsilon_add_one_eq_nfp

Modification history

2026-08-20 14:33
Mathlib/SetTheory/Ordinal/Veblen.lean
chore(SetTheory/Ordinal): execute deprecation TODOs (#40725) …
Added Ordinal.epsilon_add_one_eq_nfpView on Github →