concat_get_prefix — Mathlib

English

If x is a prefix of y and |x| < |y|, then x concatenated with the next element of y is again a prefix of y.

Русский

Если x является префиксом y и |x| < |y|, то x ++ [y на позиции |x|] является префиксом y.

LaTeX

$$$\forall x,y : \text{List}(\alpha),\ x \text{ IsPrefix } y \land |x| < |y| \Rightarrow x ++ [ y_{|x|} ] \text{ IsPrefix } y.$$$

Lean4

theorem concat_get_prefix {x y : List α} (h : x <+: y) (hl : x.length < y.length) : x ++ [y.get ⟨x.length, hl⟩] <+: y :=
  by
  use y.drop (x.length + 1)
  nth_rw 1 [List.prefix_iff_eq_take.mp h]
  convert List.take_append_drop (x.length + 1) y using 2
  rw [← List.take_concat_get, List.concat_eq_append]; rfl

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