transEquiv_eq_trans — Mathlib

English

If e is a PartialEquiv and e' an Equiv, then transEquiv coincides with trans on the corresponding PartialEquiv.

Русский

Если e — PartialEquiv, а e' — Equiv, то transEquiv согласуется с trans через соответствующий PartialEquiv.

LaTeX

$$$e.transEquiv e' = e.toPartialEquiv.trans e'.toPartialEquiv$$$

Lean4

theorem transEquiv_eq_trans (e : PartialEquiv α β) (e' : β ≃ γ) : e.transEquiv e' = e.trans e'.toPartialEquiv :=
  copy_eq ..

Похожие утверждения