English
If X is a Jacobson space and its closed points are finite, then X carries the discrete topology.
Русский
Если X — пространство Якобсона и множество замкнутых точек X конечно, то топология X дискретна.
LaTeX
$$$ \operatorname{JacobsonSpace}(X) \land (\operatorname{closedPoints}(X)).\operatorname{Finite} \Rightarrow \operatorname{DiscreteTopology}(X) $$$
Lean4
theorem discreteTopology [JacobsonSpace X] (h : (closedPoints X).Finite) : DiscreteTopology X :=
by
have : closedPoints X = Set.univ :=
by
rw [← Set.univ_subset_iff, ← closure_closedPoints, closure_subset_iff_isClosed, ←
(closedPoints X).biUnion_of_singleton]
exact h.isClosed_biUnion fun _ ↦ id
have inst : Finite X := Set.finite_univ_iff.mp (this ▸ h)
rw [discreteTopology_iff_forall_isOpen]
intro s
rw [← isClosed_compl_iff, ← sᶜ.biUnion_of_singleton]
refine sᶜ.toFinite.isClosed_biUnion fun x _ ↦ ?_
rw [← mem_closedPoints_iff, this]
trivial
