count_D_lt_count_U_of_lt_firstReturn

English

For any i with i < firstReturn, the number of D's in the i-prefix is strictly less than the number of U's.

Русский

Для любого i < firstReturn число D в префиксе(i+1) строго меньше числа U.

LaTeX

$$$$ \forall i < p.firstReturn,\ (p.toList.take(i+1)).count D < (p.toList.take(i+1)).count U. $$$$

Lean4

theorem count_D_lt_count_U_of_lt_firstReturn {i : ℕ} (hi : i < p.firstReturn) :
    (p.toList.take (i + 1)).count D < (p.toList.take (i + 1)).count U :=
  by
  have ne := not_of_lt_findIdx hi
  rw [decide_eq_false_iff_not, ← ne_eq, getElem_range] at ne
  exact lt_of_le_of_ne (p.count_D_le_count_U (i + 1)) ne.symm

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