nest_denest

Mathlib.Combinatorics.Enumerative.DyckWord

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

English

Compatibility of denesting and nesting operations under the nonzero hypothesis yields the original word.

Русский

Совместимость операций денест и nest под не нулевым условием даёт исходное Dyck слово.

LaTeX

$$$$ p.denest hn . nest = p $$$$

Lean4

theorem nest_denest (hn) : (p.denest hn).nest = p := by simpa [DyckWord.ext_iff] using p.cons_tail_dropLast_concat hn.1

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

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

Разделы

Аффилиация

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