opNorm_le_bound — Mathlib

English

For C ≥ 0, ‖f‖ ≤ C if and only if ∀ m, ‖f m‖ ≤ C · ∏ ‖m i‖.

Русский

Для C ≥ 0 верно: ‖f‖ ≤ C тогда и только тогда, когда ∀ m, ‖f m‖ ≤ C · ∏ ‖m i‖.

LaTeX

$$$$\|f\| \le C \;\iff\; \forall m, \|f m\| \le C \prod_i \|m_i\|.$$$$

Lean4

/-- If one controls the norm of every `f x`, then one controls the norm of `f`. -/
theorem opNorm_le_bound (f : E [⋀^ι]→L[𝕜] F) {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ m, ‖f m‖ ≤ M * ∏ i, ‖m i‖) : ‖f‖ ≤ M :=
  f.1.opNorm_le_bound hMp hM

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