instAddMonoidWithOne — Mathlib

English

If Y is AddMonoidWithOne, LocallyConstant X Y inherits AddMonoidWithOne with pointwise addition and unit given by the constant-one function.

Русский

Если Y имеет AddMonoidWithOne, LocallyConstant X Y наследует AddMonoidWithOne, где сложение точечное, единица — константная единица.

LaTeX

$$$\forall f,g:\mathrm{LocallyConstant}(X,Y),\; (f+g)(x) = f(x) + g(x),\; 0_{\mathrm{LocConst}}(x) = 0_Y,\; 1_{\mathrm{LocConst}}(x) = 1_Y.$$$

Lean4

instance [AddMonoidWithOne Y] : AddMonoidWithOne (LocallyConstant X Y) :=
  Function.Injective.addMonoidWithOne DFunLike.coe DFunLike.coe_injective' rfl rfl (fun _ _ => rfl) (fun _ _ => rfl)
    fun _ => rfl

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