isClosed_singleton_of_isLocallyClosed_singleton

English

In a Jacobson space, if {x} is locally closed, then {x} is closed.

Русский

В пространстве Джейкобсона, если множество {x} локально закрыто, то оно замкнуто.

LaTeX

$$$\text{IsLocallyClosed}(\{x\}) \Rightarrow \text{IsClosed}(\{x\}) \quad [\text{JacobsonSpace } X]$$$

Lean4

theorem isClosed_singleton_of_isLocallyClosed_singleton [JacobsonSpace X] {x : X} (hx : IsLocallyClosed { x }) :
    IsClosed { x } :=
  by
  obtain ⟨_, ⟨y, rfl : y = x, rfl⟩, hy'⟩ := nonempty_inter_closedPoints (Set.singleton_nonempty x) hx
  exact hy'

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