id_traverse — Mathlib

English

Traversing a vector with the identity-pure applicative equals the identity on the vector.

Русский

Обход вектора через идентичную аппликативную чистую операцию равен идентичности на векторе.

LaTeX

$$$ \\text{traverse}_{Id}(x) = Id(x) $$$

Lean4

protected theorem id_traverse : ∀ x : Vector α n, x.traverse (pure : _ → Id _) = pure x :=
  by
  rintro ⟨x, rfl⟩; dsimp [Vector.traverse, cast]
  induction x with
  | nil => rfl
  | cons x xs IH => simp! [IH]

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