coe_erase — Mathlib

English

For s : Sym α (n+1) and a ∈ α with h ∈ s, the underlying multiset of s.erase a h is exactly Multiset.erase s a.

Русский

Для s ∈ Sym α (n+1) и a ∈ α с h ∈ s, базисная мультимножество s.erase a h равно Multiset.erase s a.

LaTeX

$$$ (s.erase a h) : \mathrm{Multiset} \alpha = s \;\mathrm{toMultiset} \; \mathrm{erase} \ a. $$$

Lean4

@[simp]
theorem coe_erase [DecidableEq α] {s : Sym α n.succ} {a : α} (h : a ∈ s) :
    (s.erase a h : Multiset α) = Multiset.erase s a :=
  rfl

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