compls_sups — Mathlib

English

Complement of supremum equals infimum of complements: (s ⊻ t)ᶜˢ = sᶜˢ ⊼ tᶜˢ.

Русский

Комплемент супремума равен инфимума комплементов: (s ⊻ t)ᶜˢ = sᶜˢ ⊼ tᶜˢ.

LaTeX

$$$(s\!\sqcup t)^{\!c_s} = s^{\!c_s} \!\sqcap t^{\!c_s}$$$

Lean4

@[simp]
theorem compls_sups (s t : Finset α) : (s ⊻ t)ᶜˢ = sᶜˢ ⊼ tᶜˢ := by simp_rw [← image_compl];
  exact image_image₂_distrib fun _ _ ↦ compl_sup

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