sdiff_sdiff_eq_sdiff_union

Mathlib.Data.Finset.SDiff

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

English

If u ⊆ s, then s \ (t \ u) equals (s \ t) ∪ u.

Русский

Если u ⊆ s, то s \ (t \ u) равно (s \ t) ∪ u.

LaTeX

$$$ (u \subseteq s) \implies s \ (t \ u) = (s \ t) \cup u $$$

Lean4

theorem sdiff_sdiff_eq_sdiff_union (h : u ⊆ s) : s \ (t \ u) = s \ t ∪ u :=
  sdiff_sdiff_eq_sdiff_sup h

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

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

Разделы

Аффилиация

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