semilength — Mathlib

English

Let p be a Dyck word. The semilength of p equals the number of U steps in p, i.e. half of the total number of Dyck steps.

Русский

Пусть p — Dyck-слово. Семилength(p) равна числу шагов U в p, то есть половине общего числа шагов в p.

LaTeX

$$$$\operatorname{semilength}(p) = \#\{ i \in \{0,1,\dots, p.toList.length-1\} : p.toList[i] = U \}.$$$$

Lean4

/-- The semilength of a Dyck word is half of the number of `DyckStep`s in it, or equivalently
its number of `U`s. -/
def semilength : ℕ :=
  p.toList.count U

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