English
Let f be continuous on a neighborhood s′ of s, and suppose f maps s into t. Then the induced map between the subspace neighborhoods sends nhds-set of s to nhds-set of t; i.e. f: (s, subspace) → (t, subspace) is continuous in the sense of nhdsSet.
Русский
Пусть f непрерывна на окрестности s′ множества s, причём образ s лежит в t. Тогда отображение f между соответствующими подпространствами непрерывно в смысле множеств окрестностей nhdsSet: Tendsto f (nhdsSet s) (nhdsSet t).
LaTeX
$$$\\operatorname{Tendsto}\\ f\\ (\\mathcal{N}^{\\mathrm{set}}(s))\\ (\\mathcal{N}^{\\mathrm{set}}(t))$$$
Lean4
/-- If `f` is continuous on some neighbourhood `s'` of `s` and `f` maps `s` to `t`,
the preimage of a set neighbourhood of `t` is a set neighbourhood of `s`. -/
-- See `Continuous.tendsto_nhdsSet` for a special case.
theorem tendsto_nhdsSet {f : α → β} {s s' : Set α} {t : Set β} (hf : ContinuousOn f s') (hs' : s' ∈ 𝓝ˢ s)
(hst : MapsTo f s t) : Tendsto f (𝓝ˢ s) (𝓝ˢ t) :=
by
obtain ⟨V, hV, hsV, hVs'⟩ := mem_nhdsSet_iff_exists.mp hs'
refine ((hasBasis_nhdsSet s).tendsto_iff (hasBasis_nhdsSet t)).mpr fun U hU ↦ ⟨V ∩ f ⁻¹' U, ?_, fun _ ↦ ?_⟩
· exact ⟨(hf.mono hVs').isOpen_inter_preimage hV hU.1, subset_inter hsV (hst.mono Subset.rfl hU.2)⟩
· intro h
rw [← mem_preimage]
exact mem_of_mem_inter_right h
