instNonUnitalSeminormedRing — Mathlib

English

If β is a non-unital seminormed ring, then C0(α,β) inherits a non-unital seminormed ring structure.

Русский

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

LaTeX

$$[NonUnitalSeminormedRing β] ⇒ NonUnitalSeminormedRing C0(α,β)$$

Lean4

noncomputable instance instNonUnitalSeminormedRing [NonUnitalSeminormedRing β] : NonUnitalSeminormedRing C₀(α, β) :=
  { instNonUnitalRing, instSeminormedAddCommGroup with norm_mul_le f g := norm_mul_le f.toBCF g.toBCF }

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