instSeminormedAddCommGroup — Mathlib

English

The space C0(α,β) inherits a seminormed additively structured group when β is a seminormed additive group.

Русский

Пространство C0(α,β) наследует структуру полугруппы с полугрупповой нормой, когда β—полугруппа с полугрупповой нормой.

LaTeX

$$SeminormedAddCommGroup(C0(α,β))$$

Lean4

noncomputable instance instSeminormedAddCommGroup [SeminormedAddCommGroup β] : SeminormedAddCommGroup C₀(α, β) :=
  fast_instance%SeminormedAddCommGroup.induced _ _ (⟨⟨toBCF, rfl⟩, fun _ _ => rfl⟩ : C₀(α, β) →+ α →ᵇ β)

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