perm_erase — Mathlib

English

If s1.entries is a permutation of s2.entries, then (erase a s1).entries is a permutation of (erase a s2).entries.

Русский

Если s1.entries перестановка s2.entries, то (erase a s1).entries перестановка (erase a s2).entries.

LaTeX

$$s_1.entries \sim s_2.entries \Rightarrow (erase(a,s_1)).entries \sim (erase(a,s_2)).entries$$

Lean4

theorem perm_erase {a : α} {s₁ s₂ : AList β} : s₁.entries ~ s₂.entries → (erase a s₁).entries ~ (erase a s₂).entries :=
  Perm.kerase s₁.nodupKeys

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