mem_lists_iff — Mathlib

English

For Multiset s and List l, l is in lists s iff s equals the quotient of l by permutation.

Русский

Для Multiset s и списка l: l в lists s эквивалентно тому, что s равняется коeтвофикатору l по перестановкам.

LaTeX

$$$l \\in lists\\, s \\iff s = \\langle l \\rangle$$$

Lean4

@[simp]
theorem mem_lists_iff (s : Multiset α) (l : List α) : l ∈ lists s ↔ s = ⟦l⟧ :=
  by
  induction s using Quotient.inductionOn
  simpa using perm_comm

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