compl_truncatedSup — Mathlib

English

In a Boolean algebra, the complement of truncatedSup s a equals truncatedInf of the complement of s over a’s complement.

Русский

В булевой алгебре комплемент усечённого верхнего предела равен усечённому инфу комплемента множества над комплемент a.

LaTeX

$$$\bigl( \operatorname{truncatedSup} s \, a \bigr)^{\complement} = \operatorname{truncatedInf} s^{\complement \, s} \; a^{\complement}$$$

Lean4

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

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