English
Let β be a topological ordered set with a bottom element ⊥. If f tends to ⊥ along a filter l and g is eventually below f along l (g ≤ᶠ[l] f), then g also tends to ⊥ along l.
Русский
Пусть β — топологически упорядоченное множество с наименьшим элементом ⊥. Если функция f стремится к ⊥ по фильтру l и функция g в конце концов меньше или равна f по l (g ≤ᶠ[l] f), то и g стремится к ⊥ по l.
LaTeX
$$$\\forall l:\\\\ Filter\\\\ α,\\\\ \\forall f,g:\\\\ α \\to β,\\\\ (\\\\ Tendsto\quad f\\ l\\ (\\\\ nhds\\ (\\\\ bot))) \\\\Rightarrow (g \\le^l f) \\\\Rightarrow (\\\\ Tendsto\\ g\\ l\\ (\\\\ nhds\\ (\\\\ bot)))$$$
Lean4
theorem tendsto_nhds_bot_mono [TopologicalSpace β] [Preorder β] [OrderBot β] [OrderTopology β] {l : Filter α}
{f g : α → β} (hf : Tendsto f l (𝓝 ⊥)) (hg : g ≤ᶠ[l] f) : Tendsto g l (𝓝 ⊥) :=
tendsto_nhds_top_mono (β := βᵒᵈ) hf hg
