applyId_eq_self — Mathlib

English

As before, under nodup and length equality, x mapped to y by the zipped function corresponds to the i-th element of ys.

Русский

Как ранее, при условии без повторов и равной длины, отображение x в y через зашитый список соответствует i-й элемент ys.

LaTeX

$$$xs.Nodup \rightarrow xs.length = ys.length \rightarrow \forall x,y,i, xs[i]? = Some(x) \rightarrow (List.applyId(xs.zip ys) x = y) \iff ys[i]? = Some(y)$$$

Lean4

theorem applyId_eq_self [DecidableEq α] {xs ys : List α} (x : α) : x ∉ xs → List.applyId.{u} (xs.zip ys) x = x :=
  by
  intro h
  dsimp [List.applyId]
  rw [List.dlookup_eq_none.2]
  · rfl
  simp only [List.keys, not_exists, Prod.toSigma, exists_and_right, exists_eq_right, List.mem_map, Function.comp_apply,
    List.map_map, Prod.exists]
  intro y hy
  exact h (List.of_mem_zip hy).1

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