toFun_inv — Mathlib

English

For f in α →ᵤ[𝔖] β with Inv β, the evaluation of the inverse is the inverse of the evaluation: toFun 𝔖 (f^{-1}) = (toFun 𝔖 f)^{-1}.

Русский

Для f ∈ α →ᵤ[𝔖] β с Inv β: toFun 𝔖 (f^{-1}) = (toFun 𝔖 f)^{-1}.

LaTeX

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

Lean4

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

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