exists_idempotent_basicOpen_eq_of_isClopen

English

If a clopen subset s ⊆ Spec(R) is given, there exists an idempotent e ∈ R with s = basicOpen e.

Русский

Для данной открыто-замкнутой подмножности s ⊆ Spec(R) существует идемпотентный элемент e ∈ R такой, что s = basicOpen e.

LaTeX

$$$$ \exists e \in R, \ IsIdempotentElem(e) \land s = \operatorname{basicOpen}(e). $$$$

Lean4

theorem exists_idempotent_basicOpen_eq_of_isClopen {s : Set (PrimeSpectrum R)} (hs : IsClopen s) :
    ∃ e : R, IsIdempotentElem e ∧ s = basicOpen e :=
  have ⟨e, _, mul, add, eq, _⟩ := exists_mul_eq_zero_add_eq_one_basicOpen_eq_of_isClopen hs
  ⟨e, (IsIdempotentElem.of_mul_add mul add).1, eq⟩

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