instNorm — Mathlib

English

Let α be a compact space and E a seminormed additive group. The space C(α, E) of continuous maps from α to E is equipped with the norm defined by the supremum of pointwise norms: for f ∈ C(α, E), ‖f‖ = sup_{x∈α} ‖f(x)‖ (equivalently, ‖f‖ = dist(f, 0)).

Русский

Пусть α - компактное пространсто, E - полугруппа с нормой. Пространство C(α, E) непрерывных отображений обладает нормой, равной супремуму нормы значений: ‖f‖ = sup_{x∈α} ‖f(x)‖ (а также ‖f‖ = dist(f, 0)).

LaTeX

$$$\|f\| = \sup_{x \in \alpha} \|f(x)\|$$$

Lean4

instance : Norm C(α, E) where norm x := dist x 0

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