normedSpace — Mathlib

English

If 𝕜 is a NormedField and γ is a NormedAlgebra, then C(α, γ) forms a NormedAlgebra over 𝕜 when α is compact and α is a compact space.

Русский

Пусть 𝕜 - нормированное поле, а γ - нормированная алгебра; тогда C(α, γ) образует нормированную алгебру над 𝕜, если пространство α компактно.

LaTeX

$$$C(\alpha, \gamma)$ is a NormedAlgebra over 𝕜 with pointwise operations and the sup-norm.$$

Lean4

instance normedSpace {𝕜 : Type*} [NormedField 𝕜] [NormedSpace 𝕜 E] : NormedSpace 𝕜 C(α, E) where
  norm_smul_le := norm_smul_le

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