mathlib3

5a3cd16b - feat(order/filter/small_sets): yet another squeeze theorem (#16286)

feat(order/filter/small_sets): yet another squeeze theorem (#16286) * Add a very general version of the squeeze theorem. * Use it to golf the proof of the usual squeeze theorem. * Add docstrings.