ratio_le_opNorm

Mathlib.Analysis.NormedSpace.Alternating.Basic

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

English

If for all m, ‖f m‖ ≤ M · ∏ ‖m i‖, then ‖f‖ ≤ M.

Русский

Если для всех m выполняется ‖f m‖ ≤ M · ∏ ‖m i‖, то ‖f‖ ≤ M.

LaTeX

$$$$\|f\| \le M.$$$$

Lean4

theorem ratio_le_opNorm (f : E [⋀^ι]→L[𝕜] F) (m : ι → E) : ‖f m‖ / ∏ i, ‖m i‖ ≤ ‖f‖ :=
  f.1.ratio_le_opNorm m

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

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

Разделы

Аффилиация

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