English
Let eα: α₁ ≃ α₂ and eβ: β₁ ≃ β₂. If h relates p and q by p x y ↔ q (eα x) (eβ y), then (∀ x y, p x y) ↔ ∀ x y, q x y.
Русский
Пусть eα: α₁ ≃ α₂ и eβ: β₁ ≃ β₂. Если h связывает p и q через p x y ↔ q (eα x) (eβ 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 _1} {y:\beta _1},\ p x y \leftrightarrow q (eα x) (eβ 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 x y ↔ q (eα x) (eβ y)) : (∀ x y, p x y) ↔ ∀ x y, q x y :=
eα.forall_congr fun _ ↦ eβ.forall_congr <| @h _
