feat(topology/algebra/order/basic): f ≤ᶠ[l] g implies limit of f ≤ li…

…mit 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

src/topology/algebra/order/basic.lean

@@ -163,6 +163,8 @@ have tendsto (λb, (f b, g b)) b (𝓝 (a₁, a₂)),
 show (a₁, a₂) ∈ {p:α×α | p.1 ≤ p.2},
   from t.is_closed_le'.mem_of_tendsto this h
 
+alias le_of_tendsto_of_tendsto ← tendsto_le_of_eventually_le
+
 lemma le_of_tendsto_of_tendsto' {f g : β → α} {b : filter β} {a₁ a₂ : α} [ne_bot b]
   (hf : tendsto f b (𝓝 a₁)) (hg : tendsto g b (𝓝 a₂)) (h : ∀ x, f x ≤ g x) :
   a₁ ≤ a₂ :=