English
Swapping the two pairs of indices in a four-ary existential quantification does not change the statement: ∃ i1 j1 i2 j2, p i1 j1 i2 j2 ⇔ ∃ i2 j2 i1 j1, p i1 j1 i2 j2.
Русский
Поменяв порядок двух пар индексов в четырехместной квантификации существования, получаем эквивалентность: ∃ i1 j1 i2 j2, p i1 j1 i2 j2 ⇔ ∃ i2 j2 i1 j1, p i1 j1 i2 j2.
LaTeX
$$$$\\exists i_1\\, j_1\\, i_2\\, j_2,\\; p(i_1, j_1, i_2, j_2) \\iff \\exists i_2\\, j_2\\, i_1\\, j_1,\\; p(i_1, j_1, i_2, j_2).$$$$
Lean4
theorem exists₂_comm {ι₁ ι₂ : 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₂ := by simp only [@exists_comm (κ₁ _), @exists_comm ι₁]
