inter_sdiff_self

Mathlib.Data.Finset.SDiff

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

English

For Finsets s1 and s2, the intersection of s1 with s2 \\\\ s1 is empty: s1 ∩ (s2 \\ s1) = ∅.

Русский

Для конечных множеств s1 и s2 пересечение s1 с (s2 \ s1) пусто: s1 ∩ (s2 \\ s1) = ∅.

LaTeX

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

Lean4

@[simp]
theorem inter_sdiff_self (s₁ s₂ : Finset α) : s₁ ∩ (s₂ \ s₁) = ∅ := by grind

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

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

Разделы

Аффилиация

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