monotone_semilength — Mathlib

English

The semilength function is monotone with respect to the DyckWord order: if p ≤ q then semilength(p) ≤ semilength(q).

Русский

Функция semilength монотонична по порядку DyckWord: если p ≤ q, то semilength(p) ≤ semilength(q).

LaTeX

$$$ p \le q \Rightarrow \operatorname{semilength}(p) \le \operatorname{semilength}(q) $$$

Lean4

theorem monotone_semilength : Monotone semilength := fun p q pq ↦ by
  induction pq with
  | refl => rfl
  | tail _ mq ih =>
    rename_i m r _
    rcases eq_or_ne r 0 with rfl | hr
    · rw [insidePart_zero, outsidePart_zero, or_self] at mq
      rwa [mq] at ih
    · rcases mq with hm | hm
      · exact ih.trans (hm ▸ semilength_insidePart_lt hr).le
      · exact ih.trans (hm ▸ semilength_outsidePart_lt hr).le

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