English
Let α, β be types with Membership, and s ⊆ β. Then (∀ a (a ∈ s) ∀ b (b ∈ s), p a b) is equivalent to (∀ a b, a ∈ s → b ∈ s → p a b).
Русский
Пусть α, β — множества, и есть отношение членства ⊆ β; тогда (∀ a ∈ s) (∀ b ∈ s) p(a,b) эквивалентно (∀ a b, a ∈ s → b ∈ s → p(a,b)).
LaTeX
$$$(\\\\forall a \\\\_:{a} \\\\in s) \\\\to (\\\\forall b \\\\_:{b} \\\\in s) p(a,b)\\\\iff\\\\(\\\\forall a b, a \\\\in s \\\\to b \\\\in s \\\\to p(a,b))$$$
Lean4
theorem forall_mem_comm {α β} [Membership α β] {s : β} {p : α → α → Prop} :
(∀ a (_ : a ∈ s) b (_ : b ∈ s), p a b) ↔ ∀ a b, a ∈ s → b ∈ s → p a b :=
forall_cond_comm
