isPrefix_append_of_length — Mathlib

English

If the length of l1 is not greater than that of l2, then l1 is a prefix of l2 ++ l3 if and only if l1 is a prefix of l2.

Русский

Если длина l1 не превышает длину l2, то l1 префикс l2 ++ l3 тогда и только тогда, когда l1 префикс l2.

LaTeX

$$$$ l1.length \le l2.length \Rightarrow (l1 <+: l2 ++ l3) \iff (l1 <+: l2). $$$$

Lean4

theorem isPrefix_append_of_length (h : l₁.length ≤ l₂.length) : l₁ <+: l₂ ++ l₃ ↔ l₁ <+: l₂ :=
  ⟨fun h ↦ by rw [prefix_iff_eq_take] at *; nth_rw 1 [h, take_eq_left_iff]; tauto, fun h ↦
    h.trans <| l₂.prefix_append l₃⟩

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