English
Transporting a sigma type through an equivalence of the base: (sigmaCongrLeft' f).
Русский
Перемещаем сигма-тип через эквивалентность основания: (sigmaCongrLeft' f).
LaTeX
$$$${\text{sigmaCongrLeft'}(f): (\Sigma a_1, \beta a) \\cong (\Sigma a_2, \beta (f^{-1} a))}.$$$$
Lean4
/-- An equivalence `f : α₁ ≃ α₂` generates an equivalence between `Σ a, β (f a)` and `Σ a, β a`. -/
@[simps (attr := grind =) apply]
def sigmaCongrLeft {α₁ α₂ : Type*} {β : α₂ → Sort _} (e : α₁ ≃ α₂) : (Σ a : α₁, β (e a)) ≃ Σ a : α₂, β a
where
toFun a := ⟨e a.1, a.2⟩
invFun a := ⟨e.symm a.1, (e.right_inv' a.1).symm ▸ a.2⟩
left_inv := fun ⟨a, b⟩ => by simp
right_inv := fun ⟨a, b⟩ => by simp
