opNorm_le_iff

Mathlib.Analysis.NormedSpace.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousAlternatingMap.opNorm_le_iff

English

Using NNReal norms, ‖f m‖₊ ≤ ‖f‖₊ · ∏ ‖m i‖₊ for all inputs m.

Русский

С использованием nnnorm: ‖f m‖₊ ≤ ‖f‖₊ · ∏ ‖m_i‖₊ для всех входов m.

LaTeX

$$$$\|f m\|_{+} \le \|f\|_{+} \cdot \prod_i \|m_i\|_{+}.$$$$

Lean4

theorem opNorm_le_iff {C : ℝ} (hC : 0 ≤ C) : ‖f‖ ≤ C ↔ ∀ m, ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
  f.1.opNorm_le_iff hC

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru