tendsto_nhdsWithin_range — Mathlib

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⟩⟩

Похожие утверждения