English
Mapping the right side of a Forall₂ relation through a function f preserves Forall₂ with the right-mapped second component.
Русский
Отображение по правой стороне отношения Forall₂ через функцию f сохраняет Forall₂ между списками по правой стороне.
LaTeX
$$$$\\text{MapRightForall2: } SublistForall₂\\ R\\ l_1\\ (\\mathrm{map}\\ f\\ l_2) \\iff SublistForall₂\\ (\\lambda a c. R a (f c))\\ l_1\\ l_2 $$$$
Lean4
@[simp]
theorem sublistForall₂_map_right_iff {f : γ → β} {l₁ : List α} {l₂ : List γ} :
SublistForall₂ R l₁ (map f l₂) ↔ SublistForall₂ (fun a c => R a (f c)) l₁ l₂ :=
by
simp only [sublistForall₂_iff]
constructor
· rintro ⟨l1, h1, h2⟩
obtain ⟨l', hl1, rfl⟩ := sublist_map_iff.mp h2
use l'
simpa [hl1] using h1
· rintro ⟨l1, h1, h2⟩
use l1.map f
simp [h1, h2.map]
