basic): add `is_greatest_univ_iff` etc (#18162)

Commit

3 years ago

feat(order/bounds/basic): add `is_greatest_univ_iff` etc (#18162) Also add `ae_measurable_const'` and golf 2 proofs.

Author

urkud

Parents