instStarRingOfContinuousStar — Mathlib

English

If β is a StarRing with ContinuousStar, then C(α, β) inherits a StarRing structure with the star operation defined pointwise.

Русский

Если β — звездо-кольцо с непрерывной звездой, то C(α, β) наследует структуру звездного кольца, звезда действует по точкам.

LaTeX

$$$\mathrm{StarRing}\bigl(C(\alpha, \beta)\bigr)$$$

Lean4

instance [NonUnitalNonAssocSemiring β] [IsTopologicalSemiring β] [StarRing β] [ContinuousStar β] : StarRing C(α, β) :=
  { ContinuousMap.starAddMonoid, ContinuousMap.starMul with }

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