nest_ne_zero

Mathlib.Combinatorics.Enumerative.DyckWord

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

English

For any nonzero Dyck word p, its nest is nonzero.

Русский

Для любого Dyck слова p, не равного нулю, его nest не равно нулю.

LaTeX

$$$$ p.nest \neq 0 $$$$

Lean4

@[simp]
theorem nest_ne_zero : p.nest ≠ 0 := by simp [← toList_ne_nil, nest]

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

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

Разделы

Аффилиация

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