arithmetic): Lemmas about `bsup o.succ f` on a monotone function (#14289)

Commit

3 years ago

feat(set_theory/ordinal/arithmetic): Lemmas about `bsup o.succ f` on a monotone function (#14289)

Author

vihdzp

Parents