English
Let f be continuous within the set f^{-1}(s) at x, and let y = f(x). If t is a neighborhood of y relative to s (i.e., t ∈ nhdsWithin y s), then the preimage f^{-1}(t) is a neighborhood of x relative to f^{-1}(s).
Русский
Пусть f непрерывна на f^{-1}(s) в точке x, и пусть y = f(x). Если t является окрестностью y относительно s (t ∈ nhdsWithin y s), тогда предобраз t под f является окрестностью x относительно f^{-1}(s).
LaTeX
$$$f^{-1}(t) \\in \\mathcal{N}_{f^{-1}(s)}(x)$, при условии $h : ContinuousWithinAt\\ f\\ (f^{-1}(s))\\ x$, $ht : t \\in \\mathcal{N}[s](y)$ и $hxy : y = f(x)$, следовательно $f^{-1}(t) \\in \\mathcal{N}_{f^{-1}(s)}(x)$.$$
Lean4
theorem preimage_mem_nhdsWithin'' {y : β} {s t : Set β} (h : ContinuousWithinAt f (f ⁻¹' s) x) (ht : t ∈ 𝓝[s] y)
(hxy : y = f x) : f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x := by
rw [hxy] at ht
exact h.preimage_mem_nhdsWithin' (nhdsWithin_mono _ (image_preimage_subset f s) ht)
