English
Let m be a natural number and n: Fin m → ℕ. For i ∈ Fin m and j ∈ Fin (n i), the natural number corresponding to the function Pi.single i j under the standard encoding equals j times the product of the sizes n(·) over all indices strictly before i.
Русский
Пусть m — натуральное число и n: Fin m → ℕ. Пусть i ∈ Fin m и j ∈ Fin (n i). Число, соответствующее функции Pi.single i j под стандартным кодированием, равно j умножить на произведение n(k) по всем индексам, меньшим i.
LaTeX
$$$(\\mathrm{finPiFinEquiv}(\\Pi\\text{.single } i\\, j) : \\mathbb{N}) = j \\cdot \\prod_{k \\in \\mathrm{Fin}(m),\\ k < i} n(k)$$$
Lean4
theorem finPiFinEquiv_single {m : ℕ} {n : Fin m → ℕ} [∀ i, NeZero (n i)] (i : Fin m) (j : Fin (n i)) :
(finPiFinEquiv (Pi.single i j : ∀ i : Fin m, Fin (n i)) : ℕ) = j * ∏ j, n (Fin.castLE i.is_lt.le j) :=
by
rw [finPiFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
rintro x hx
rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]
