English
The statement that cons is injective in both arguments is equivalent to x0 not in range x and x is injective.
Русский
Утверждение, что cons инъективно по обоим аргументам, эквивалентно тому, что x0 не принадлежит образу x и что x инъективна.
LaTeX
$$$\\mathrm{cons\_injective\_iff}\\; {n} {\\alpha} {x_0} {x} :\\; \\mathrm{Injective}(\\\\mathrm{cons}(x_0,x)) \\iff (x_0 \\notin \\mathrm{range}(x) \\land \\mathrm{Injective}(x))$$$
Lean4
theorem cons_injective_iff {α} {x₀ : α} {x : Fin n → α} :
Function.Injective (cons x₀ x : Fin n.succ → α) ↔ x₀ ∉ Set.range x ∧ Function.Injective x :=
by
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ cons_injective_of_injective h.1 h.2⟩
· rintro ⟨i, hi⟩
replace h := @h i.succ 0
simp [hi] at h
· simpa [Function.comp] using h.comp (Fin.succ_injective _)
