English
Let β be a topological ordered set with a top element ⊤. If f converges to ⊤ along a filter l and f ≤ g (pointwise), then g converges to ⊤ along l.
Русский
Пусть β — топологически упорядоченное множество с верхней границей ⊤. Если f сходится к ⊤ по фильтру l и f ≤ g (точечно), то и g сходится к ⊤ по l.
LaTeX
$$$\\forall l:\\\\ Filter\\\\ α,\\\\ \\forall f,g:\\\\ α \\to β,\\\\ (\\\\ Tendsto\\ f\\ l\\ (\\\\ nhds\\ \\top)) \\\\land (f \\le g) \\\\Rightarrow (\\\\ Tendsto\\ g\\ l\\ (\\\\ nhds\\ \\top))$$$
Lean4
theorem tendsto_nhds_top_mono' [TopologicalSpace β] [Preorder β] [OrderTop β] [OrderTopology β] {l : Filter α}
{f g : α → β} (hf : Tendsto f l (𝓝 ⊤)) (hg : f ≤ g) : Tendsto g l (𝓝 ⊤) :=
tendsto_nhds_top_mono hf (Eventually.of_forall hg)
