sdiff_inter_self_right

Mathlib.Data.Finset.SDiff

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

English

If a ∉ s, then a ∉ s \\ t.

Русский

Если a ∉ s, то a ∉ s \\ t.

LaTeX

$$$ a \\notin s \\Rightarrow a \\notin s \\\\ t. $$$

Lean4

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

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

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

Разделы

Аффилиация

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