mem_toMultiset — Mathlib

English

The elements of the unordered pair belong to the corresponding multiset.

Русский

Элементы неупорядоченной пары являются элементами соответствующего мультсет.

LaTeX

$$$$ x \in (z.toMultiset) \iff x \in z. $$$$

Lean4

/-- The members of an unordered pair are members of the corresponding unordered list. -/
@[simp]
theorem mem_toMultiset {α : Type*} {x : α} {z : Sym2 α} : x ∈ (z.toMultiset : Multiset α) ↔ x ∈ z :=
  by
  induction z
  simp [Sym2.toMultiset]

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