sdiff_inter_right_comm

Mathlib.Data.Finset.SDiff

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

English

SDiff and intersection satisfy a right-commutation identity: s \\ t ∩ u = (s ∩ u) \\ t.

Русский

Разность над пересечением справа от перестановок: s \\ t ∩ u = (s ∩ u) \\ t.

LaTeX

$$$ s \\setminus t \\cap u = (s \\cap u) \\setminus t. $$$

Lean4

/-- See also `Finset.inter_sdiff_assoc`. -/
theorem sdiff_inter_right_comm (s t u : Finset α) : s \ t ∩ u = (s ∩ u) \ t :=
  sdiff_inf_right_comm ..

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

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

Разделы

Аффилиация

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