cons_erase — Mathlib

English

For s : Sym α n.succ and a ∈ α with h ∈ s, we have a ::ₛ (s.erase a h) = s; removing a and then inserting it at the front returns the original Sym element.

Русский

Для s ∈ Sym α (n+1) и a ∈ α с h ∈ s, выполняется a ::ₛ (s.erase a h) = s; удалить a затем вставить его в начало возвращает исходный элемент Sym.

LaTeX

$$$ a ::_{\mathrm{Sym}} (s.erase a h) = s. $$$

Lean4

@[simp]
theorem cons_erase [DecidableEq α] {s : Sym α n.succ} {a : α} (h : a ∈ s) : a ::ₛ s.erase a h = s :=
  coe_injective <| Multiset.cons_erase h

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