traverse_eq_map_id — Mathlib

English

For any f : α → β, traversing with f inside a pure context equals pure of map f over the vector.

Русский

Для любого отображения f: α → β обход с f внутри чистой контексты равен чистому отображению map f над вектором.

LaTeX

$$$ \\forall x,\\; x.traverse (\\text{pure} \\circ f) = \\text{pure} (\\text{map} f\\ x) $$$

Lean4

protected theorem traverse_eq_map_id {α β} (f : α → β) :
    ∀ x : Vector α n, x.traverse ((pure : _ → Id _) ∘ f) = pure (map f x) := by rintro ⟨x, rfl⟩; simp! ;
  induction x <;> simp! [*, functor_norm]; rfl

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