English
For any list l1 and l2, SublistForall₂ R l1 l2 holds exactly when there exists a list l such that l1 and l are related by Forall₂ with l1, and l is a sublist of l2. In particular, when R is reflexive, any list l1 is SublistForall₂-related to l2 if l1 is a sublist of l2.
Русский
Для любых списков l1, l2 часть отношения SublistForall₂ R l1 l2 ровно тогда, когда существует список l, для которого l1 и l связаны Forall₂ R и l является подпоследовательностью l2. Если R - рефлексивно, то любой подпоследовательный список удовлетворяет SublistForall₂.
LaTeX
$$$$\\text{SublistForall₂ R l_1 l_2} \\quad\\Leftrightarrow\\quad \\exists l,\\; \\mathrm{Forall_2\\ } R\\ l_1\\ l \\land l\\ <+ l_2.$$$$
Lean4
theorem sublistForall₂_iff {l₁ : List α} {l₂ : List β} : SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂ :=
by
constructor <;> intro h
·
induction h with
| nil => exact ⟨nil, Forall₂.nil, nil_sublist _⟩
| @cons a b l1 l2 rab _ ih =>
obtain ⟨l, hl1, hl2⟩ := ih
exact ⟨b :: l, Forall₂.cons rab hl1, hl2.cons_cons b⟩
| cons_right _ ih =>
obtain ⟨l, hl1, hl2⟩ := ih
exact ⟨l, hl1, hl2.trans (Sublist.cons _ (Sublist.refl _))⟩
· obtain ⟨l, hl1, hl2⟩ := h
revert l₁
induction hl2 with
| slnil =>
intro l₁ hl1
rw [forall₂_nil_right_iff.1 hl1]
exact SublistForall₂.nil
| cons _ _ ih => intro l₁ hl1; exact SublistForall₂.cons_right (ih hl1)
| cons₂ _ _ ih =>
intro l₁ hl1
obtain - | ⟨hr, hl⟩ := hl1
exact SublistForall₂.cons hr (ih hl)
