reduceOption — Mathlib

English

If l1 is a prefix of l2 for lists of Option objects, then l1.reduceOption is a prefix of l2.reduceOption.

Русский

Если l1 является префиксом l2 для списков элементов типа Option, то l1.reduceOption является префиксом l2.reduceOption.

LaTeX

$$$\forall {l_1 l_2 : \text{List}(\text{Option}(\alpha))},\; l_1 <+: l_2 \Rightarrow l_1.reduceOption <+: l_2.reduceOption.$$$

Lean4

protected theorem reduceOption {l₁ l₂ : List (Option α)} (h : l₁ <+: l₂) : l₁.reduceOption <+: l₂.reduceOption :=
  h.filterMap id

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