English
A family of pointwise equivalences F(a) between β1(a) and β2(a) yields an equivalence between the function spaces ∀a,β1(a) and ∀a,β2(a).
Русский
Пара отождествлений F(a): β1(a) ≃ β2(a) задаёт эквивалентность между пространствами функций ∀a, β1(a) и ∀a, β2(a).
LaTeX
$$$$ (\\forall a, β_1(a) \\cong β_2(a)) \\;\\Rightarrow\\; (\\forall a, β_1(a)) \\cong (\\forall a, β_2(a)). $$$$
Lean4
/-- A family of equivalences `∀ a, β₁ a ≃ β₂ a` generates an equivalence between `∀ a, β₁ a` and
`∀ a, β₂ a`. -/
@[simps]
def piCongrRight {β₁ β₂ : α → Sort*} (F : ∀ a, β₁ a ≃ β₂ a) : (∀ a, β₁ a) ≃ (∀ a, β₂ a) :=
⟨Pi.map fun a ↦ F a, Pi.map fun a ↦ (F a).symm, fun H => funext <| by simp, fun H => funext <| by simp⟩
