English
If e: α ⇄ β and e': β ⇄ γ with e.target = e'.source, the composed partial equivalence e trans' e' from α to γ has toFun = e' ∘ e, invFun = e.symm ∘ e'.symm, source = e.source, target = e'.target.
Русский
Если e: α ⇄ β и e': β ⇄ γ с e.target = e'.source, образующееся частичное эквивалентное отображение e trans' e' имеет toFun = e' ∘ e, invFun = e.symm ∘ e'.symm, source = e.source, target = e'.target.
LaTeX
$$$\text{If } e:\PartialEquiv(\alpha,\beta),\ e':\PartialEquiv(\beta,\gamma),\ e.target = e'.source,\ \text{then }(e'\circ e)\in\PartialEquiv(\alpha,\gamma)$$$
Lean4
/-- Composing two partial equivs if the target of the first coincides with the source of the
second. -/
@[simps]
protected def trans' (e' : PartialEquiv β γ) (h : e.target = e'.source) : PartialEquiv α γ
where
toFun := e' ∘ e
invFun := e.symm ∘ e'.symm
source := e.source
target := e'.target
map_source' x hx := by simp [← h, hx]
map_target' y hy := by simp [h, hy]
left_inv' x hx := by simp [hx, ← h]
right_inv' y hy := by simp [hy, h]
