dichotomy

Mathlib.Combinatorics.Enumerative.DyckWord

URI: https://scilib.ai/kg/mathlib#DyckStep.dichotomy

English

Every step of a Dyck word is either U (up-step) or D (down-step).

Русский

Каждый шаг Dyck слова либо U, либо D.

LaTeX

$$$$ s = U \lor s = D $$$$

Lean4

/-- Named in analogy to `Bool.dichotomy`. -/
theorem dichotomy (s : DyckStep) : s = U ∨ s = D := by cases s <;> tauto

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

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

Разделы

Аффилиация

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