sdiff_inter_distrib_right

Mathlib.Data.Finset.SDiff

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

English

Distributivity of SDiff over intersection: sdiff_inter_distrib_right

Русский

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

LaTeX

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

Lean4

theorem sdiff_inter_distrib_right (s t u : Finset α) : s \ (t ∩ u) = s \ t ∪ s \ u :=
  sdiff_inf

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

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

Разделы

Аффилиация

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