perm_replace — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem perm_replace {a : α} {b : β a} {s₁ s₂ : AList β} :
    s₁.entries ~ s₂.entries → (replace a b s₁).entries ~ (replace a b s₂).entries :=
  Perm.kreplace s₁.nodupKeys

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