English
Let l be a list of pairs (a, b) with a ∈ α and b ∈ β a. If f: α → α′ is injective, then the dependent lookup after transporting the first coordinate along f yields the same result as the original lookup: dlookup(f(a)) of the transformed list equals dlookup(a) of the original list.
Русский
Пусть l — список пар (a, b) с a ∈ α и b ∈ β(a). Пусть f: α → α′ инъективно. Тогда результирующий dlookup после переноса первой координаты вдоль f равен исходному: dlookup(f(a)) преобразованного списка равен dlookup(a) исходного списка.
LaTeX
$$$ (\mathrm{List.map}(\mathrm{Sigma.map} \; f \; \mathrm{id})\ l)\; :\; (\Sigma a', β a') \; with \; dlookup (f a) (l.map (Sigma.map f id)) = dlookup(a,l) $$$
Lean4
theorem dlookup_map₁ {β : Type v} (l : List (Σ _ : α, β)) {f : α → α'} (hf : Function.Injective f) (a : α) :
(l.map (.map f fun _ => id) : List (Σ _ : α', β)).dlookup (f a) = l.dlookup a :=
by
have := dlookup_map (β' := fun _ => β) (f := f) (g := fun _ => id)
grind [Option.map_id']
