English
There is a canonical subtraction operation on Finset α, defined by subtracting the underlying multisets; in particular, (s \\ t).val = s.val − t.val, and the result is a Finset (with the nodup property).
Русский
Существует каноническая операция вычитания для Finset α, определённая вычитанием соответствующих мультимножеств; в частности, (s \\ t).val = s.val − t.val, и результат представляет собой Finset (с свойством без повторов).
LaTeX
$$$ (s \\ t).val = s.val - t.val. $$$
Lean4
/-- `s \ t` is the set consisting of the elements of `s` that are not in `t`. -/
instance instSDiff : SDiff (Finset α) :=
⟨fun s₁ s₂ => ⟨s₁.1 - s₂.1, nodup_of_le (Multiset.sub_le_self ..) s₁.2⟩⟩
