insert_insert

Mathlib.Data.Finmap

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

← MathLib Explorer

English

If a ≠ a', then (s.insert a b).insert a' b' = (s.insert a' b').insert a b.

Русский

Если a ≠ a', то (s.insert a b).insert a' b' = (s.insert a' b').insert a b.

LaTeX

$$$ (s.insert a b).insert a' b' = (s.insert a' b').insert a b $$$

Lean4

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

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

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

Разделы

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

Аффилиация

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