compls_infs

Mathlib.Data.Finset.Sups

URI: https://scilib.ai/kg/mathlib#Finset.compls_infs

English

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

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru