English
If f tends to the top along filter l and g is eventually below f with respect to l, then g also tends to the top along l.
Русский
Если f стремится к вершине по фильтру l, а g рапространено меньше фля f по l, то g также стремится к вершине по l.
LaTeX
$$$\\text{Tendsto } f\\ l (\\mathcal{N}_{\\top}) \\land f \\leq^l g \\Rightarrow \\text{Tendsto } g\\ l (\\mathcal{N}_{\\top}).$$$
Lean4
theorem tendsto_nhds_top_mono [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α}
{f g : α → β} (hf : Tendsto f l (𝓝 ⊤)) (hg : f ≤ᶠ[l] g) : Tendsto g l (𝓝 ⊤) :=
by
simp only [nhds_top_order, tendsto_iInf, tendsto_principal] at hf ⊢
intro x hx
filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le
