preimage_closedPoints — Mathlib

English

If f is a closed embedding, then the preimage of closedPoints of Y equals closedPoints of X.

Русский

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

LaTeX

$$$\text{IsClosedEmbedding}(f) \Rightarrow f^{-1}(\text{closedPoints}(Y)) = \text{closedPoints}(X)$$$

Lean4

theorem preimage_closedPoints (hf : IsClosedEmbedding f) : f ⁻¹' closedPoints Y = closedPoints X :=
  by
  ext x
  simp [mem_closedPoints_iff, ← Set.image_singleton, hf.isClosed_iff_image_isClosed]

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