compl_sInf — Mathlib

English

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

Русский

Дополнение к наименьшему элементу множества равен верхней границе дополнений элементов множества: (sInf s)ᶜ = ⨆ i∈s, iᶜ.

LaTeX

$$$ (\mathrm{sInf}~s)^{\complement} = \bigvee_{i \in s} i^{\complement}. $$$

Lean4

theorem compl_sInf : (sInf s)ᶜ = ⨆ i ∈ s, iᶜ := by simp only [sInf_eq_iInf, compl_iInf]

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