sdiff_val — Mathlib

English

For Finset s1 and s2, the underlying multiset of the difference equals the multiset difference of the underlying multisets: (s1 \\ s2).val = s1.val − s2.val.

Русский

Для конечных множеств s1 и s2, базовая мультиset-структура разности равна разности базовых мультисет: (s1 \\ s2).val = s1.val − s2.val.

LaTeX

$$$ (s_1 \\ s_2).val = s_1.\\val - s_2.\\val. $$$

Lean4

@[simp]
theorem sdiff_val (s₁ s₂ : Finset α) : (s₁ \ s₂).val = s₁.val - s₂.val :=
  rfl

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