English
Let f be a bijection between types α and β. Transport along f induces an equivalence φ_f between finitary-support M-valued functions on α and on β; the inverse of φ_f is precisely the transport along f^{-1}. In particular, the isomorphism obtained by transporting along f is invertible with inverse transported along f^{-1}.
Русский
Пусть f — биекция между типами α и β. Перенос вдоль f задаёт взаимно однозначное отображение между функциями с конечной опорой из α в M и из β в M; его обратное отображение совпадает с переносом вдоль f^{-1}. В частности, изотропизм переноса вдоль f имеет обратимый перенос вдоль f^{-1}.
LaTeX
$$$\\bigl(\\operatorname{Transport}_{f} \\bigr)^{-1} = \\operatorname{Transport}_{f^{-1}}.$$$
Lean4
@[simp]
theorem equivCongrLeft_symm (f : α ≃ β) : (@equivCongrLeft _ _ M _ f).symm = equivCongrLeft f.symm :=
rfl
