English
For xs : Fin m → α and ys : Fin n → α, Function.Injective (Fin.append xs ys) is equivalent to Function.Injective xs ∧ Function.Injective ys ∧ ∀ i ∈ Fin m, ∀ j ∈ Fin n, xs i ≠ ys j.
Русский
Для xs : Fin m → α и ys : Fin n → α, инъективность Fin.append xs ys эквивалентна инъективности xs и ys и неравенству xs i ≠ ys j для всех i∈Fin m, j∈Fin n.
LaTeX
$$$\\mathrm{Function.Injective}(\\mathrm{Fin.append}\, xs\, ys) \\iff \\mathrm{Function.Injective}(xs) \\wedge \\mathrm{Function.Injective}(ys) \\wedge \\forall i \\in Fin m, \\forall j \\in Fin n, xs(i) \\neq ys(j).$$$
Lean4
/-- Splitting a dependent finite sequence v into an initial part and a final part,
and then concatenating these components, produces an identical sequence. -/
theorem addCases_castAdd_natAdd {γ : Fin (m + n) → Sort*} (v : ∀ i, γ i) :
addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) = v :=
by
ext i
cases i using addCases <;> simp
