English
If l is a list of Σ a, β a with NodupKeys, then mapping the first component by an injective f produces a list whose NodupKeys property is preserved; i.e., (l.map (.map f fun _ => id)).NodupKeys holds whenever l.NodupKeys holds and f is injective.
Русский
Если l — список пар Σ a, β a и имеет свойство NodupKeys, то отображение первой координаты через инъективную f сохраняет свойство NodupKeys у полученного списка.
LaTeX
$$$ \forall {l : List ((\, : α) \times β)}, l.NodupKeys \rightarrow (List.map (Sigma.map f (\lambda x, \mathrm{id})) l).NodupKeys $$$
Lean4
theorem map₁ {β : Type v} (f : α → α') (hf : Function.Injective f) {l : List (Σ _ : α, β)} (nd : l.NodupKeys) :
(l.map (.map f fun _ => id) : List (Σ _ : α', β)).NodupKeys := by
induction l with
| nil => grind [nodupKeys_nil]
| cons hd tl =>
have := dlookup_map₁ tl hf hd.fst
grind [dlookup_isSome, → notMem_keys_of_nodupKeys_cons, nodupKeys_of_nodupKeys_cons, nodupKeys_cons]
