Entries of nested Array.ofFn

This file reads an entry of a two-dimensional array built with Array.ofFn.

Main results

• Array.getElem_getElem_ofFn_ofFn: the (i, k) entry of Array.ofFn fun a ↦ Array.ofFn (F a) is F i k.

theorem Array.getElem_getElem_ofFn_ofFn {β : Type u_1} {m n : Nat} (F : Fin m → Fin n → β) (i : Fin m) (k : Fin n) (h₁ : ↑i < (ofFn fun (a : Fin m) => ofFn (F a)).size) (h₂ : ↑k < (ofFn fun (a : Fin m) => ofFn (F a))[↑i].size) : (ofFn fun (a : Fin m) => ofFn (F a))[↑i][↑k] = F i k

The (i, k) entry of the two-dimensional array Array.ofFn fun a ↦ Array.ofFn (F a) is F i k.