flatMap — Mathlib

English

If l1 is a prefix of l2, then applying a function f to each element and flattening preserves the prefix relation.

Русский

Если l1 префикс l2, то применение f ко всем элементам и последующее объединение сохраняют префикс.

LaTeX

$$$$ h : l1 <+: l2 \Rightarrow l1.flatMap f <+: l2.flatMap f. $$$$

Lean4

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

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