sdiff_idem

Mathlib.Data.Finset.SDiff

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

English

Removing t twice from s is the same as removing it once: (s \ t) \ t = s \ t.

Русский

Удаление множества t из s дважды эквивалентно одному удалению: (s \ t) \ t = s \ t.

LaTeX

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

Lean4

theorem sdiff_idem (s t : Finset α) : (s \ t) \ t = s \ t :=
  _root_.sdiff_idem

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

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

Разделы

Аффилиация

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