inter_sdiff_assoc

Mathlib.Data.Finset.SDiff

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

English

The intersection distributes over SDiff: (s ∩ t) \\ u = s ∩ (t \\ u).

Русский

Пересечение распределяется над разностью: (s ∩ t) \\ u = s ∩ (t \\ u).

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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