compl_truncatedInf — Mathlib

English

In a Boolean algebra, the complement map commutes with truncatedInf and truncatedSup via the complement operation.

Русский

В булевой алгебре комплемент взаимосоответствует операциям truncatedInf и truncatedSup через операцию complement.

LaTeX

$$$\mathrm{compl}(\mathrm{truncatedInf}\ s\ a) = \mathrm{truncatedSup}(s^{c}\, a^{c})$$$

Lean4

@[simp]
theorem compl_truncatedInf (s : Finset α) (a : α) : (truncatedInf s a)ᶜ = truncatedSup sᶜˢ aᶜ :=
  map_truncatedInf (OrderIso.compl α) _ _

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