English
Associativity of transPartialEquiv: composing with another partial equivalence on the right distributes as a single transPartialEquiv of the composed Equiv.
Русский
Ассоциативность transPartialEquiv: присоединение справа к частичной эквивалентности распространяется как единый transPartialEquiv от составной эквивалентности.
LaTeX
$$$\\forall e:\\PartialEquiv, f', f''$;\\ $(e.transPartialEquiv f').transPartialEquiv f'' = e.transPartialEquiv (f'.transPartialEquiv f'')$$$
Lean4
@[simp, mfld_simps]
theorem transPartialEquiv_trans (e : α ≃ β) (f' : PartialEquiv β γ) (f'' : PartialEquiv γ δ) :
(e.transPartialEquiv f').trans f'' = e.transPartialEquiv (f'.trans f'') := by
simp only [transPartialEquiv_eq_trans, PartialEquiv.trans_assoc]
