English
ContinuousMulEquiv M N carries an EquivLike structure, with coe f = f.toFun, inv f = f.invFun, left_inv f = f.left_inv, right_inv f = f.right_inv.
Русский
Объекты ContinuousMulEquiv между M и N образуют структуру EquivLike: сопряжение функций, обратное отображение и соответствующая когерентность через toFun, invFun, left_inv, right_inv.
LaTeX
$$$\text{EquivLike}(\mathrm{ContinuousMulEquiv}\,M\,N)\,M\,N\quad\text{with }\mathrm{coe}(f)=f\!\toFun,\ \mathrm{inv}(f)=f\!\invFun,\ \mathrm{left\_inv}(f)=f\!\leftinv,\ \mathrm{right\_inv}(f)=f\!\rightinv.$$$
Lean4
@[to_additive]
instance : EquivLike (M ≃ₜ* N) M N where
coe f := f.toFun
inv f := f.invFun
left_inv f := f.left_inv
right_inv f := f.right_inv
coe_injective' f g h₁
h₂ := by
cases f
cases g
congr
exact MulEquiv.ext_iff.mpr (congrFun h₁)
