norm_alternatizeUncurryFinCLM_le — Mathlib

English

The operator norm of the linear map alternatizeUncurryFinCLM (n := n) 𝕜 E F is at most n + 1.

Русский

Операционная норма линейного отображения alternatizeUncurryFinCLM (n := n) над полем 𝕜 в пространствах E и F не превышает n + 1.

LaTeX

$$$\\| \\operatorname{alternatizeUncurryFinCLM}_{\\mathbb{k},E,F} \\| \\le n + 1$$$

Lean4

theorem norm_alternatizeUncurryFinCLM_le : ‖alternatizeUncurryFinCLM (n := n) 𝕜 E F‖ ≤ n + 1 :=
  by
  rw [alternatizeUncurryFinCLM]
  apply AlternatingMap.mkContinuousLinear_norm_le
  positivity

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