instInvUniformOnFun — Mathlib

English

If β has an inversion, the UniformOnFun α β 𝔖 inherits an inverse operation, defined pointwise by (f)(a)^{-1} at each a ∈ α.

Русский

Если β имеет обратное, то UniformOnFun α β 𝔖 наследует операцию инверсии, определяемую по точкам: (f)^{-1}(a) = f(a)^{-1} для каждого a.

LaTeX

$$$ (f^{-1})(a) = f(a)^{-1} \quad \text{for all } a. $$$

Lean4

@[to_additive]
instance [Inv β] : Inv (α →ᵤ[𝔖] β) :=
  Pi.instInv

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