nest — Mathlib

English

Denesting a nested Dyck word with an inverse operation preserves nesting.

Русский

Разворачивание вложенного Dyck слова с обратной операцией сохраняет вложенность.

LaTeX

$$$$ (p.denest hn).nest = p $$$$

Lean4

protected theorem nest : p.nest.IsNested :=
  ⟨nest_ne_zero, fun i lb ub ↦ by
    simp_rw [nest, length_append, length_singleton] at ub ⊢
    rw [take_append_of_le_length (by rw [singleton_append, length_cons]; cutsat), take_append,
      take_of_length_le (by rw [length_singleton]; cutsat), length_singleton, singleton_append,
      count_cons_of_ne (by simp), count_cons_self, Nat.lt_add_one_iff]
    exact p.count_D_le_count_U _⟩

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