English
A property holds for all i in {0,...,m+n-1} iff it holds on the first m indices and on the next n indices after offset m.
Русский
Свойство выполняется для всех индексов {0,...,m+n-1} тогда и только тогда, когда оно выполняется для первых m индексов и для индексов после смещения на m.
LaTeX
$$$\\\\forall i, P i \\\\Leftrightarrow \\\\big(\\\\forall i, P(\\\\castAdd n i)\\\\big) \\\\land \\\\big(\\\\forall j, P(\\\\natAdd m j)\\\\big)$$$
Lean4
/-- A finite sequence of properties P holds for {0, ..., m + n - 1} iff
it holds separately for both {0, ..., m - 1} and {m, ..., m + n - 1}. -/
theorem forall_fin_add {m n} (P : Fin (m + n) → Prop) : (∀ i, P i) ↔ (∀ i, P (castAdd _ i)) ∧ (∀ j, P (natAdd _ j)) :=
⟨fun h => ⟨fun _ => h _, fun _ => h _⟩, fun ⟨hm, hn⟩ => Fin.addCases hm hn⟩
