English
For finite sets s1 and s2, the set difference s1 \\ s2 equals the filter of s1 by functions not in s2: s1 \\ s2 = filter (· ∉ s2) s1.
Русский
Для конечных множеств s1, s2 выполняется, что s1 \\ s2 = фильтр по элементам не принадлежащим s2: s1 \\ s2 = filter (x ∉ s2) s1.
LaTeX
$$$s_1 \\ s_2 = \\operatorname{filter} (\\lambda x. x \\notin s_2)\\, s_1$$$
Lean4
theorem sdiff_eq_filter (s₁ s₂ : Finset α) : s₁ \ s₂ = filter (· ∉ s₂) s₁ := by grind