insert_toFinmap — Mathlib

English

Inserting a value b at key a into the Finmap corresponding to s preserves the Finmap obtained from inserting into the AList: insert a b (AList.toFinmap s) = AList.toFinmap (s.insert a b).

Русский

Вставка значения b по ключу a в Finmap, соответствующий s, эквивалентна преобразованию вставки в AList: insert a b (AList.toFinmap s) = AList.toFinmap (s.insert a b).

LaTeX

$$$ insert\ a\ b\ (AList.toFinmap\ s) = AList.toFinmap\ (s.insert\ a\ b) $$$

Lean4

@[simp]
theorem insert_toFinmap (a : α) (b : β a) (s : AList β) :
    insert a b (AList.toFinmap s) = AList.toFinmap (s.insert a b) := by simp [insert]

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