mathlib
2a528d11 - feat(set_theory/cardinal/ordinal): Beth numbers form a normal family (#16853)

Commit
3 years ago
feat(set_theory/cardinal/ordinal): Beth numbers form a normal family (#16853) Prove `is_normal (λ o, (beth o).ord)`
Author
Parents
Loading