toEnumFinset_filter_eq — Mathlib

English

For any a, the subset of m.toEnumFinset consisting of elements with first component a equals a singleton paired with a finite range according to the multiplicity of a in m.

Русский

Для любого a множество {x ∈ m.toEnumFinset | x.1 = a} равно {a} ×ˢ Finset.range(count a m).

LaTeX

$${x ∈ m.toEnumFinset | x.1 = a} = { a } ×ˢ Finset.range (m.count a)$$

Lean4

@[simp]
theorem toEnumFinset_filter_eq (m : Multiset α) (a : α) :
    {x ∈ m.toEnumFinset | x.1 = a} = { a } ×ˢ Finset.range (m.count a) := by aesop

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