instNonAssocSemiringOfIsTopologicalSemiring

English

The continuous maps C(α, β) form a nonassociative semiring when β is a nonassociative semiring with IsTopologicalSemiring.

Русский

Непрерывные отображения образуют нелинейное полуринг, если β обладает соответствующим топологическим полем.

LaTeX

$$$\text{instNonAssocSemiring}(α,β)$$$

Lean4

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

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