reduceOption_length_lt_iff — Mathlib

English

The reduced length is strictly less than the original length iff none occurs in l.

Русский

Уменьшенная длина строго меньше исходной тогда и только тогда, когда в l встречается none.

LaTeX

$$$|\mathrm{reduceOption}(l)| < |l| \iff \mathrm{none} \in l$$$

Lean4

theorem reduceOption_length_lt_iff {l : List (Option α)} : l.reduceOption.length < l.length ↔ none ∈ l :=
  by
  rw [Nat.lt_iff_le_and_ne, and_iff_right (reduceOption_length_le l), Ne, reduceOption_length_eq_iff]
  induction l
  · simp
  · grind [cases Option]

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