instNorm — Mathlib

English

The norm on the based function space C(α,R)₀ is defined by the norm of the underlying continuous map: ‖f‖ := ‖(f : C(α,R))‖.

Русский

Норма пространства неподвижных отображений C(α,R)₀ задаётся как норма соответствующего непрерывного отображения: ‖f‖ := ‖(f : C(α,R))‖.

LaTeX

$$$\\|f\\| = \\|(f : C(α, R))\\|$$$

Lean4

noncomputable instance [NormedAddCommGroup R] : Norm C(α, R)₀ where norm f := ‖(f : C(α, R))‖

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