IsNested

Mathlib.Combinatorics.Enumerative.DyckWord

URI: https://scilib.ai/kg/mathlib#DyckWord.IsNested

Lean4

/-- A property stating that `p` is nonempty and strictly positive in its interior,
i.e. is of the form `(x)` with `x` a Dyck word. -/
def IsNested : Prop :=
  p ≠ 0 ∧ ∀ ⦃i⦄, 0 < i → i < p.toList.length → (p.toList.take i).count D < (p.toList.take i).count U

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru