norm_map_cons_le — Mathlib

English

A bound for the cons operation of a multilinear map: the norm of f(cons x m) is at most the product of ‖f‖, ‖x‖, and ∏ ‖m_i‖.

Русский

Для cons: норма f(cons x m) не превосходит ‖f‖ · ‖x‖ · ∏ ‖m_i‖.

LaTeX

$$$\|f(\text{cons } x\; m)\| \leq \|f\| \cdot \|x\| \cdot \prod_i \|m_i\|$$$

Lean4

theorem norm_map_cons_le (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei 0) (m : ∀ i : Fin n, Ei i.succ) :
    ‖f (cons x m)‖ ≤ ‖f‖ * ‖x‖ * ∏ i, ‖m i‖ := by simpa [prod_univ_succ, mul_assoc] using f.le_opNorm (cons x m)

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