basicOpen_isIdempotentElemEquivClopens_symm

English

The basic open corresponding to the opposite of an idempotent element corresponds to the clopen complement under the isomorphism.

Русский

Базовый открытый, соответствующий противоположному идемпотенту, соответствует дополнению клипона через изоморфизм.

LaTeX

$$basicOpen_isIdempotentElemEquivClopens_symm : ∀ s, basicOpen (isIdempotentElemEquivClopens (R := R).symm s).1 = s.toOpens$$

Lean4

theorem basicOpen_isIdempotentElemEquivClopens_symm (s) :
    basicOpen (isIdempotentElemEquivClopens (R := R).symm s).1 = s.toOpens :=
  Opens.ext <| congr_arg (·.1) (isIdempotentElemEquivClopens.apply_symm_apply s)

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