tendsto_nhdsWithin_iff_subtype — Mathlib

English

Let s ⊆ α with a ∈ s. Then Tendsto f on nhdsWithin a s is equivalent to Tendsto f restricted to the subtype into nhds of a in the ambient space.

Русский

Пусть s ⊆ α и a ∈ s. Тогда Tendsto f (nhdsWithin a s) эквивалентно Tendsto f ограниченного до подтипа в nhds a в окружающем пространстве.

LaTeX

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

Lean4

theorem tendsto_nhdsWithin_iff_subtype {s : Set α} {a : α} (h : a ∈ s) (f : α → β) (l : Filter β) :
    Tendsto f (𝓝[s] a) l ↔ Tendsto (s.restrict f) (𝓝 ⟨a, h⟩) l := by
  rw [nhdsWithin_eq_map_subtype_coe h, tendsto_map'_iff]; rfl

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