id

Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

URI: https://scilib.ai/kg/mathlib#IsBoundedLinearMap.id

English

Applying bilinearRestrictScalars to x,y gives the same result as B(x,y)

Русский

Применение bilinearRestrictScalars к x,y дает тот же результат, что и B(x,y).

LaTeX

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

Lean4

theorem id : IsBoundedLinearMap 𝕜 fun x : E => x :=
  LinearMap.id.isLinear.with_bound 1 <| by simp [le_refl]

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

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

Разделы

Аффилиация

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