tendsto_nhdsWithin_mono_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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