mk_mem_sym2_iff — Mathlib

English

The set of pairs forming Sym2 elements contained in m.sym2 coincides with the Sym2 of the set of elements contained in m.

Русский

Множество пар, содержащихся в m.sym2, совпадает с Sym2 множества элементов m.

LaTeX

$$$ {z : Sym2 \\alpha | z \\in m.sym2} = {x : \\alpha | x \\in m}.sym2 $$$

Lean4

theorem mk_mem_sym2_iff {m : Multiset α} {a b : α} : s(a, b) ∈ m.sym2 ↔ a ∈ m ∧ b ∈ m :=
  m.inductionOn fun xs => by simp [List.mk_mem_sym2_iff]

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