traverse_def — Mathlib

English

There is a simple rule for traverse: traversing a vector with f at its head equals mapping f over head together with traversing the tail.

Русский

Существует простое правило для traverse: обход вектора с функцией f в голове эквивалентен отображению f над головой и обходу хвоста.

LaTeX

$$$ \\text{traverse}\\ f\\ (\\text{cons } x\\ xs) = \\text{map}\\ (\\text{cons } \\; f\\ x)\\ (\\text{traverse}\\ f\\ xs) $$$

Lean4

@[simp]
protected theorem traverse_def (f : α → F β) (x : α) :
    ∀ xs : Vector α n, (x ::ᵥ xs).traverse f = cons <$> f x <*> xs.traverse f := by rintro ⟨xs, rfl⟩; rfl

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