English
A family of fiberwise equivalences F(a): β1(a) ≃ β2(a) yields an equivalence between the dependent sums ∑' a, β1(a) and ∑' a, β2(a).
Русский
families эквивалентностей по волокнам F(a): β1(a) ≃ β2(a) порождают эквивалентность между зависимыми суммами ∑' a, β1(a) и ∑' a, β2(a).
LaTeX
$$$$(\Sigma' a:\alpha, \beta_1(a)) \cong (\Sigma' a:\alpha, \beta_2(a)).$$$$
Lean4
/-- A family of equivalences `Π a, β₁ a ≃ β₂ a` generates an equivalence between `Σ' a, β₁ a` and
`Σ' a, β₂ a`. -/
@[simps (attr := grind =) apply]
def psigmaCongrRight {β₁ β₂ : α → Sort*} (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
