union_sdiff_symm

Mathlib.Data.Finset.SDiff

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

English

For finite sets s and t, s ∪ (t \ s) = t ∪ (s \ t).

Русский

Для конечных множеств s и t выполняется s ∪ (t \ s) = t ∪ (s \ t).

LaTeX

$$$ s \cup t \setminus s = t \cup s \setminus t $$$

Lean4

theorem union_sdiff_symm : s ∪ t \ s = t ∪ s \ t := by simp [union_comm]

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

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

Разделы

Аффилиация

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