le_opNorm_mul_prod_of_le — Mathlib

English

If ‖f‖ ≤ C and for all i, ‖m_i‖ ≤ b_i, then ‖f m‖ ≤ C · ∏ b_i.

Русский

Если ‖f‖ ≤ C и для каждого i верно ‖m_i‖ ≤ b_i, то ‖f m‖ ≤ C · ∏ b_i.

LaTeX

$$$$\|f m\| \le C \prod_i b_i,$$ при условии $\|f\| \le C$ и $\|m_i\| \le b_i$.$$

Lean4

theorem le_opNorm_mul_prod_of_le (f : E [⋀^ι]→L[𝕜] F) {b : ι → ℝ} (hm : ∀ i, ‖m i‖ ≤ b i) : ‖f m‖ ≤ ‖f‖ * ∏ i, b i :=
  f.1.le_opNorm_mul_prod_of_le hm

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