le_add_self — Mathlib

English

For any Dyck words p and q, we have q ≤ p + q in the natural order on Dyck words.

Русский

Для любых DyckWord p и q выполняется q ≤ p + q в естественном порядке для DyckWord.

LaTeX

$$$ q \le p + q $$$

Lean4

theorem le_add_self (p q : DyckWord) : q ≤ p + q :=
  by
  by_cases h : p = 0
  · simp [h]
  · have := semilength_outsidePart_lt h
    exact (le_add_self p.outsidePart q).trans (Relation.ReflTransGen.single (Or.inr (outsidePart_add h).symm))
termination_by p.semilength

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