English
If s and t are separated in X and f: X → Y is continuous, then the preimages f^{-1}(s) and f^{-1}(t) are separated in X.
Русский
Если s и t разделены в X и f: X → Y непрерывна, то их прообраза f^{-1}(s) и f^{-1}(t) разделены в X.
LaTeX
$$$ \mathrm{SeparatedNhds}(s,t) \to \mathrm{Continuous}(f) \to \mathrm{SeparatedNhds}(f^{-1}(s), f^{-1}(t)) $$$
Lean4
theorem preimage [TopologicalSpace Y] {f : X → Y} {s t : Set Y} (h : SeparatedNhds s t) (hf : Continuous f) :
SeparatedNhds (f ⁻¹' s) (f ⁻¹' t) :=
let ⟨U, V, oU, oV, sU, tV, UV⟩ := h
⟨f ⁻¹' U, f ⁻¹' V, oU.preimage hf, oV.preimage hf, preimage_mono sU, preimage_mono tV, UV.preimage f⟩