English
If l1 is an infix of l2 (i.e., l2 contains l1 as a contiguous block), then for every f: α → List β, the list l1.flatMap f is an infix of l2.flatMap f.
Русский
Если l1 является инфиксом (подпоследовательность подряд) l2, то для любой функции f: α → List β список 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 p,q : \text{List}(\alpha),\ l_2 = p ++ l_1 ++ q) \Rightarrow (\exists p',q' : \text{List}(\beta),\ l_2.flatMap f = p' ++ (l_1.flatMap f) ++ q').$$$
Lean4
@[gcongr]
protected theorem flatMap (h : l₁ <:+: l₂) (f : α → List β) : l₁.flatMap f <:+: l₂.flatMap f :=
(h.map _).flatten
