sdiff_inter_self_left

Mathlib.Data.Finset.SDiff

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

English

No additional content; see item 95808.

Русский

Нет дополнительного содержания; смотрите пункт 95808.

LaTeX

$$$ s \\setminus (t \\cap u) = (s \\setminus t) \\cup (s \\setminus u). $$$

Lean4

@[simp]
theorem sdiff_inter_self_left (s t : Finset α) : s \ (s ∩ t) = s \ t :=
  sdiff_inf_self_left _ _

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

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

Разделы

Аффилиация

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