English
IsClopen s is equivalent to the existence of e,f with e f = 0, e + f = 1, and s equals the zero locus of e or the basicOpen of e depending on variant; in particular, s is a zero locus of a single element.
Русский
Неразделимое открытое и замкнутое множество s эквивалентно существованию e,f с ef=0, e+f=1 и s = zeroLocus {e} (или = basicOpen e).
LaTeX
$$$$ \IsClopen s \iff \exists e,f\in R,\ ef=0 \wedge (e+f=1) \wedge s = zeroLocus\{e\}. $$$$
Lean4
theorem isClopen_iff_mul_add {s : Set (PrimeSpectrum R)} :
IsClopen s ↔ ∃ e f : R, e * f = 0 ∧ e + f = 1 ∧ s = basicOpen e :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· have ⟨e, f, h⟩ := exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen h
exact ⟨e, f, by simp only [h, and_self]⟩
rintro ⟨e, f, mul, add, rfl⟩
exact isClopen_basicOpen_of_mul_add e f mul add
