mkContinuous_norm_le — Mathlib

English

Constructing a continuous linear map from a bound yields a bound on its operator norm by the maximum with zero.

Русский

Построение непрерывного линейного отображения из ограничений даёт ограничение на его операторную норму максимумом с нулём.

LaTeX

$$$\|f^{\mathrm{mkContinuous}}\| \le \max\{C,0\}$$$

Lean4

/-- If a continuous alternating map is constructed from a alternating map via the constructor
`mkContinuous`, then its norm is bounded by the bound given to the constructor if it is
nonnegative. -/
theorem mkContinuous_norm_le (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ} (hC : 0 ≤ C) (H : ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖) :
    ‖f.mkContinuous C H‖ ≤ C :=
  f.toMultilinearMap.mkContinuous_norm_le hC H

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