instIsTopologicalSemiringOfLocallyCompactSpace

English

If α is locally compact and β is a nonunital semiring with IsTopologicalSemiring, then the continuous maps C(α, β) carry an IsTopologicalSemiring structure.

Русский

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

LaTeX

$$$ IsTopologicalSemiring\ C(\alpha, \beta) \text{ holds when } α\text{ locally compact and } β\text{ is a nonunital semiring with } IsTopologicalSemiring. $$$

Lean4

instance {α : Type*} {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [LocallyCompactSpace α] [NonUnitalSemiring β]
    [IsTopologicalSemiring β] : IsTopologicalSemiring C(α, β) where

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