isIdempotentElemEquivClopens_one_sub

English

Under the equivalence, the image of the complement corresponds to the complement of the image; i.e., one_sub maps to the complement on clopens.

Русский

При отображении через эквивалентность образ дополнения соответствует дополнению образа.

LaTeX

$$isIdempotentElemEquivClopens_one_sub : ∀ e, isIdempotentElemEquivClopens ⟨_, e.2.one_sub⟩ = (isIdempotentElemEquivClopens e)ᶜ$$

Lean4

theorem isIdempotentElemEquivClopens_one_sub (e : {e : R | IsIdempotentElem e}) :
    isIdempotentElemEquivClopens ⟨_, e.2.one_sub⟩ = (isIdempotentElemEquivClopens e)ᶜ :=
  map_compl ..

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