norm_smulRightL_le

Mathlib.Analysis.Normed.Operator.NormedSpace

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

English

Equivalence between ennorm and operator norm for isomorphisms.

Русский

Эквивалентность между ènorm и операторной нормой для изоморфизмов.

LaTeX

$$$\\|f\\|_{toCLM} = 1$ in appropriate setups.$$

Lean4

theorem norm_smulRightL_le : ‖smulRightL 𝕜 E Fₗ‖ ≤ 1 :=
  LinearMap.mkContinuous₂_norm_le _ zero_le_one _

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

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

Разделы

Аффилиация

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