compl_sSup — Mathlib

English

In a complete Boolean algebra, the complement of the supremum over a set equals the infimum over the complements indexed by that set: (sSup s)ᶜ = ⨅ i ∈ s, iᶜ.

Русский

Дополнение к объединению множества равно пересечению дополнений элементов множества: (sSup s)ᶜ = ⨅ i∈s, iᶜ.

LaTeX

$$$ (\mathrm{sSup}~s)^{\complement} = \bigwedge_{i \in s} i^{\complement}. $$$

Lean4

theorem compl_sSup : (sSup s)ᶜ = ⨅ i ∈ s, iᶜ := by simp only [sSup_eq_iSup, compl_iSup]

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