English
Tendsto f l to nhdsWithin a (range f) is equivalent to Tendsto f l to nhds a.
Русский
Сходимость f к a по nhdsWithin внутри диапазона значений f эквивалентна обычной сходимости к a.
LaTeX
$$$ Tendsto f l (\\mathcal{N} [range f] a) \\iff Tendsto f l (\\mathcal{N} a) $$$
Lean4
@[simp]
theorem tendsto_nhdsWithin_range {a : α} {l : Filter β} {f : β → α} : Tendsto f l (𝓝[range f] a) ↔ Tendsto f l (𝓝 a) :=
⟨fun h => h.mono_right inf_le_left, fun h =>
tendsto_inf.2 ⟨h, tendsto_principal.2 <| Eventually.of_forall mem_range_self⟩⟩