outsidePart_nest

Mathlib.Combinatorics.Enumerative.DyckWord

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

← MathLib Explorer

English

If p ≠ 0, then p.nest.outsidePart = 0.

Русский

Если p ≠ 0, то p.nest.outsidePart = 0.

LaTeX

$$$$ p \neq 0 \implies p.nest.outsidePart = 0. $$$$

Lean4

@[simp]
theorem outsidePart_nest : p.nest.outsidePart = 0 :=
  by
  simp_rw [outsidePart, nest_ne_zero, dite_false, firstReturn_nest]
  rw [DyckWord.ext_iff]; apply drop_of_length_le
  simp_rw [nest, length_append, length_singleton]; cutsat

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

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

Разделы

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

Аффилиация

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