sdiff_inter_self

Mathlib.Data.Finset.SDiff

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

English

The SDiff of a set with another is disjoint after intersection: (s2 \\ s1) ∩ s1 = ∅.

Русский

Разность множества с другим после пересечения даёт пустое множество: (s2 \\ s1) ∩ s1 = ∅.

LaTeX

$$$ (s_2 \\ s_1) \\cap s_1 = \\emptyset. $$$

Lean4

@[simp]
theorem sdiff_inter_self (s₁ s₂ : Finset α) : s₂ \ s₁ ∩ s₁ = ∅ :=
  inf_sdiff_self_left

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

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

Разделы

Аффилиация

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