isIdempotentElemEquivClopens_symm_sup

English

The idempotent corresponding to the union of two clopen sets is the sum minus their product of the respective idempotents: e(s1 ⊔ s2) = e(s1) + e(s2) − e(s1) e(s2).

Русский

Идемпотент, соответствующий объединению двух клозоподмножеств, равен сумме идемпотентов без их произведения: e(s1 ⊔ s2) = e(s1) + e(s2) − e(s1) e(s2).

LaTeX

$$$e(s_1 \lor s_2) = e(s_1) + e(s_2) - e(s_1) e(s_2)$$$

Lean4

theorem isIdempotentElemEquivClopens_symm_sup (s₁ s₂ : Clopens (PrimeSpectrum R)) :
    letI e := isIdempotentElemEquivClopens (R := R).symm
    e (s₁ ⊔ s₂) = ⟨_, (e s₁).2.add_sub_mul (e s₂).2⟩ :=
  map_sup ..

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