instSemigroup — Mathlib

English

If Y has a semigroup structure, then the LocallyConstant X Y inherit a semigroup structure with the product defined pointwise: (f * g)(x) = f(x) · g(x).

Русский

Если Y имеет структуру полугруппы, то LocallyConstant X Y inherits такую же полугруппу, где умножение определяется по точкам: (f · g)(x) = f(x) · g(x).

LaTeX

$$$\forall f,g:\mathrm{LocallyConstant}(X,Y),\; (f*g)(x) = f(x)\,g(x).$$$

Lean4

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

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