instNonUnitalNonAssocSemiringOfIsTopologicalSemiring

English

If β is a NonUnitalSemiring with IsTopologicalSemiring, then C_c(α,β) inherits a NonUnitalSemiring structure via pointwise addition and multiplication.

Русский

Если β — NonUnitalSemiring и IsTopologicalSemiring, то C_c(α,β) получает структуру NonUnitalSemiring через точечное сложение и умножение.

LaTeX

$$$$ (f+g)(x) = f(x)+g(x), \ (f\cdot g)(x) = f(x)\cdot g(x) $$$$

Lean4

instance [NonUnitalNonAssocSemiring β] [IsTopologicalSemiring β] : NonUnitalNonAssocSemiring C_c(α, β) :=
  DFunLike.coe_injective.nonUnitalNonAssocSemiring _ coe_zero coe_add coe_mul fun _ _ => rfl

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