traverse — Mathlib

English

Traverse for Finset maps a function α → F β to a Finset β inside F, producing an F-structured Finset of results.

Русский

Traverse для Finset переводит функцию α → F β в Finset β внутри F, создавая Finset β с обрамлением F.

LaTeX

$$$$ \\mathrm{traverse} \\; f \\; s : F (\\mathrm{Finset}\\; \\beta) $$$$

Lean4

/-- Traverse function for `Finset`. -/
def traverse [DecidableEq β] (f : α → F β) (s : Finset α) : F (Finset β) :=
  Multiset.toFinset <$> Multiset.traverse f s.1

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