coe_sym2 — Mathlib

English

The underlying set of s.sym2 equals the sym2 of the underlying set of s: (s.sym2 : Set (Sym2 α)) = (s : Set α).sym2.

Русский

Множество, лежащее в основе s.sym2, равно sym2 взятое от множества s: (s.sym2 : Set (Sym2 α)) = (s : Set α).sym2.

LaTeX

$$$(s^{\!\text{sym2}} : Set (Sym2\,\alpha)) = (s : Set \alpha)^{\!\text{sym2}}$$$

Lean4

@[simp]
theorem coe_sym2 {m : Finset α} : (m.sym2 : Set (Sym2 α)) = (m : Set α).sym2 :=
  Set.ext fun z ↦ z.ind fun a b => by simp

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