tendsto_nhdsWithin_mono_left — Mathlib

English

If s ⊆ t and f tends to nhdsWithin t at a, then f tends to nhdsWithin s at a.

Русский

Если s ⊆ t и f сходится в nhdsWithin t в точке a, то f сходится в nhdsWithin s в точке a.

LaTeX

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

Lean4

theorem tendsto_nhdsWithin_mono_left {f : α → β} {a : α} {s t : Set α} {l : Filter β} (hst : s ⊆ t)
    (h : Tendsto f (𝓝[t] a) l) : Tendsto f (𝓝[s] a) l :=
  h.mono_left <| nhdsWithin_mono a hst

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