forall₂_drop_append — Mathlib

English

If a list l is Forall₂-related to l1 ++ l2, then drop(|l1|) l is Forall₂-related to l2.

Русский

Если список l связан Forall₂ с l1 ++ l2, то drop(|l1|) l связан Forall₂ с l2.

LaTeX

$$$ \forall l:\mathrm{List}\,\alpha\forall l_1:\mathrm{List}\,\beta\forall l_2:\mathrm{List}\,\beta,\ \mathrm{Forall₂}\ R\ l\ (l_1++l_2) \Rightarrow \mathrm{Forall₂}\ R\ (\mathrm{drop}\ (|l_1|)\ l)\ l_2 $$$

Lean4

theorem forall₂_drop_append (l : List α) (l₁ : List β) (l₂ : List β) (h : Forall₂ R l (l₁ ++ l₂)) :
    Forall₂ R (List.drop (length l₁) l) l₂ :=
  by
  have h' : Forall₂ R (drop (length l₁) l) (drop (length l₁) (l₁ ++ l₂)) := forall₂_drop (length l₁) h
  rwa [drop_left] at h'

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