English
Let l be a filter on α, u: α → E and v: α → 𝕜 with E a normed additive group and 𝕜 a normed field. If u = o_l(v) and v tends to some y ∈ 𝕜 along l, then u tends to 0 along l.
Русский
Пусть l — фильтр на α, u: α → E, v: α → 𝕜; если u = o_l(v) и v сходится к некоторому y ∈ 𝕜 по l, то u сходится к 0 по l.
LaTeX
$$$\\displaystyle \\text{Let } l \\text{ be a filter on } \\alpha,\\ u:\\alpha\\to E,\\ v:\\alpha\\to \\mathbb{K},\\ (E\\text{ normed additive group}),\\ (\\mathbb{K}\\text{ normed field}). \\\\ u = o_l(v) \\text{ and } v \\to y \\text{ in } \\mathbb{K} \\\\ \\Rightarrow\\ u \\to 0 \\text{ in } E.$$$
Lean4
theorem tendsto_zero_of_tendsto {α E 𝕜 : Type*} [NormedAddCommGroup E] [NormedField 𝕜] {u : α → E} {v : α → 𝕜}
{l : Filter α} {y : 𝕜} (huv : u =o[l] v) (hv : Tendsto v l (𝓝 y)) : Tendsto u l (𝓝 0) :=
by
suffices h : u =o[l] fun _x => (1 : 𝕜) by rwa [isLittleO_one_iff] at h
exact huv.trans_isBigO (hv.isBigO_one 𝕜)
