zero_le

Mathlib.Combinatorics.Enumerative.DyckWord

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

English

Every Dyck word p is greater than or equal to the zero word in the DyckWord order: 0 ≤ p.

Русский

Любое DyckWord p не меньше нулевого слова в порядке DyckWord: 0 ≤ p.

LaTeX

$$$ 0 \le p $$$

Lean4

protected theorem zero_le : 0 ≤ p :=
  add_zero p ▸ le_add_self p 0

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

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

Разделы

Аффилиация

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