mathlib

c14c84e4 - chore(topology/algebra/ordered): `le_of_tendsto`: use `∀ᶠ`, add primed versions (#2270)

chore(topology/algebra/ordered): `le_of_tendsto`: use `∀ᶠ`, add primed versions (#2270) Also fix two typos in `order/filter/basic` Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>