map₂_keys — Mathlib

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]

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