isClopen_basicOpen_of_mul_add — Mathlib

English

If there exist e,f ∈ R with e f = 0 and e+f = 1, then the basic open set D(e) is clopen in Spec(R). Conversely, under these relations, D(e) is clopen.

Русский

Если существуют e,f ∈ R такие, что e f = 0 и e+f = 1, тогда D(e) — это как открытое, так и закрытое множество в спектре Spec(R).

LaTeX

$$$$ \text{IsClopen}( \operatorname{basicOpen}(e) ) $$ под условием $e f = 0$ и $e+f=1$; в обратном случае существуют такие e,f.$$

Lean4

theorem isClopen_basicOpen_of_mul_add (e f : R) (mul : e * f = 0) (add : e + f = 1) :
    IsClopen (basicOpen e : Set (PrimeSpectrum R)) :=
  ⟨basicOpen_eq_zeroLocus_of_mul_add e f mul add ▸ isClosed_zeroLocus _, (basicOpen e).2⟩

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