English
Composition of partial equivalences respects equivalence: if e ≈ e' and f ≈ f', then e.trans f ≈ e'.trans f'.
Русский
Сложение частичных эквивалентностей сохраняет эквивалентность: если e ≈ e' и f ≈ f', то e.trans f ≈ e'.trans f'.
LaTeX
$$$ (e \\approx e') \\land (f \\approx f') \\Rightarrow e.trans f \\approx e'.trans f' $$$
Lean4
/-- Composition of partial equivs respects equivalence. -/
theorem trans' {e e' : PartialEquiv α β} {f f' : PartialEquiv β γ} (he : e ≈ e') (hf : f ≈ f') :
e.trans f ≈ e'.trans f' := by
constructor
· rw [trans_source'', trans_source'', ← target_eq he, ← hf.1]
exact (he.symm'.eqOn.mono inter_subset_left).image_eq
· intro x hx
rw [trans_source] at hx
simp [Function.comp_apply, PartialEquiv.coe_trans, (he.2 hx.1).symm, hf.2 hx.2]
