English
Jacobson spaces are characterized by a local-closure condition: JacobsonSpace X iff for every nonempty locally closed Z, Z ∩ closedPoints X is nonempty.
Русский
Пространства Джейкобсона характеризуются условием локального замыкания: J- пространство X эквивалентно тому, что для каждого непустого локально закрытого Z совмещение Z ∩ closedPoints X непусто.
LaTeX
$$$\operatorname{JacobsonSpace}(X) \iff \forall Z, Z.\text{Nonempty} \rightarrow \operatorname{IsLocallyClosed}(Z) \rightarrow (Z \cap \text{closedPoints}(X)).\text{Nonempty}$$$
Lean4
theorem jacobsonSpace_iff_locallyClosed :
JacobsonSpace X ↔ ∀ Z, Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty :=
by
rw [jacobsonSpace_iff]
constructor
· simp_rw [isLocallyClosed_iff_isOpen_coborder, coborder, isOpen_compl_iff, Set.nonempty_iff_ne_empty]
intro H Z hZ hZ' e
have : Z ⊆ closure Z \ Z := by
refine subset_closure.trans ?_
nth_rw 1 [← H isClosed_closure]
rw [hZ'.closure_subset_iff, Set.subset_diff, Set.disjoint_iff, Set.inter_assoc, Set.inter_comm _ Z, e]
exact ⟨Set.inter_subset_left, Set.inter_subset_right⟩
rw [Set.subset_diff, disjoint_self, Set.bot_eq_empty] at this
exact hZ this.2
· intro H Z hZ
refine subset_antisymm (hZ.closure_subset_iff.mpr Set.inter_subset_left) ?_
rw [← Set.disjoint_compl_left_iff_subset, Set.disjoint_iff_inter_eq_empty, ← Set.not_nonempty_iff_eq_empty]
intro H'
have := H _ H' (isClosed_closure.isOpen_compl.isLocallyClosed.inter hZ.isLocallyClosed)
rw [Set.nonempty_iff_ne_empty, Set.inter_assoc, ne_eq, ← Set.disjoint_iff_inter_eq_empty,
Set.disjoint_compl_left_iff_subset] at this
exact this subset_closure
