infix_of_le — Mathlib

English

If p ≤ q then the list representation of p is an infix of the list representation of q.

Русский

Если p ≤ q, то список p является внутри списка q.

LaTeX

$$$ \text{If } p \le q, \ p^{\text{toList}} \text{ is an infix of } q^{\text{toList}}. $$$$

Lean4

theorem infix_of_le (h : p ≤ q) : p.toList <:+: q.toList := by
  induction h with
  | refl => exact infix_refl _
  | tail _pm 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
    · have : [U] ++ r.insidePart ++ [D] ++ r.outsidePart = r := DyckWord.ext_iff.mp (nest_insidePart_add_outsidePart hr)
      grind

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