le_opNorm — Mathlib

English

For any input m, the inequality ‖f m‖ ≤ ‖f‖ · ∏ i ‖m i‖ holds.

Русский

Для любого входа m выполняется неравенство ‖f m‖ ≤ ‖f‖ · ∏_i ‖m_i‖.

LaTeX

$$$$\|f m\| \le \|f\| \cdot \prod_i \|m_i\|.$$$$

Lean4

/-- The fundamental property of the operator norm of a continuous alternating map:
`‖f m‖` is bounded by `‖f‖` times the product of the `‖m i‖`. -/
theorem le_opNorm (f : E [⋀^ι]→L[𝕜] F) (m : ι → E) : ‖f m‖ ≤ ‖f‖ * ∏ i, ‖m i‖ :=
  f.1.le_opNorm m

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