English
If l1 is a suffix of l2, then for every function f: α → List β, the operation of mapping f over the two lists preserves the suffix relation: l1.flatMap f is a suffix of l2.flatMap f.
Русский
Если l1 является суффиксом l2, то для любой функции f: α → List β отображение f по двум спискам сохраняет отношение суффикса: l1.flatMap f является суффиксом l2.flatMap f.
LaTeX
$$$\forall \alpha \forall \beta \forall l_1,l_2 : \text{List}(\alpha), \forall f : \alpha \to \text{List}(\beta),\; (\exists t : \text{List}(\alpha),\ l_2 = l_1 ++ t) \Rightarrow (\exists t' : \text{List}(\beta),\ l_2.flatMap f = l_1.flatMap f ++ t'.flatMap f).$$$
Lean4
@[gcongr]
protected theorem flatMap (h : l₁ <:+ l₂) (f : α → List β) : l₁.flatMap f <:+ l₂.flatMap f :=
(h.map _).flatten
