insertIdx_injective — Mathlib

English

The function l ↦ l.insertIdx n x is injective for all natural n and elements x.

Русский

Функция l ↦ l.insertIdx n x инъективна для всех натуральных n и элементов x.

LaTeX

$$$\forall l_1,l_2:\text{List}(\alpha),\ l_1.insertIdx(n,x)=l_2.insertIdx(n,x) \Rightarrow l_1=l_2.$$$

Lean4

theorem insertIdx_injective (n : ℕ) (x : α) : Function.Injective (fun l : List α => l.insertIdx n x) := by
  induction n with
  | zero => simp
  | succ n IH => rintro (_ | ⟨a, as⟩) (_ | ⟨b, bs⟩) h <;> simpa [IH.eq_iff] using h

Похожие утверждения