basic): add `supr_inf_principal` and `tendsto_supr` (#9051)

Commit

4 years ago

feat(order/filter/basic): add `supr_inf_principal` and `tendsto_supr` (#9051) Also golf a few proofs

Author

urkud

Parents