head_eq_U — Mathlib

English

Let p be a nonempty Dyck word. Then the first element of its list representation is U.

Русский

Пусть p — ненулевое Dyck-слово. Тогда первый элемент списка, соответствующего p, равен U.

LaTeX

$$$$ \\text{If } p \\neq 0, \\quad \\text{head}(p.toList) = U. $$$$

Lean4

/-- The first element of a nonempty Dyck word is `U`. -/
theorem head_eq_U (p : DyckWord) (h) : p.toList.head h = U :=
  by
  rcases p with - | s; · tauto
  rw [head_cons]
  by_contra f
  rename_i _ nonneg
  simpa [s.dichotomy.resolve_left f] using nonneg 1

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