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