lookup_insert_ne — Mathlib

English

If a ≠ a', then the two-step insertions are permutation-equivalent: inserting (a,b) then (a',b') into s has the same entries as inserting (a',b') then (a,b) into s.

Русский

Если a ≠ a', то последовательности вставок с ключами (a,b) и (a',b') эквивалентны по перестановке: в любом случае получатся одинаковые записи до перестановки.

LaTeX

$$$ a \\neq a' \\Rightarrow ((s.insert a b).insert a' b').entries \\text{.Perm} ((s.insert a' b').insert a b).entries $$$

Lean4

@[simp]
theorem lookup_insert_ne {a a'} {b' : β a'} {s : AList β} (h : a ≠ a') : lookup a (insert a' b' s) = lookup a s :=
  dlookup_kinsert_ne h

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