id_traverse — Mathlib

English

For any x in a Multiset, traversing with the identity pure (Id) yields the identity of x under the Id monad: traverse (pure : α→Id α) x = pure x.

Русский

Для любого элемента мультсета выполняется: обход через тождественное чистое возвращает тот же элемент: traverse (pure) x = pure x.

LaTeX

$$$\\operatorname{traverse} (\\mathrm{pure} : \\alpha \\to \\mathrm{Id}\\ \\alpha)\\ x = \\mathrm{pure}\\ x$$$

Lean4

theorem id_traverse {α : Type*} (x : Multiset α) : traverse (pure : α → Id α) x = pure x :=
  by
  refine Quotient.inductionOn x ?_
  intro
  simp [traverse]

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