flatMap — Mathlib

English

If l1 is a sublist of l2, then l1.flatMap f is a sublist of l2.flatMap f for any function f.

Русский

Если l1 является подпоследовательностью l2, то l1.flatMap f является подпоследовательностью l2.flatMap f для любой функции f.

LaTeX

$$$$ \\text{If } l_1 <+ l_2, \\ \\ l_1.\\mathrm{flatMap} f <+ l_2.\\mathrm{flatMap} f. $$$$

Lean4

@[gcongr]
protected theorem flatMap {l₁ l₂ : List α} (h : l₁ <+ l₂) (f : α → List β) : l₁.flatMap f <+ l₂.flatMap f :=
  (h.map f).flatten

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