setOf_mem_sym2 — Mathlib

English

The set {z ∈ Sym^2 α | z ∈ m.sym2} equals {x ∈ α | x ∈ m}.sym2.

Русский

Множество {z ∈ Sym^2 α | z ∈ m.sym2} равно {x ∈ α | x ∈ m}.sym2.

LaTeX

$$$\{ z \in \mathrm{Sym}^2(\alpha) \mid z \in m.\mathrm{sym}^2 \} = \{ x \in \alpha \mid x \in m \}.\mathrm{sym}^2$$$

Lean4

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

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