English
Let eα: α₁ ≃ α₂ and eβ: β₁ ≃ β₂. If h relates p (eα x) (eβ y) ↔ q x y, then (∀ x y, p x y) ↔ ∀ x y, q x y.
Русский
Пусть eα: α₁ ≃ α₂ и eβ: β₁ ≃ β₂. Если h связывает p (eα x) (eβ y) ↔ q x y, то (∀ x y, p x y) ↔ (∀ x y, q x y).
LaTeX
$$$ \forall eα:(\alpha _1 \simeq \alpha _2) \ \forall eβ:(\beta _1 \simeq \beta _2),\ (\forall {x:\alpha _2} {y:\beta _2},\ p (eα x) (eβ y) \leftrightarrow q x y) \rightarrow (\forall x:\alpha _1) (\forall y:\beta _1,\ p x y) \leftrightarrow (\forall x:\alpha _2) (\forall y:\beta _2,\ q x y) $$$
Lean4
protected theorem forall₂_congr' {α₁ α₂ β₁ β₂ : Sort*} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop} (eα : α₁ ≃ α₂)
(eβ : β₁ ≃ β₂) (h : ∀ {x y}, p (eα.symm x) (eβ.symm y) ↔ q x y) : (∀ x y, p x y) ↔ ∀ x y, q x y :=
(Equiv.forall₂_congr eα.symm eβ.symm h.symm).symm
