tendsto_nhdsWithin — Mathlib

English

Let a ∈ s. Then Tendsto f (nhdsWithin a s) l is equivalent to Tendsto (s.restrict f) (nhds ⟨a, h⟩) l.

Русский

Пусть a ∈ s. Тогда Tendsto f (nhdsWithin a s) l эквивалентно Tendsto (s.restrict f) (nhds ⟨a, h⟩) l.

LaTeX

$$$ (h : a \in s) (f) (l) \\Rightarrow (Tendsto f (\\mathcal{N} [s] a) l \\iff Tendsto (s.restrict f) (\\mathcal{N} ⟨a, h\\rangle) l) $$$

Lean4

theorem tendsto_nhdsWithin {t : Set β} (h : ContinuousWithinAt f s x) (ht : MapsTo f s t) :
    Tendsto f (𝓝[s] x) (𝓝[t] f x) :=
  tendsto_inf.2 ⟨h, tendsto_principal.2 <| mem_inf_of_right <| mem_principal.2 <| ht⟩

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