English
Let p be a predicate taking four arguments a, b, c, d from two index families. Then the universal quantification over all four arguments is equivalent to the universal quantification after swapping the two pairs of arguments: ∀ i1, j1, i2, j2, p i1 j1 i2 j2 ⇔ ∀ i2, j2, i1, j1, p i1 j1 i2 j2.
Русский
Пусть p — предикат, зависящий от четырех аргументов; тогда всеобщность по всем четырем аргументам эквивалентна всеобщности после обмена двух первых и двух вторых пар аргументов: ∀ i1, j1, i2, j2, p i1 j1 i2 j2 ⇔ ∀ i2, j2, i1, j1, p i1 j1 i2 j2.
LaTeX
$$$$\\left(\\forall i_1 j_1 i_2 j_2,\\; p\\,i_1\\,j_1\\,i_2\\,j_2\\right) \\Longleftrightarrow \\left(\\forall i_2 j_2 i_1 j_1,\\; p\\,i_1\\,j_1\\,i_2\\,j_2\\right).$$$$
Lean4
theorem forall₂_swap {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} {p : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Prop} :
(∀ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∀ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂ :=
⟨swap₂, swap₂⟩
