of_isOpenEmbedding — Mathlib

English

If f: X → Y is an open embedding and Y is Jacobson, then X is Jacobson.

Русский

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

LaTeX

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

Lean4

theorem of_isOpenEmbedding [JacobsonSpace Y] (hf : IsOpenEmbedding 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.isOpen_range.isLocallyClosed)
  exact ⟨_, hx, hx'⟩

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