mkContinuousMultilinear_norm_le' — Mathlib

English

The evaluation of the continuous multilinear map produced by mkContinuousMultilinear at m equals the original multilinear map evaluated at m.

Русский

Значение отображения, полученного через mkContinuousMultilinear, в аргументе m совпадает с исходным отображением, вычисленным на m.

LaTeX

$$$ (mkContinuousMultilinear f C H) \; m = f(m) $$$

Lean4

theorem mkContinuousMultilinear_norm_le' (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ)
    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) : ‖mkContinuousMultilinear f C H‖ ≤ max C 0 :=
  by
  dsimp only [mkContinuousMultilinear]
  exact mkContinuous_norm_le _ (le_max_right _ _) _

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