English
For a map f : (a:α) → β a → β′ a, mapping each Sigma by id f preserves keys; i.e., (l.map (id f)).keys = l.keys.
Русский
Для отображения f: (a:α) → β a → β′ a, отображение Sigma по id f сохраняет ключи; т. е. (l.map (id f)).keys = l.keys.
LaTeX
$$$ (l.map (\mathrm{Sigma.map} \mathrm{id} f)).keys = l.keys $$$
Lean4
theorem map₂_keys {β β' : α → Type*} (f : (a : α) → β a → β' a) (l : List (Σ a, β a)) :
(l.map (.map id f)).keys = l.keys := by induction l <;> grind [Sigma.map]