union_sdiff_cancel_left

Mathlib.Data.Finset.SDiff

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

English

If s and t are disjoint, then (s ∪ t) \ s = t.

Русский

Если s и t дизъюнктны, то (s ∪ t) \ s = t.

LaTeX

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

Lean4

theorem union_sdiff_cancel_left (h : Disjoint s t) : (s ∪ t) \ s = t :=
  h.sup_sdiff_cancel_left

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

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

Разделы

Аффилиация

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