norm_bilinearRestrictScalars

Mathlib.Analysis.Normed.Operator.Bilinear

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

English

For x ∈ E and y ∈ F, the evaluation of bilinearRestrictScalars at (x,y) equals the evaluation of B at (x,y).

Русский

Для x ∈ E и y ∈ F значение bilinearRestrictScalars при (x,y) равно значению B при (x,y).

LaTeX

$$$ (B.bilinearRestrictScalars 𝕜) x y = B x y $$$

Lean4

@[simp]
theorem norm_bilinearRestrictScalars : ‖B.bilinearRestrictScalars 𝕜‖ = ‖B‖ :=
  rfl

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

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

Разделы

Аффилиация

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