nonempty_inter_closedPoints — Mathlib

English

If Z is a nonempty locally closed subset of a Jacobson space X, then Z intersects the closed points nontrivially.

Русский

Если Z непустый локально закрытый подмножество пространства Джейкобсона X, то Z пересекается с замкнутыми точками не пустым множеством.

LaTeX

$$[JacobsonSpace X] {Z : Set X} (hZ : Z.Nonempty) (hZ' : IsLocallyClosed Z) : (Z ∩ closedPoints X).Nonempty$$

Lean4

theorem nonempty_inter_closedPoints [JacobsonSpace X] {Z : Set X} (hZ : Z.Nonempty) (hZ' : IsLocallyClosed Z) :
    (Z ∩ closedPoints X).Nonempty :=
  jacobsonSpace_iff_locallyClosed.mp inferInstance Z hZ hZ'

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