English
A partial equivalence e determines a canonical equivalence between its source e.source and its target e.target, with the forward map x ↦ e x and inverse map y ↦ e.symm y.
Русский
Частичное эквивное отображение e задаёт естественную эквив между областью определения e.source и областью значений e.target, с переходом x ↦ e x и обратным отображением y ↦ e.symm y.
LaTeX
$$$e.source \simeq e.target$$$
Lean4
/-- Associate to a `PartialEquiv` an `Equiv` between the source and the target. -/
protected def toEquiv : e.source ≃ e.target
where
toFun x := ⟨e x, e.map_source x.mem⟩
invFun y := ⟨e.symm y, e.map_target y.mem⟩
left_inv := fun ⟨_, hx⟩ => Subtype.eq <| e.left_inv hx
right_inv := fun ⟨_, hy⟩ => Subtype.eq <| e.right_inv hy
