English
Let R be a relation on α×β and f a function γ → β. For any lists l of α and u of γ, we have Forall₂ R l (map f u) is equivalent to Forall₂ (λ a c, R a (f c)) l u.
Русский
Пусть R — отношение на α×β, и f: γ → β. Для любых списков l ⊆ α и u ⊆ γ имеем: Forall₂ R l (map f u) эквивалентно Forall₂ (λ a c, R a (f c)) l u.
LaTeX
$$$ \forall f:\gamma \to \beta,\ \forall l:\mathrm{List}\;\alpha,\ \forall u:\mathrm{List}\;\gamma,\ \mathrm{Forall₂}\ R\ l\ (\mathrm{map}\ f\ u)\ \iff\ \mathrm{Forall₂}\ (\lambda a\, c.\ R\ a\ (f\ c))\ l\ u $$$
Lean4
@[simp]
theorem forall₂_map_right_iff {f : γ → β} : ∀ {l u}, Forall₂ R l (map f u) ↔ Forall₂ (fun a c => R a (f c)) l u
| _, [] => by simp only [map, forall₂_nil_right_iff]
| _, b :: u => by simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]
