English
Forall₂ (λ a b, p(a) ∧ R a b) l u holds iff (∀ a ∈ l, p(a)) ∧ Forall₂ R l u.
Русский
Forall₂ (λ a b, p(a) ∧ R a b) l u выполняется тогда и только тогда, когда (∀ a ∈ l, p(a)) и Forall₂ R l u.
LaTeX
$$$$ \\forall {l\\,u},\\ Forall₂ (\\\\lambda a b, p(a) \\\\land R a b) l u \\iff (\\\\forall a \\\\in l, p(a)) \\\\land Forall₂ R l u. $$$$
Lean4
theorem forall₂_and_left {p : α → Prop} : ∀ l u, Forall₂ (fun a b => p a ∧ R a b) l u ↔ (∀ a ∈ l, p a) ∧ Forall₂ R l u
| [], u => by simp only [forall₂_nil_left_iff, forall_prop_of_false not_mem_nil, imp_true_iff, true_and]
| a :: l, u =>
by
simp only [forall₂_and_left l, forall₂_cons_left_iff, forall_mem_cons, and_assoc, exists_and_left]
simp only [and_comm, and_assoc, ← exists_and_right]
