English
snoc x x0 is injective iff x is injective and x0 not in range x.
Русский
snoc x x0 инъективно тогда и только тогда, когда x инъективна и x0 не принадлежит образу x.
LaTeX
$$$\\\\operatorname{Injective}(\\\\operatorname{snoc} x x_0) \\\\Leftrightarrow (\\\\operatorname{Injective} x) \\\\land (x_0 \\notin \\operatorname{range}(x))$$$
Lean4
theorem snoc_injective_iff {α} {x₀ : α} {x : Fin n → α} :
Function.Injective (snoc x x₀ : Fin n.succ → α) ↔ Function.Injective x ∧ x₀ ∉ Set.range x :=
by
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ snoc_injective_of_injective h.1 h.2⟩
· simpa [Function.comp] using h.comp (Fin.castSucc_injective _)
· rintro ⟨i, hi⟩
rw [← @snoc_last n (fun i ↦ α) x₀ x, ← @snoc_castSucc n (fun i ↦ α) x₀ x i, h.eq_iff] at hi
exact ne_last_of_lt i.castSucc_lt_last hi
