union_sdiff_distrib

Mathlib.Data.Finset.SDiff

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

English

For finite s1,s2,t, (s1 ∪ s2) \ t = (s1 \ t) ∪ (s2 \ t).

Русский

Для конечных s1,s2,t выполняется (s1 ∪ s2) \ t = (s1 \ t) ∪ (s2 \ t).

LaTeX

$$$ (s_1 \cup s_2) \setminus t = (s_1 \setminus t) \cup (s_2 \setminus t) $$$

Lean4

theorem union_sdiff_distrib (s₁ s₂ t : Finset α) : (s₁ ∪ s₂) \ t = s₁ \ t ∪ s₂ \ t :=
  sup_sdiff

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

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

Разделы

Аффилиация

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