compls_infs_eq_diffs

Mathlib.Data.Finset.Sups

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

English

The infimum with a complement equals the set difference in the other direction: sᶜˢ ⊼ t = t \ s.

Русский

Инфикс с комплементом: sᶜˢ ⊼ t = t \ s.

LaTeX

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

Lean4

@[simp]
theorem compls_infs_eq_diffs (s t : Finset α) : sᶜˢ ⊼ t = t \\ s := by rw [infs_comm, infs_compls_eq_diffs]

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

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

Разделы

Аффилиация

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