compl_compl_inf_distrib — Mathlib

English

(a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ.

Русский

(a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ.

LaTeX

$$$(a \land b)^{\complement\complement} = a^{\complement\complement} \land b^{\complement\complement}$$$

Lean4

theorem compl_compl_inf_distrib (a b : α) : (a ⊓ b)ᶜᶜ = aᶜᶜ ⊓ bᶜᶜ :=
  by
  refine ((compl_anti compl_sup_compl_le).trans (compl_sup_distrib _ _).le).antisymm ?_
  rw [le_compl_iff_disjoint_right, disjoint_assoc, disjoint_compl_compl_left_iff, disjoint_left_comm,
    disjoint_compl_compl_left_iff, ← disjoint_assoc, inf_comm]
  exact disjoint_compl_right

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