traverse_eq_map_id — Mathlib

English

Traversing with id after mapping equals mapping after traversing with f, with Id as the target functor.

Русский

Перебор с идентичностью после отображения равен отображению после перебора с f в цель Id.

LaTeX

$$$ \forall f:\alpha \to \beta,\ t:\mathrm{Tree}\ \alpha,\ t.traverse(\mathrm{Id}.instMonad.pure \circ f) = \mathrm{Id}.instMonad.pure (t.map f). $$$

Lean4

theorem traverse_eq_map_id (f : α → β) (t : Tree α) : t.traverse ((pure : β → Id β) ∘ f) = pure (t.map f) := by
  induction t with
  | nil => rw [traverse, map]
  | node v l r hl hr =>
    rw [traverse, map, hl, hr, Function.comp_apply, map_pure, pure_seq, map_pure, pure_seq, map_pure]

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