le_opENorm

Mathlib.Analysis.Normed.Operator.NNNorm

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

English

Same as above: for any x, the bound holds: ‖f x‖ ≤ ‖f‖ · ‖x‖.

Русский

То же самое: для любого x выполняется ‖f x‖ ≤ ‖f‖ · ‖x‖.

LaTeX

$$$\\|f x\\| ≤ \\|f\\| \\cdot \\|x\\|$$$

Lean4

theorem le_opENorm (f : E →SL[σ₁₂] F) (x : E) : ‖f x‖ₑ ≤ ‖f‖ₑ * ‖x‖ₑ := by dsimp [enorm]; exact mod_cast le_opNNNorm ..

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

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

Разделы

Аффилиация

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