id_traverse — Mathlib

English

Traversing Finset with the Identity monad yields the original Finset (up to the monad structure): traverse Id.pure s = Id.pure s.

Русский

Обход Finset через монаду идентичности возвращает исходное Finset (в рамках монады): traverse Id.pure s = Id.pure s.

LaTeX

$$$$ \\mathrm{traverse} (\\mathrm{Id}.\\mathrm{pure})\\; s = \\mathrm{Id}.\\mathrm{pure} \\; s $$$$

Lean4

@[simp]
theorem id_traverse [DecidableEq α] (s : Finset α) : traverse (pure : α → Id α) s = pure s :=
  by
  rw [traverse, Multiset.id_traverse]
  exact s.val_toFinset

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