tendsto_nhdsWithin_of_tendsto_nhds

English

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

Русский

Если f сходится к a в nhds, то f сходится к a внутри nhdsWithin a s для любого s.

LaTeX

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

Lean4

theorem tendsto_nhdsWithin_of_tendsto_nhds {f : α → β} {a : α} {s : Set α} {l : Filter β} (h : Tendsto f (𝓝 a) l) :
    Tendsto f (𝓝[s] a) l :=
  h.mono_left inf_le_left

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