unit_le_opNorm

Mathlib.Analysis.Normed.Operator.Basic

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

← MathLib Explorer

English

If ∥x∥ ≤ 1, then ∥f x∥ ≤ ∥f∥.

Русский

Если ∥x∥ ≤ 1, то ∥f x∥ ≤ ∥f∥.

LaTeX

$$$\\|x\\| \\le 1 \\Rightarrow \\|f x\\| \\le \\|f\\|$$$

Lean4

/-- The image of the unit ball under a continuous linear map is bounded. -/
theorem unit_le_opNorm : ‖x‖ ≤ 1 → ‖f x‖ ≤ ‖f‖ :=
  mul_one ‖f‖ ▸ f.le_opNorm_of_le

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

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

Разделы

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

Аффилиация

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