norm_def — Mathlib

English

The norm on C(α,R)₀ coincides with the norm of the underlying continuous map; this is an immediate consequence of how the norm is defined via the ambient space.

Русский

Норма на C(α,R)₀ совпадает с нормой соответствующего непрерывного отображения в зачении пространства C(α,R).

LaTeX

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

Lean4

theorem norm_def [NormedAddCommGroup R] (f : C(α, R)₀) : ‖f‖ = ‖(f : C(α, R))‖ :=
  rfl

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