take — Mathlib

English

Take i symbols from a Dyck word forming a new Dyck word provided the numbers of U and D are balanced in that prefix.

Русский

Взять первые i символов из Dyck слова дают новое Dyck слово при условии баланса U и D в префиксе.

LaTeX

$$$$ \text{take}(i, hi) : \text{DyckWord} $$$$

Lean4

/-- Prefix of a Dyck word as a Dyck word, given that the count of `U`s and `D`s in it are equal. -/
def take (i : ℕ) (hi : (p.toList.take i).count U = (p.toList.take i).count D) : DyckWord
    where
  toList := p.toList.take i
  count_U_eq_count_D := hi
  count_D_le_count_U k := by rw [take_take]; exact p.count_D_le_count_U (min k i)

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