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