sdiff_union_self_eq_union

Mathlib.Data.Finset.SDiff

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

English

The union of a difference with the other set on the left yields the same union: s \\ t ∪ t = s ∪ t.

Русский

Объединение разности слева с другим множеством даёт то же множество: s \\ t ∪ t = s ∪ t.

LaTeX

$$$ (s \\ t) \\cup t = s \\cup t. $$$

Lean4

@[simp]
theorem sdiff_union_self_eq_union : s \ t ∪ t = s ∪ t :=
  sup_sdiff_self_left _ _

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

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

Разделы

Аффилиация

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