norm_compContinuousLinearMapLRight_le

English

The operator norm of compContinuousLinearMapLRight is bounded by the norm of g and the product of the norms of the f_i.

Русский

Норма оператора compContinuousLinearMapLRight ограничена нормой g и произведением норм f_i.

LaTeX

$$$ \|compContinuousLinearMapLRight (E := E) g\| ≤ \|g\| \cdot \prod_i \|f_i\| $$$

Lean4

theorem norm_compContinuousLinearMapLRight_le (g : ContinuousMultilinearMap 𝕜 E₁ G) :
    ‖compContinuousLinearMapLRight (E := E) g‖ ≤ ‖g‖ :=
  MultilinearMap.mkContinuous_norm_le _ (norm_nonneg _) _

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