preimage — Mathlib

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⟩

Похожие утверждения