sdiff_sdiff_self_left

Mathlib.Data.Finset.SDiff

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

English

For any finite sets s and t, s \ (s \ t) equals s ∩ t.

Русский

Для любых конечных множеств s и t верно, что s \ (s \ t) = s ∩ t.

LaTeX

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

Lean4

theorem sdiff_sdiff_self_left (s t : Finset α) : s \ (s \ t) = s ∩ t :=
  sdiff_sdiff_right_self

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

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

Разделы

Аффилиация

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