reduceOption_getElem?_iff — Mathlib

English

There exists an index i such that the i-th element equals some (some x) iff there exists an index i with the i-th element of reduceOption equal to some x.

Русский

Существует индекс i, при котором i-й элемент равен some (some x), если и только если существует индекс i, при котором i-й элемент reduceOption равен some x.

LaTeX

$$$\exists i:\\mathbb{N}, l[i]? = \mathrm{some}(\mathrm{some}(x)) \iff \exists i:\\mathbb{N}, l.reduceOption[i]? = \mathrm{some}(x)$$$

Lean4

theorem reduceOption_getElem?_iff {l : List (Option α)} {x : α} :
    (∃ i : ℕ, l[i]? = some (some x)) ↔ ∃ i : ℕ, l.reduceOption[i]? = some x := by
  rw [← mem_iff_getElem?, ← mem_iff_getElem?, reduceOption_mem_iff]

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