English
If there exists x such that Tendsto g f (nhds x), then Tendsto g f (nhds (limUnder f g)).
Русский
Если существует x, к которому g стремится по f, тогда g стремится к nhds(limUnder f g).
LaTeX
$$$\exists x, \operatorname{Tendsto} g f (\nhds x) \Rightarrow \operatorname{Tendsto} g f (\nhds(\operatorname{limUnder} f g))$$$
Lean4
/-- If `g` tends to some `𝓝 x` along `f`, then it tends to `𝓝 (Filter.limUnder f g)`. We formulate
this lemma with a `[Nonempty X]` argument of `lim` derived from `h` to make it useful for types
without a `[Nonempty X]` instance. Because of the built-in proof irrelevance, Lean will unify this
instance with any other instance. -/
theorem tendsto_nhds_limUnder {f : Filter α} {g : α → X} (h : ∃ x, Tendsto g f (𝓝 x)) :
Tendsto g f (𝓝 (@limUnder _ _ _ h.nonempty f g)) :=
le_nhds_lim h
