interval_succ): new file (#14294)

Commit

3 years ago

feat(order/succ_pred/interval_succ): new file (#14294) Add 2 lemmas about `set.Ioc (f x) (f (order.succ x))`, where `f` is a monotone function.

Author

urkud

Parents