compl_image_latticeClosure_eq_of_compl_image_eq_self

English

If compl '' s = s, then compl '' latticeClosure s = latticeClosure s.

Русский

Если compl '' s = s, то compl '' latticeClosure s = latticeClosure s.

LaTeX

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

Lean4

theorem compl_image_latticeClosure_eq_of_compl_image_eq_self (hs : compl '' s = s) :
    compl '' latticeClosure s = latticeClosure s :=
  compl_image_latticeClosure s ▸ hs.symm ▸ rfl

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