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