reduceOption_eq_append_iff — Mathlib

English

The reduceOption of l equals the concatenation of the reduces of its parts when l is split.

Русский

ReduceOption(l) равен конкатенации ReduceOption частей l, когда l разбивается на части.

LaTeX

$$$\mathrm{reduceOption}(l) = (l_1 \append l_2).\mathrm{reduceOption} \iff \exists l_1, l_2,\; l = l_1 \append l_2 \land l_1.reduceOption = l' \land l_2.reduceOption = l''$$$

Lean4

theorem reduceOption_eq_append_iff (l : List (Option α)) (l'₁ l'₂ : List α) :
    l.reduceOption = l'₁ ++ l'₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.reduceOption = l'₁ ∧ l₂.reduceOption = l'₂ :=
  by
  dsimp [reduceOption]
  exact filterMap_eq_append_iff

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