of_isClosedEmbedding — Mathlib

English

If f: X → Y is a closed embedding and Y is Jacobson, then X is Jacobson.

Русский

Если f: X → Y — замкнутое вложение и Y — пространство Якобсона, то X тоже является пространством Якобсона.

LaTeX

$$$ \operatorname{IsClosedEmbedding}(f) \land \operatorname{JacobsonSpace}(Y) \Rightarrow \operatorname{JacobsonSpace}(X) $$$

Lean4

theorem of_isClosedEmbedding [JacobsonSpace Y] (hf : IsClosedEmbedding f) : JacobsonSpace X :=
  by
  rw [jacobsonSpace_iff_locallyClosed, ← hf.preimage_closedPoints]
  intro Z hZ hZ'
  obtain ⟨_, ⟨x, hx, rfl⟩, hx'⟩ :=
    nonempty_inter_closedPoints (hZ.image f) (hZ'.image hf.isInducing hf.isClosed_range.isLocallyClosed)
  exact ⟨_, hx, hx'⟩

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