sdiff_eq_filter — Mathlib

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

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