norm_extendTo𝕜

Mathlib.Analysis.Normed.Module.RCLike.Extend

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.norm_extendTo𝕜

English

Alternate presentation of the bound on the 𝕜-extension norm.

Русский

Альтернативная формулировка границы нормы расширения 𝕜.

LaTeX

$$$\\|fr.extendTo𝕜' x\\| ≤ \\|fr\\| \\cdot \\|x\\|$$$

Lean4

@[simp]
theorem norm_extendTo𝕜 (fr : StrongDual ℝ (RestrictScalars ℝ 𝕜 F)) : ‖fr.extendTo𝕜‖ = ‖fr‖ :=
  fr.norm_extendTo𝕜'

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

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

Разделы

Аффилиация

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