English
For a family of inhabited types Γ indexed by ι, the nth element of the map of projections equals the nth projection value: (ListBlank.map (proj i) L).nth n = L.nth n i.
Русский
Для семейства типов Γ i индексируемого множества ι, где каждый Γ i непуст, элемент списка после отображения проекции proj i равен соответствующему элементу проекции: (ListBlank.map (proj i) L).nth n = L.nth n i.
LaTeX
$$$\forall {\iota} {\Gamma : \iota → Type} [\forall i, Inhabited (\Gamma i)] (i : \iota) (L : ListBlank((i : \iota) → \Gamma i)) (n : \mathbb{N}), (ListBlank.map (proj i) L).nth n = L.nth n i$$$
Lean4
theorem proj_map_nth {ι : Type*} {Γ : ι → Type*} [∀ i, Inhabited (Γ i)] (i : ι) (L n) :
(ListBlank.map (@proj ι Γ _ i) L).nth n = L.nth n i := by rw [ListBlank.nth_map]; rfl
