length_eq_reduceOption_length_add_filter_none

English

The total length of l equals the sum of the reduced length and the number of none’s in l.

Русский

Общее число элементов списка равно сумме длины reduceOption(l) и числа none в l.

LaTeX

$$$|l| = |\mathrm{reduceOption}(l)| + | \{ i : l_i = \mathrm{none} \} |$$$

Lean4

theorem length_eq_reduceOption_length_add_filter_none {l : List (Option α)} :
    l.length = l.reduceOption.length + (l.filter Option.isNone).length := by
  simp_rw [reduceOption_length_eq, l.length_eq_length_filter_add Option.isSome, Option.not_isSome]

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