ofFun_inv — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem ofFun_inv [Inv β] (f : α → β) : ofFun (f⁻¹) = (ofFun f)⁻¹ :=
  rfl

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