reduceOption_length_eq — Mathlib

English

The length of reduceOption(l) equals the length of the filter of l by isSome.

Русский

Длина reduceOption(l) равна длине фильтра по isSome над l.

LaTeX

$$$\mathrm{length}(\mathrm{reduceOption}(l)) = \mathrm{length}(\mathrm{filter}(\mathrm{Option.isSome}, l))$$$

Lean4

theorem reduceOption_length_eq {l : List (Option α)} : l.reduceOption.length = (l.filter Option.isSome).length := by
  induction l with
  | nil => simp_rw [reduceOption_nil, filter_nil, length]
  | cons hd tl hl => cases hd <;> simp [hl]

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