reduceOption_eq_nil_iff — Mathlib

English

ReduceOption equals nil exactly when the list is a replication of none's.

Русский

ReduceOption равен пустому тогда и только тогда, когда список состоит из none повторений.

LaTeX

$$$\operatorname{reduceOption}(l) = [] \iff \exists n,\; l = \mathrm{replicate}_n(\mathrm{none})$$$

Lean4

theorem reduceOption_eq_nil_iff (l : List (Option α)) : l.reduceOption = [] ↔ ∃ n, l = replicate n none :=
  by
  dsimp [reduceOption]
  rw [filterMap_eq_nil_iff]
  constructor
  · intro h
    exact ⟨l.length, eq_replicate_of_mem h⟩
  · grind

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