perm_lookup

Mathlib.Data.List.AList

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

English

If s1.entries is a permutation of s2.entries, then lookup a s1 = lookup a s2.

Русский

Если entries s1 является перестановкой entries s2, то lookup a s1 = lookup a s2.

LaTeX

$$s_1.entries \sim s_2.entries \Rightarrow \mathrm{lookup}(a,s_1) = \mathrm{lookup}(a,s_2)$$

Lean4

theorem perm_lookup {a : α} {s₁ s₂ : AList β} (p : s₁.entries ~ s₂.entries) : s₁.lookup a = s₂.lookup a :=
  perm_dlookup _ s₁.nodupKeys p

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

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

Разделы

Аффилиация

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