isIdempotentElemEquivClopens_symm_compl

English

Under the same correspondence, the idempotent element associated to the complement of a clopen set is 1 minus the idempotent associated to the set.

Русский

При той же корреляции идемпотент, соответствующий дополнению клозопадного множества, равен 1 минус идемпотент, соответствующий самому множеству.

LaTeX

$$$e(s^{c}) = 1 - e(s)$$$

Lean4

theorem isIdempotentElemEquivClopens_symm_compl (s : Clopens (PrimeSpectrum R)) :
    isIdempotentElemEquivClopens.symm sᶜ = ⟨_, (isIdempotentElemEquivClopens.symm s).2.one_sub⟩ :=
  map_compl ..

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