unit_le_opNorm

Mathlib.Analysis.NormedSpace.Alternating.Basic

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

← MathLib Explorer

English

If ‖m‖ ≤ 1, then ‖f m‖ ≤ ‖f‖.

Русский

Если ‖m‖ ≤ 1, то ‖f m‖ ≤ ‖f‖.

LaTeX

$$$$\|f m\| \le \|f\|.$$$$

Lean4

/-- The image of the unit ball under a continuous alternating map is bounded. -/
theorem unit_le_opNorm (f : E [⋀^ι]→L[𝕜] F) (h : ‖m‖ ≤ 1) : ‖f m‖ ≤ ‖f‖ :=
  f.1.unit_le_opNorm h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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