English
A canonical equality holds between transPartialEquiv and trans: the composed PartialEquiv equals the translation of the composed Equivalences.
Русский
Существует каноническое равенство между transPartialEquiv и trans: композиция PartialEquiv равна трансляции композиции эквивалентностей.
LaTeX
$$$e.\\text{transPartialEquiv } f' = e.\\text{toPartialEquiv}.trans f'$$$
Lean4
/-- Precompose a partial equivalence with an equivalence.
We modify the source and target to have better definitional behavior. -/
@[simps!]
def transPartialEquiv (e : α ≃ β) (f' : PartialEquiv β γ) : PartialEquiv α γ :=
(e.toPartialEquiv.trans f').copy _ rfl _ rfl (e ⁻¹' f'.source) (univ_inter _) f'.target (inter_univ _)
