English
Let n be a natural number and α i a family of types indexed by Fin n. For any chooser v : (i : Fin n) → α i, taking all n coordinates with the reflexive bound yields the original family; i.e., take n (le_refl n) v = v.
Русский
Пусть n—натуральное число и α i—семейство множеств (типов) индексируемое Fin n. Для любой функции v : (i : Fin n) → α i операция взятия всех n координат с отражением по отношению к тождественному доказательству дает исходную семью; т.е. take n (le_refl n) v = v.
LaTeX
$$$\\mathrm{take}_n(\\mathrm{le\\_refl}(n))\\, v = v$$$
Lean4
@[simp]
theorem take_eq_self (v : (i : Fin n) → α i) : take n (le_refl n) v = v :=
by
ext i
simp [take]
