entries_insert_of_notMem

Mathlib.Data.List.AList

URI: https://scilib.ai/kg/mathlib#AList.entries_insert_of_notMem

← MathLib Explorer

English

If a ∉ s, then (insert a b s).entries = ⟨a,b⟩ :: s.entries.

Русский

Если a ∉ s, то (insert a b s).entries = ⟨a,b⟩ :: s.entries.

LaTeX

$$a \not\in s \Rightarrow (insert(a,b,s)).entries = (\langle a,b \rangle :: s.entries)$$

Lean4

theorem entries_insert_of_notMem {a} {b : β a} {s : AList β} (h : a ∉ s) :
    (insert a b s).entries = ⟨a, b⟩ :: s.entries := by rw [entries_insert, kerase_of_notMem_keys h]

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

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

Разделы

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

Аффилиация

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