English
If x specializes to y and f has ContinuousWithinAt on s at y, and x ∈ s, then f(x) specializes to f(y).
Русский
Если x специализируется на y, и f имеет непрерывность внутри s в y, и x ∈ s, тогда f(x) специализируется на f(y).
LaTeX
$$$$\forall X\ [\text{TopologicalSpace } X],\ \forall Y, {x,y:X}, {s:Set X},\ x\rightsquigarrow y \rightarrow ContinuousWithinAt\ f\ s\ y \rightarrow x\in s \rightarrow f\,x\rightsquigarrow f\,y.$$$$
Lean4
theorem map_of_continuousWithinAt {s : Set X} (h : x ⤳ y) (hf : ContinuousWithinAt f s y) (hx : x ∈ s) : f x ⤳ f y :=
by
rw [specializes_iff_pure] at h ⊢
calc
pure (f x)
_ = map f (pure x) := (map_pure f x).symm
_ ≤ map f (𝓝 y ⊓ 𝓟 s) := (map_mono (le_inf h ((pure_le_principal x).mpr hx)))
_ = map f (𝓝[s] y) := rfl
_ ≤ _ := hf.tendsto
