instSemiringOfIsTopologicalSemiring

English

If β is a semiring with IsTopologicalSemiring, then C(α, β) is a semiring under pointwise operations.

Русский

Если β — полукольцо с IsTopologicalSemiring, то C(α, β) образует полукольцо по точечному умножению и сложению.

LaTeX

$$$\text{Semiring}(C(α,β))$$$

Lean4

instance {α : Type*} {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [Semiring β] [IsTopologicalSemiring β] :
    Semiring C(α, β) :=
  coe_injective.semiring _ coe_zero coe_one coe_add coe_mul coe_nsmul coe_pow coe_natCast

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