English
Let α be a type, s a predicate on α, and p a binary relation on α. Then (for all a with s(a)) (for all b with s(b)) p(a,b) holds iff for all a,b, s(a) → s(b) → p(a,b).
Русский
Пусть α — множество, s — предикат на α, и p — бинарная relation. Тогда (∀ a, s(a) → ∀ b, s(b) → p(a,b)) эквивалентно (∀ a b, s(a) → s(b) → p(a,b)).
LaTeX
$$$\\Big(\\forall a, s(a) \\to \\forall b, s(b) \\to p(a,b)\\Big)\\\\iff\\Big(\\\\forall a\\\\ b, s(a) \\\\to s(b) \\\\to p(a,b)\\\\Big)$$$
Lean4
theorem forall_cond_comm {α} {s : α → Prop} {p : α → α → Prop} :
(∀ a, s a → ∀ b, s b → p a b) ↔ ∀ a b, s a → s b → p a b :=
⟨fun h a b ha hb ↦ h a ha b hb, fun h a ha b hb ↦ h a b ha hb⟩
