English
Let l be a list of Σ a, γ a. For a family of maps f = ∀ a, γ a → δ a, we have dlookup a on the mapped list equals the original dlookup a on l, then mapped by f a: (l.map (.map id f)).dlookup a = (l.dlookup a).map (f a).
Русский
Пусть l — список пар Σ a, γ a. Пусть f a: γ a → δ a. Тогда dlookup a на отображенном списке равен исходному dlookup a на l, отображенному по f a: (l.map id f).dlookup a = (l.dlookup a).map (f a).
LaTeX
$$$ (l.map (\mathrm{Sigma.map} \mathrm{id} f) : List (\Sigma a, \delta a)).dlookup a = (l.dlookup a).map (f a) $$$
Lean4
theorem dlookup_map₂ {γ δ : α → Type*} {l : List (Σ a, γ a)} {f : ∀ a, γ a → δ a} (a : α) :
(l.map (.map id f) : List (Σ a, δ a)).dlookup a = (l.dlookup a).map (f a) :=
dlookup_map l Function.injective_id _ _
