sdiff_union_distrib

Mathlib.Data.Finset.SDiff

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

English

For finite s,t1,t2, s \ (t1 ∪ t2) = (s \ t1) ∩ (s \ t2).

Русский

Для конечных s,t1,t2: s \ (t1 ∪ t2) = (s \ t1) ∩ (s \ t2).

LaTeX

$$$ s \\setminus (t_1 \cup t_2) = (s \\setminus t_1) \cap (s \\setminus t_2) $$$

Lean4

theorem sdiff_union_distrib (s t₁ t₂ : Finset α) : s \ (t₁ ∪ t₂) = s \ t₁ ∩ (s \ t₂) :=
  sdiff_sup

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

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

Разделы

Аффилиация

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