tendsto_nhds_of_tendsto_nhdsWithin

English

If f tends to nhdsWithin a s, then f tends to nhds a.

Русский

Если f сходится в nhdsWithin a s, то f сходится в nhds a.

LaTeX

$$$$ (\\\\mathrm{Tendsto}\, f \\\\ l \\\\ (\\\\nhdsWithin a s)) \\\\Rightarrow \\\\mathrm{Tendsto}\, f \\\\ l \\\\ (\\\\nhds a). $$$$

Lean4

theorem tendsto_nhds_of_tendsto_nhdsWithin {f : β → α} {a : α} {s : Set α} {l : Filter β} (h : Tendsto f l (𝓝[s] a)) :
    Tendsto f l (𝓝 a) :=
  h.mono_right nhdsWithin_le_nhds

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