le_of_opNorm_le

Mathlib.Analysis.NormedSpace.Alternating.Basic

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

English

If ‖f‖ ≤ C then ∀ m, ‖f m‖ ≤ C · ∏ ‖m i‖.

Русский

Если ‖f‖ ≤ C, тогда для любого m выполняется ‖f m‖ ≤ C · ∏ ‖m i‖.

LaTeX

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

Lean4

theorem le_of_opNorm_le {C : ℝ} (h : ‖f‖ ≤ C) (m : ι → E) : ‖f m‖ ≤ C * ∏ i, ‖m i‖ :=
  f.1.le_of_opNorm_le h m

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

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

Разделы

Аффилиация

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