English
If x,y are complements and x',y' are complements, then their mixed join-meet 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 \lor x', y \land y'). $$$$
Lean4
theorem sup_inf {x' y'} (h : IsCompl x y) (h' : IsCompl x' y') : IsCompl (x ⊔ x') (y ⊓ y') :=
of_eq
(by rw [inf_sup_right, ← inf_assoc, h.inf_eq_bot, bot_inf_eq, bot_sup_eq, inf_left_comm, h'.inf_eq_bot, inf_bot_eq])
(by
rw [sup_inf_left, sup_comm x, sup_assoc, h.sup_eq_top, sup_top_eq, top_inf_eq, sup_assoc, sup_left_comm,
h'.sup_eq_top, sup_top_eq])
