mathlib
dc5f7fbf - feat(set_theory/ordinal_arithmetic): Further theorems on normal functions (#12484)

Commit

3 years ago

feat(set_theory/ordinal_arithmetic): Further theorems on normal functions (#12484) We prove various theorems giving more convenient characterizations of normal functions.

Author

vihdzp

Parents

e3ad468b

mathlib dc5f7fbf - feat(set_theory/ordinal_arithmetic): Further theorems on normal functions (#12484)

mathlib
dc5f7fbf - feat(set_theory/ordinal_arithmetic): Further theorems on normal functions (#12484)