norm_toContinuousMap_eq — Mathlib

English

For any f ∈ α →ᵇ E (bounded continuous functions), the norm of its associated continuous map equals the norm of f: ‖f.toContinuousMap‖ = ‖f‖.

Русский

Для любого f ∈ α →ᵇ E нормa соответствующего непрерывного отображения равна норме f: ‖f.toContinuousMap‖ = ‖f‖.

LaTeX

$$$\|f.\mathrm{toContinuousMap}\| = \|f\|$$$

Lean4

@[simp]
theorem _root_.BoundedContinuousFunction.norm_toContinuousMap_eq (f : α →ᵇ E) : ‖f.toContinuousMap‖ = ‖f‖ :=
  rfl

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