getElem_idxOf — Mathlib

English

If a is in l and idxOf a l is some i, then l[i] = a.

Русский

Если a ∈ l и idxOf a l = i, то l[i] = a.

LaTeX

$$$ a \in l \Rightarrow \mathrm{getElem}\ l\; (\mathrm{idxOf}\ a\ l) = a $$$

Lean4

@[simp]
theorem getElem_idxOf [DecidableEq α] {a : α} : ∀ {l : List α} (h : idxOf a l < l.length), l[idxOf a l] = a
  | b :: l, h => by
    by_cases h' : b = a <;>
      simp [h', getElem_idxOf]
        -- This is incorrectly named and should be `get_idxOf`;
        -- this already exists, so will require a deprecation dance.

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