setOf_mem_sym2 — Mathlib

English

The set of Sym2-elements obtained from membership in xs is the same as the Sym2-set built from xs.

Русский

Множество элементов Sym2, полученных из xs, совпадает с множеством Sym2, полученным из xs.

LaTeX

$$$$ \\{ z : Sym2 α \\mid z \\in xs.sym2 \\} = \\{ x : Sym2 α \\mid x \\in xs \\}.sym2 $$$$

Lean4

theorem setOf_mem_sym2 {xs : List α} : {z : Sym2 α | z ∈ xs.sym2} = {x : α | x ∈ xs}.sym2 :=
  Set.ext fun z ↦ z.ind fun a b => by simp [mk_mem_sym2_iff]

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