count_take_firstReturn_add_one — Mathlib

English

In the prefix up to firstReturn + 1, the number of U's equals the number of D's.

Русский

В префиксе до firstReturn + 1 число U равно числу D.

LaTeX

$$$$ (p.toList.take(p.firstReturn+1)).count U = (p.toList.take(p.firstReturn+1)).count D. $$$$

Lean4

theorem count_take_firstReturn_add_one :
    (p.toList.take (p.firstReturn + 1)).count U = (p.toList.take (p.firstReturn + 1)).count D :=
  by
  have := findIdx_getElem (w := (length_range (n := p.toList.length)).symm ▸ firstReturn_lt_length h)
  simpa using this

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