Map identity over a list

2/4 ~25 minlean

Prove that mapping the identity function does not change a list.

3 lines · Lean 4

theorem map_id_local (xs : List α) :
    xs.map (fun x => x) = xs := by
  sorry

Objectifs

Indices

Voir la solution

theorem map_id_local (xs : List α) :
    xs.map (fun x => x) = xs := by
  induction xs with
  | nil => rfl
  | cons x xs ih => simp [ih]