lookup_union_left

Mathlib.Data.List.AList

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

English

If a is in s1, then lookup of a in s1 ∪ s2 equals the lookup in s1.

Русский

Если a принадлежит s1, то поиск a в s1 ∪ s2 равен поиску в s1.

LaTeX

$$$ a \in s_1 \Rightarrow \mathrm{lookup}(a, s_1 \cup s_2) = \mathrm{lookup}(a, s_1) $$$

Lean4

@[simp]
theorem lookup_union_left {a} {s₁ s₂ : AList β} : a ∈ s₁ → lookup a (s₁ ∪ s₂) = lookup a s₁ :=
  dlookup_kunion_left

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

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

Разделы

Аффилиация

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