instSeminormedRing

Mathlib.Topology.ContinuousMap.Compact

URI: https://scilib.ai/kg/mathlib#ContinuousMap.instSeminormedRing

← MathLib Explorer

English

If R is a SeminormedRing, then C(α,R) is a SeminormedRing with pointwise operations.

Русский

Если R — SeminormedRing, тогда C(α,R) — SeminormedRing с точечно заданными операциями.

LaTeX

$$$C(\alpha,R) \text{ is a SeminormedRing}$$$

Lean4

instance [SeminormedRing R] : SeminormedRing C(α, R)
    where
  __ : NonUnitalSeminormedRing C(α, R) := inferInstance
  __ : Ring C(α, R) := inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru