infs_compls_eq_diffs

Mathlib.Data.Finset.Sups

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

English

Set difference with a complemented set equals the infimum with the other set: s \ tᶜˢ = s ⊼ t.

Русский

Разность с комплементом: s \ tᶜˢ = s ⊼ t.

LaTeX

$$$s \\ t^{\!c_s} = s^{\!\!\sqcap} t$$$

Lean4

@[simp]
theorem infs_compls_eq_diffs (s t : Finset α) : s ⊼ tᶜˢ = s \\ t := by ext; simp [sdiff_eq]; aesop

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

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

Разделы

Аффилиация

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