English
Let n be a natural number and α a family of sets indexed by Fin n. For any m ≤ n and any v: (i : Fin n) → α i, the m-element prefix is the function on Fin m defined by taking the i-th entry from v at the corresponding position in Fin n. Equivalently, (take m h v)(i) = v(castLE h i).
Русский
Пусть n — натуральное число и α — семейство множеств, индексируемое Fin n. Для любого m ≤ n и любого v: (i : Fin n) → α i, первые m координат задают отображение Fin m → α i, заданное как (take m h v)(i) = v(castLE h i). Эквивалентно, take — это ограничение v на первый m координат.
LaTeX
$$$$\forall m, n, h, v:\ Fin \ m \to \alpha i, \ (\text{take } m\ h\ v)(i) = v(\operatorname{castLE} h\ i) \,\text{ for all } i \in \mathrm{Fin}(m). $$$$
Lean4
/-- Take the first `m` elements of an `n`-tuple where `m ≤ n`, returning an `m`-tuple. -/
def take (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) : (i : Fin m) → α (castLE h i) := fun i ↦ v (castLE h i)
