inf_sup — Mathlib

English

If x,y and x',y' are complements, then their mixed inf-sup is complementary: IsCompl(x ⊓ x', y ⊔ y').

Русский

Если x,y и x',y' комплементы, то их смешанное пересечение и объединение комплементны: IsCompl(x ⊓ x', y ⊔ y').

LaTeX

$$$$ IsCompl(x,y) \rightarrow IsCompl(x',y') \rightarrow IsCompl(x \land x', y \lor y'). $$$$

Lean4

theorem inf_sup {x' y'} (h : IsCompl x y) (h' : IsCompl x' y') : IsCompl (x ⊓ x') (y ⊔ y') :=
  (h.symm.sup_inf h'.symm).symm

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