mathlib3

2e9985e9 - feat(topology/algebra/order/basic): f ≤ᶠ[l] g implies limit of f ≤ limit of g (#12727)

feat(topology/algebra/order/basic): f ≤ᶠ[l] g implies limit of f ≤ limit of g (#12727) There are several implications of the form `eventually_*_of_tendsto_*`, which involve the order relationships between the limit of a function and other constants. What appears to be missing are reverse implications: If two functions are eventually ordered, then their limits respect the order. This is lemma will be used in further work on the asymptotics of squarefree numbers