English
A property holds for all dependent Fin (m+n) indices iff it holds for all Fin m and Fin n decompositions via addCases.
Русский
Свойство верно для всех зависимых индексов Fin(m+n) тогда и только тогда, когда оно верно для всех разложений на Fin m и Fin n через addCases.
LaTeX
$$$\\\\forall {\\\\gamma : Fin (m+n) \\to Sort*} {P : (\\\\forall i, \\\\gamma i) \\to Prop}, \\\\bigl( (\\\\forall v, P v) \\bigr) \\\\Leftrightarrow \\\\bigl(\\\\forall v_m : (\\\\forall i, \\\\gamma (castAdd n i)) \ (v_n : (\\\\forall j, \\\\gamma (natAdd m j))), P(\\\\operatorname{addCases} v_m v_n) \\bigr)$$$
Lean4
/-- A property holds for all dependent finite sequence of length m + n iff
it holds for the concatenation of all pairs of length m sequences and length n sequences. -/
theorem forall_fin_add_pi {γ : Fin (m + n) → Sort*} {P : (∀ i, γ i) → Prop} :
(∀ v, P v) ↔ (∀ (vₘ : ∀ i, γ (castAdd n i)) (vₙ : ∀ j, γ (natAdd m j)), P (addCases vₘ vₙ))
where
mp hv vm vn := hv (addCases vm vn)
mpr h
v := by
convert h (fun i => v (castAdd n i)) (fun j => v (natAdd m j))
exact (addCases_castAdd_natAdd v).symm
