firstReturn — Mathlib

English

Let p be a nonzero Dyck word. The firstReturn(p) is the least index i such that the prefix of length i+1 has equal numbers of U and D; for p = 0, firstReturn(0) = 0.

Русский

Пусть p ≠ 0. firstReturn(p) — наименьший индекс i, для которого префикс длины i+1 содержит равное число U и D; для p = 0 выполняется firstReturn(0) = 0.

LaTeX

$$$$ firstReturn(p) = \min\{ i : (p.toList.take(i+1)).count U = (p.toList.take(i+1)).count D \}.$$$$

Lean4

/-- `p.firstReturn` is 0 if `p = 0` and the index of the `D` matching the initial `U` otherwise. -/
def firstReturn : ℕ :=
  (range p.toList.length).findIdx fun i ↦ (p.toList.take (i + 1)).count U = (p.toList.take (i + 1)).count D

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