reduceOption_cons_of_some — Mathlib

English

The reduceOption of a list starting with some x is x followed by the reduceOption of the tail.

Русский

Уменьшение списка, начинающегося с some x, даёт x и далее уменьшение хвоста.

LaTeX

$$$\operatorname{reduceOption}(\mathrm{cons}(\mathrm{Option.some}(x), l)) = x :: l.reduceOption$$$

Lean4

@[simp]
theorem reduceOption_cons_of_some (x : α) (l : List (Option α)) : reduceOption (some x :: l) = x :: l.reduceOption := by
  simp only [reduceOption, filterMap, id]

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