preimage — Mathlib

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⟩

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