toFun_inv — Mathlib

English

If β has an inversion, then the evaluation of the inverse is the inverse of the evaluation: toFun(f^{-1}) = (toFun f)^{-1}.

Русский

Если в β существует обращение, то значение f^{-1} под toFun равно обратному значения f: toFun(f^{-1}) = (toFun f)^{-1}.

LaTeX

$$$\operatorname{toFun}(f^{-1}) = (\operatorname{toFun} f)^{-1}. $$$

Lean4

@[to_additive (attr := simp)]
theorem toFun_inv [Inv β] (f : α →ᵤ β) : toFun (f⁻¹) = (toFun f)⁻¹ :=
  rfl

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