closure_closedPoints — Mathlib

English

In a Jacobson space, the closure of the set of closed points is the whole space.

Русский

В пространстве Джейкобсона замыкание множества замкнутых точек — это вся пространство.

LaTeX

$$$\text{closure}(\text{closedPoints}(X)) = \mathrm{Set.univ} \quad [\text{JacobsonSpace } X]$$$

Lean4

theorem closure_closedPoints [JacobsonSpace X] : closure (closedPoints X) = Set.univ := by
  simpa using closure_inter_closedPoints isClosed_univ

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