isClopen_iff_zeroLocus — Mathlib

English

A subset of the prime spectrum is clopen iff it is the zero locus of an idempotent element.

Русский

Подмножество спектра простых идеалов клозово тогда и только тогда, когда оно равно нулевому множеству идемпотентного элемента.

LaTeX

$$$IsClopen(S) \\iff \\exists e: R, IsIdempotentElem(e) \\land S = \\mathrm{zeroLocus}({e})$$$

Lean4

theorem isClopen_iff_zeroLocus {s : Set (PrimeSpectrum R)} :
    IsClopen s ↔ ∃ e : R, IsIdempotentElem e ∧ s = zeroLocus { e } :=
  isClopen_iff.trans <|
    ⟨fun ⟨e, he, h⟩ ↦ ⟨1 - e, he.one_sub, h.trans (basicOpen_eq_zeroLocus_of_isIdempotentElem e he)⟩, fun ⟨e, he, h⟩ ↦
      ⟨1 - e, he.one_sub, h.trans (zeroLocus_eq_basicOpen_of_isIdempotentElem e he)⟩⟩

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