coe_attach — Mathlib

English

The attach of a Sym, when coerced, matches the corresponding multiset construction.

Русский

При приведении типа, attach Sym согласуется с соответствующим построением мультисета.

LaTeX

$$$\\forall s : \\mathrm{Sym}(\\alpha,n),\\ (s.attach : \\operatorname{Multiset} \\{ x \\mid x \\in s \\}) = \\operatorname{Multiset.attach}(s : \\operatorname{Multiset}(\\alpha)).$$$

Lean4

@[simp]
theorem coe_attach (s : Sym α n) : (s.attach : Multiset { a // a ∈ s }) = Multiset.attach (s : Multiset α) :=
  rfl

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