norm_smulRightL_apply

Mathlib.Analysis.Normed.Operator.Bilinear

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

English

The same norm identity holds for smulRightL: ||smulRightL c f|| = ||c|| · ||f||.

Русский

Для smulRightL выполняется та же тождество норм: ||smulRightL c f|| = ||c|| · ||f||.

LaTeX

$$$ \\|smulRightL\\,c\\,f\\| = \\|c\\| \\cdot \\|f\\| $$$

Lean4

@[simp]
theorem norm_smulRightL_apply (c : StrongDual 𝕜 E) (f : Fₗ) : ‖smulRightL 𝕜 E Fₗ c f‖ = ‖c‖ * ‖f‖ :=
  norm_smulRight_apply c f

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

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

Разделы

Аффилиация

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