instGroup — Mathlib

English

If Y is a Group, LocallyConstant X Y inherits a Group structure with pointwise inversion.

Русский

Если Y — группа, LocallyConstant X Y наследует структуру группы с точечной операцией взятия обратного.

LaTeX

$$$\forall f:\mathrm{LocallyConstant}(X,Y),\; f^{-1}(x) = (f(x))^{-1}.$$$

Lean4

@[to_additive]
instance [Group Y] : Group (LocallyConstant X Y) :=
  Function.Injective.group DFunLike.coe DFunLike.coe_injective' rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl)

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