entries_insert_of_notMem — Mathlib

English

If a is not present in s, then (insert a b s).entries = ⟨a,b⟩ ::ₘ s.entries.

Русский

Если ключ a отсутствует в s, тогда записи после вставки включают парa (a,b) перед записями s.

LaTeX

$$$ a \notin s \Rightarrow (insert a b s).entries = ⟨a, b⟩ ::ₘ s.entries $$$

Lean4

theorem entries_insert_of_notMem {a : α} {b : β a} {s : Finmap β} :
    a ∉ s → (insert a b s).entries = ⟨a, b⟩ ::ₘ s.entries :=
  induction_on s fun s h => by simp [AList.entries_insert_of_notMem (mt mem_toFinmap.1 h), -entries_insert]

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