English
A family of equivalences F(a): β1(a) ≃ β2(a) induces an equivalence between the dependent sums Σ a, β1(a) and Σ a, β2(a).
Русский
Семейство эквивалентностей по основаниям F(a): β1(a) ≃ β2(a) порождает эквивалентность между зависимыми суммами Σ a, β1(a) и Σ a, β2(a).
LaTeX
$$$$ (\Sigma a, β_1 a) \cong (\Sigma a, β_2 a). $$$$
Lean4
/-- A family of equivalences `Π a, β₁ a ≃ β₂ a` generates an equivalence between `Σ a, β₁ a` and
`Σ a, β₂ a`. -/
@[simps (attr := grind =) apply]
def sigmaCongrRight {α} {β₁ β₂ : α → Type*} (F : ∀ a, β₁ a ≃ β₂ a) : (Σ a, β₁ a) ≃ Σ a, β₂ a
where
toFun a := ⟨a.1, F a.1 a.2⟩
invFun a := ⟨a.1, (F a.1).symm a.2⟩
left_inv := by grind
right_inv := by grind
