compl_image_latticeClosure — Mathlib

English

Complement image commutes with lattice closure for Boolean algebras: compl '' latticeClosure s = latticeClosure (compl '' s).

Русский

Образ дополнения через замыкание по решётке совместимо с комплементарной операцией в булевой алгебре: compl '' latticeClosure s = latticeClosure (compl '' s).

LaTeX

$$$\\\\operatorname{compl} '' \\\\operatorname{latticeClosure}(s) = \\\\operatorname{latticeClosure}(\\\\operatorname{compl} '' s).$$$

Lean4

theorem compl_image_latticeClosure (s : Set α) : compl '' latticeClosure s = latticeClosure (compl '' s) :=
  image_latticeClosure' s _ compl_sup_distrib (fun _ _ => compl_inf)

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