instAddDyckWord

Mathlib.Combinatorics.Enumerative.DyckWord

URI: https://scilib.ai/kg/mathlib#instAddDyckWord

Lean4

instance : Add DyckWord where
  add p
    q :=
    ⟨p ++ q, by simp only [count_append, p.count_U_eq_count_D, q.count_U_eq_count_D],
      by
      simp only [take_append, count_append]
      exact fun _ ↦ add_le_add (p.count_D_le_count_U _) (q.count_D_le_count_U _)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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