preimage_closedPoints — Mathlib

English

Let f: X → Y be an open embedding and Y a Jacobson space. Then the set of closed points of X is exactly the preimage under f of the closed points of Y.

Русский

Пусть f: X → Y — открытое вложение и Y — пространство Якобсона. Тогда множество замкнутых точек X совпадает с предобразом множества замкнутых точек Y под f.

LaTeX

$$$f^{-1}(\operatorname{closedPoints}(Y)) = \operatorname{closedPoints}(X)$$$

Lean4

theorem preimage_closedPoints (hf : IsOpenEmbedding f) [JacobsonSpace Y] : f ⁻¹' closedPoints Y = closedPoints X :=
  by
  apply subset_antisymm (preimage_closedPoints_subset hf.injective hf.continuous)
  intro x hx
  apply isClosed_singleton_of_isLocallyClosed_singleton
  rw [← Set.image_singleton]
  exact (hx.isLocallyClosed.image hf.isInducing hf.isOpen_range.isLocallyClosed)

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