English
If s is locally closed in Y and f: X → Y is continuous, then f^{-1}(s) is locally closed in X.
Русский
Если s локально замкнуто в Y и f: X → Y непрерывно, то предобраз f^{-1}(s) локально замкнут в X.
LaTeX
$$$\text{IsLocallyClosed}(s) \Rightarrow \text{IsLocallyClosed}(f^{-1}(s))$ (for continuous f)$$
Lean4
theorem preimage {s : Set Y} (hs : IsLocallyClosed s) {f : X → Y} (hf : Continuous f) : IsLocallyClosed (f ⁻¹' s) :=
by
obtain ⟨U, Z, hU, hZ, rfl⟩ := hs
exact ⟨_, _, hU.preimage hf, hZ.preimage hf, preimage_inter⟩