reduceOption_concat — Mathlib

English

Reducing after concatenating a list with an element equals the concatenation of the reduced list with that element.

Русский

Уменьшение после конкатенации списка с элементом равняется конкатенации уменьшенного списка и этого элемента.

LaTeX

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

Lean4

theorem reduceOption_concat (l : List (Option α)) (x : Option α) :
    (l.concat x).reduceOption = l.reduceOption ++ x.toList := by
  induction l generalizing x with
  | nil => cases x <;> simp [Option.toList]
  | cons hd tl hl =>
    simp only [concat_eq_append, reduceOption_append] at hl
    cases hd <;> simp [hl, reduceOption_append]

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