preimage_closedPoints_subset — Mathlib

English

If f is injective and continuous, then the preimage of the closed points of Y is contained in the closed points of X.

Русский

Если f инъективна и непрерывна, то предобраз замкнутых точек Y содержится в замкнутых точках X.

LaTeX

$$$\operatorname{Function.Injective}(f) \Rightarrow \operatorname{Continuous}(f) \Rightarrow f^{-1}(\text{closedPoints}(Y)) \subseteq \text{closedPoints}(X)$$$

Lean4

theorem preimage_closedPoints_subset (hf : Function.Injective f) (hf' : Continuous f) :
    f ⁻¹' closedPoints Y ⊆ closedPoints X := by
  intro x hx
  rw [mem_closedPoints_iff]
  convert continuous_iff_isClosed.mp hf' _ hx
  rw [← Set.image_singleton, Set.preimage_image_eq _ hf]

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