map_append_flatMap_perm — Mathlib

English

Mapping on the left combined with flatMap on the right yields a permutation to a mapped flatMap form.

Русский

Отображение слева в сочетании с flatMap справа образуют перестановку в соответствующей карте.

LaTeX

$$$l.map f ++ l.flatMap g \\sim l.flatMap (\\lambda x. f x :: g x)$$$

Lean4

theorem map_append_flatMap_perm (l : List α) (f : α → β) (g : α → List β) :
    l.map f ++ l.flatMap g ~ l.flatMap fun x => f x :: g x := by
  simpa [← map_eq_flatMap] using flatMap_append_perm l (fun x => [f x]) g

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