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]