instInv — Mathlib

English

If Y has inverses, LocallyConstant X Y carries an inverse operation defined pointwise by (f^{-1})(x) = (f(x))^{-1}.

Русский

Если у Y есть обратные элементы, LocallyConstant X Y имеет операцию обратного действия, задаваемую по точкам: (f^{-1})(x) = (f(x))^{-1}.

LaTeX

$$$\text{Inv } Y \Rightarrow\ \big( f^{-1} \big)(x) = (f(x))^{-1}$ for all $x$.$$

Lean4

@[to_additive]
instance [Inv Y] : Inv (LocallyConstant X Y) where inv f := ⟨f⁻¹, f.isLocallyConstant.inv⟩

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