mkContinuousMultilinear_norm_le — Mathlib

English

The isomorphism maps z to a constant-valued multilinear map; conversely, a multilinear map corresponds to its evaluation at the all-ones vector.

Русский

Изоморфизм отправляет z в константное много-линейное отображение; наоборот, отображение соответствует своему значению на векторе из единиц.

LaTeX

$$$ z \leftrightarrow f_z, \; f_z(i) = z \quad\text{ и } \; f \mapsto f(1,1,...,1) $$$

Lean4

theorem mkContinuousMultilinear_norm_le (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ} (hC : 0 ≤ C)
    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) : ‖mkContinuousMultilinear f C H‖ ≤ C :=
  (mkContinuousMultilinear_norm_le' f C H).trans_eq (max_eq_left hC)

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