reduceOption_concat_of_some — Mathlib

English

Concatenating a list with some x and then reducing equals reducing the list and appending x.

Русский

Объединение списка с some x и последующее уменьшение эквивалентно уменьшению списка и добавлению x.

LaTeX

$$$\mathrm{reduceOption}(l \concat (\mathrm{some} x)) = (\mathrm{reduceOption}(l)).\concat x$$$

Lean4

theorem reduceOption_concat_of_some (l : List (Option α)) (x : α) :
    (l.concat (some x)).reduceOption = l.reduceOption.concat x := by
  simp only [reduceOption_nil, concat_eq_append, reduceOption_append, reduceOption_cons_of_some]

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