lookup_insert

Mathlib.Data.Finmap

URI: https://scilib.ai/kg/mathlib#Finmap.lookup_insert

← MathLib Explorer

English

lookup a (insert a b s) = some b.

Русский

lookup a (insert a b s) = some b.

LaTeX

$$$ lookup\ a\ (insert\ a\ b\ s) = \mathrm{Some}(b) $$$

Lean4

@[simp]
theorem lookup_insert {a} {b : β a} (s : Finmap β) : lookup a (insert a b s) = some b :=
  induction_on s fun s => by simp only [insert_toFinmap, lookup_toFinmap, AList.lookup_insert]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru